Transition.lean`

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Finite weak transition components and finite-scan instruction semantics.

def OAI.FiniteAlgebraicEnvelopes.Compiler.Terminal line 15
Source documentation
An internal terminal configuration has no forward transition.
```
def Terminal (r : α → α → Prop) (a : α) : Prop := ∀ b, ¬ r a b
```
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.deterministic_join line 18
Source documentation
Determinism makes forward-reachability joins an equivalence relation.
```
theorem deterministic_join (hr : Relator.RightUnique r) :
    Equivalence (Join (ReflTransGen r)) := by
…
```
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.weak_component_joins line 28
Source documentation
Undirected internal connectivity may be converted to a common forward descendant; no reversibility of the simulated machine is required.
```
theorem weak_component_joins (hr : Relator.RightUnique r) {a b : α}
    (h : EqvGen r a b) : Join (ReflTransGen r) a b := by
…
```
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.terminal_eq_of_reaches line 33
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.reaches_terminal line 42
Source documentation
Every configuration in a terminal's weak component reaches that terminal. This is the graph-theoretic core of source Lemma compiler-components, and holds even without the finite-component assumption.
```
theorem reaches_terminal (hr : Relator.RightUnique r) {a b : α}
    (hb : Terminal r b) (hab : EqvGen r a b) : ReflTransGen r a b := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Terminal
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.terminal_unique line 50
Source documentation
In particular there cannot be two successful terminal sectors in the same weak component, even with arbitrary reverse branching on dirty data.
```
theorem terminal_unique (hr : Relator.RightUnique r) {a b : α}
    (ha : Terminal r a) (hb : Terminal r b) (hab : EqvGen r a b) : a=b :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Terminal
structure OAI.FiniteAlgebraicEnvelopes.Compiler.Configuration line 56
Source documentation
Fixed ordered bases, a head gap, and finite tags are the finite search data of the finite compiler. Workspace quota insertion is NOT an internal step.
```
structure Configuration (Head Tag : Type*) (k : ℕ) where
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Tag
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.configuration_card line 62
def OAI.FiniteAlgebraicEnvelopes.Compiler.expand line 77
Source documentation
One effective expansion by undirected internal edges.
```
def expand (s : Finset α) : Finset α :=
…
```
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.mem_expand line 80
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.subset_expand line 84
def OAI.FiniteAlgebraicEnvelopes.Compiler.search line 88
Source documentation
This finite algorithm never calls the simulated partial function.
```
def search (a : α) : ℕ → Finset α
  | 0 => {a}
  | n+1 => expand r (search a n)
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.expand
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.search_mono line 92
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.search_stabilizes line 97
def OAI.FiniteAlgebraicEnvelopes.Compiler.component line 115
Source documentation
Entire weak component, computed by at most the known number of vertices many finite expansions. Unlike running the machine, this always terminates.
```
def component (a : α) : Finset α := search r a (Fintype.card α)
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.search
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.self_mem_component line 117
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.component_saturated line 120
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.mem_search_connected line 127
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.mem_component_iff line 144
Source documentation
Exactness of the finite component search on malformed as well as genuine configurations.
```
theorem mem_component_iff (a b : α) : b ∈ component r a ↔ EqvGen r a b := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.component
def OAI.FiniteAlgebraicEnvelopes.Compiler.decideConnected line 158
Source documentation
Consequently internal weak connectivity has a decision procedure that uses only the table and finite configuration data, not a halting oracle.
```
def decideConnected (a b : α) : Bool := decide (b ∈ component r a)
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.component
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.decideConnected_eq_true line 160
inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Base line 167
Source comment
The actual finite-scan instruction semantics of the finite compiler. The immutable bases are not part of what an instruction may update.
```
inductive Base (S : Type*)
  | anchor : S → Base S
  | cutC : Base S
  | cutD : Base S
  | workspace : Base S
  deriving DecidableEq, Fintype
```
structure OAI.FiniteAlgebraicEnvelopes.Compiler.Tag line 174
def OAI.FiniteAlgebraicEnvelopes.Compiler.clean line 183
Source documentation
The same clean tag is used on every base, including its unused fields.
```
def clean {S Γ : Type*} (blank : Γ) : Tag S Γ :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Tag
inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Direction line 186
instance OAI.FiniteAlgebraicEnvelopes.Compiler.(instance at line 190) line 190
structure OAI.FiniteAlgebraicEnvelopes.Compiler.Instruction line 192
structure OAI.FiniteAlgebraicEnvelopes.Compiler.Table line 201
Source documentation
Each state designates one reading side. A cell test has at most one result; boundary tests only change the state. A failed (or absent-boundary) test has no result. This is exactly the source's disjoint-case convention.
```
structure Table (Head Base Tag : Type*) where
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag
def OAI.FiniteAlgebraicEnvelopes.Compiler.step line 209
Source documentation
The finite state transition on sectors with fixed ordered base sequence. The two flags record whether alpha and omega are present. There is no insertion or deletion among internal steps.
```
def step {Head Base Tag : Type*} (table : Table Head Base Tag)
    {k : ℕ} (bases : Fin k → Base) (leftBoundary rightBoundary : Bool)
    (c : Configuration Head Tag k) : Option (Configuration Head Tag k) :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Table, OAI.FiniteAlgebraicEnvelopes.Compiler.Configuration
def OAI.FiniteAlgebraicEnvelopes.Compiler.InternalStep line 236
Source documentation
The relation used for component search; the equation is used both ways in the presentation, but only this direction in the deterministic analysis.
```
def InternalStep {Head Base Tag : Type*} (table : Table Head Base Tag)
    {k : ℕ} (bases : Fin k → Base) (leftBoundary rightBoundary : Bool)
    (c d : Configuration Head Tag k) : Prop :=
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Table, OAI.FiniteAlgebraicEnvelopes.Compiler.Configuration
instance OAI.FiniteAlgebraicEnvelopes.Compiler.(instance at line 241) line 241
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.internalStep_deterministic line 248
Source documentation
Determinism is proved on ALL data, not assumed for clean initial sectors.
```
theorem internalStep_deterministic {Head Base Tag : Type*} (table : Table Head Base Tag)
    {k : ℕ} (bases : Fin k → Base) (leftBoundary rightBoundary : Bool) :
    Relator.RightUnique (InternalStep table bases leftBoundary rightBoundary) := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Table, OAI.FiniteAlgebraicEnvelopes.Compiler.InternalStep
theorem OAI.FiniteAlgebraicEnvelopes.Compiler.internal_terminal_reached line 255
Source documentation
The success-terminal assertion applies directly to the finite scan semantics.
```
theorem internal_terminal_reached {Head Base Tag : Type*} (table : Table Head Base Tag)
    {k : ℕ} (bases : Fin k → Base) (l r : Bool) {a b : Configuration Head Tag k}
    (hb : step table bases l r b = none)
    (hab : EqvGen (InternalStep table bases l r) a b) :
    ReflTransGen (InternalStep table bases l r) a b := by
…
```
Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Table, OAI.FiniteAlgebraicEnvelopes.Compiler.Configuration, OAI.FiniteAlgebraicEnvelopes.Compiler.step, OAI.FiniteAlgebraicEnvelopes.Compiler.InternalStep