Chain.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TwoWayComplementation.ChainNode line 10

Source documentation

Internal vertices of a chain with one distinguished final cell.

def ChainNode (m : ℕ) : ℕ → Type
  | 0 => Fin m
  | n + 1 => Fin m ⊕ ChainNode m n

namespace ChainNode

/-- Zero-based cell coordinate. -/

def OAI.TwoWayComplementation.ChainNode.position line 17
Source documentation
Zero-based cell coordinate.
```
def position {m : ℕ} : {n : ℕ} → ChainNode m n → ℕ
  | 0, _ => 0
  | _ + 1, .inl _ => 0
  | _ + 1, .inr c => c.position + 1

/-- State label carried at a cell. -/
```
Mentions: OAI.TwoWayComplementation.ChainNode, OAI.TwoWayComplementation.ChainNode.label

def OAI.TwoWayComplementation.ChainNode.label line 23

Source documentation

State label carried at a cell.

def label {m : ℕ} : {n : ℕ} → ChainNode m n → Fin m
  | 0, q => q
  | _ + 1, .inl q => q
  | _ + 1, .inr c => c.label

/-- Every vertex belongs to one of the chain's cells. -/

Mentions: OAI.TwoWayComplementation.ChainNode

theorem OAI.TwoWayComplementation.ChainNode.position_le line 29
Source documentation
Every vertex belongs to one of the chain's cells.
```
theorem position_le {m n : ℕ} (c : ChainNode m n) : c.position ≤ n := by
…
```
Mentions: OAI.TwoWayComplementation.ChainNode
theorem OAI.TwoWayComplementation.ChainNode.coordinates_injective line 38
Source documentation
A cell coordinate and a state label uniquely identify an internal vertex.
```
theorem coordinates_injective {m n : ℕ} (c d : ChainNode m n)
    (hp : c.position = d.position) (hq : c.label = d.label) : c = d := by
…
```
Mentions: OAI.TwoWayComplementation.ChainNode
theorem OAI.TwoWayComplementation.ChainNode.coordinates_surjective line 54
Source documentation
Every valid cell coordinate and state label occurs.
```
theorem coordinates_surjective {m n : ℕ} (q : Fin m) (p : ℕ) (hp : p ≤ n) :
    ∃ c : ChainNode m n, c.label = q ∧ c.position = p := by
…
```
Mentions: OAI.TwoWayComplementation.ChainNode
def OAI.TwoWayComplementation.chainSymbol line 68
Source documentation
The symbol at a vertex in a nonempty cell chain.
```
def chainSymbol {Sigma : Type*} {m : ℕ} (w : List Sigma) (last : Sigma) :
    ChainNode m w.length → Sigma :=
…
```
Mentions: OAI.TwoWayComplementation.ChainNode
def OAI.TwoWayComplementation.cellNetwork line 77
Source documentation
A single cell retains stays internally and exposes its two moving transitions.
```
def cellNetwork {m : ℕ} (moves : Fin 3 → SetRel (Fin m) (Fin m)) : Network m (Fin m) where
…
```
Mentions: OAI.TwoWayComplementation.Network
def OAI.TwoWayComplementation.chainNetwork line 85
Source documentation
Join a list of cells to a distinguished final cell.
```
def chainNetwork {Sigma : Type*} {m : ℕ}
    (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma) :
    Network m (ChainNode m w.length) :=
…
```
Mentions: OAI.TwoWayComplementation.Network, OAI.TwoWayComplementation.ChainNode

theorem OAI.TwoWayComplementation.chainNetwork_summary line 93

Source documentation

The path summary of a cell chain is the product of its cell diagrams.

theorem chainNetwork_summary {Sigma : Type*} {m : ℕ}
    (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma) :
    (chainNetwork moves w last).summary =
      wordDiagram (fun a => cellDiagram m (moves a 1) (moves a 2) (moves a 0)) (w ++ [last]) := by
…

Mentions: OAI.TwoWayComplementation.chainNetwork, OAI.TwoWayComplementation.wordDiagram, OAI.TwoWayComplementation.cellDiagram

theorem OAI.TwoWayComplementation.chainNetwork_entrances line 109

Source documentation

Entrances attach exactly to the first and last cells with their unchanged labels.

theorem chainNetwork_entrances {Sigma : Type*} {m : ℕ}
    (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma)
    (q : Fin m) (c : ChainNode m w.length) :
    ((q, c) ∈ (chainNetwork moves w last).leftIn ↔ c.position = 0 ∧ q = c.label) ∧
    ((q, c) ∈ (chainNetwork moves w last).rightIn ↔ c.position = w.length ∧ q = c.label) := by
…

Mentions: OAI.TwoWayComplementation.ChainNode, OAI.TwoWayComplementation.chainNetwork

theorem OAI.TwoWayComplementation.chainNetwork_exits line 135

Source documentation

Only the endpoint cells can exit a chain, using the appropriate moving transition.

theorem chainNetwork_exits {Sigma : Type*} {m : ℕ}
    (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma)
    (c : ChainNode m w.length) (q : Fin m) :
    ((c, q) ∈ (chainNetwork moves w last).leftOut ↔
      c.position = 0 ∧ (c.label, q) ∈ moves (chainSymbol w last c) 0) ∧
    ((c, q) ∈ (chainNetwork moves w last).rightOut ↔
      c.position = w.length ∧ (c.label, q) ∈ moves (chainSymbol w last c) 2) := by
…

Mentions: OAI.TwoWayComplementation.ChainNode, OAI.TwoWayComplementation.chainNetwork, OAI.TwoWayComplementation.chainSymbol

theorem OAI.TwoWayComplementation.chainNetwork_edges line 166

Source documentation

Internal edges are precisely local transitions that stay within the chain.

theorem chainNetwork_edges {Sigma : Type*} {m : ℕ}
    (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma)
    (c d : ChainNode m w.length) :
    (c, d) ∈ (chainNetwork moves w last).edge ↔
      ∃ move : Fin 3, (c.label, d.label) ∈ moves (chainSymbol w last c) move ∧
        (d.position : ℤ) = (c.position : ℤ) + (move.val : ℤ) - 1 := by
…

Mentions: OAI.TwoWayComplementation.ChainNode, OAI.TwoWayComplementation.chainNetwork, OAI.TwoWayComplementation.chainSymbol