One-way-liveness proof: Cells

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Automata/Cells.lean

Module and namespace names, imports, and formatting are adapted to complexitylib. The machine definitions are shared through Models.FiniteAutomaton.Defs.

theorem Complexity.FiniteAutomaton.Pairing.transport_compatible {P : Type u_1} {Q : Type u_2} {C : Type u_3} (a : Pairing P) (e : P ≃ Q) (c : Q → C) : (a.transport e).Compatible c ↔ a.Compatible (c ∘ ⇑e)

noncomputable def Complexity.FiniteAutomaton.Pairing.close {P I : Type} [Fintype P] [Fintype I] (lanes : Pairing (P ⊕ I)) (joins : Pairing I) : Pairing P

Close all internal tips with a matching of local joins.

Equations

• lanes.close joins = (lanes.compose (joins.transport (Equiv.sumEmpty I Empty).symm)).transport (Equiv.sumEmpty P Empty)

theorem Complexity.FiniteAutomaton.Pairing.close_compatible {P I : Type} [Fintype P] [Fintype I] (lanes : Pairing (P ⊕ I)) (joins : Pairing I) (c : P → Bool) : (lanes.close joins).Compatible c ↔ ∃ (f : I → Bool), lanes.Compatible (Sum.elim c f) ∧ joins.Compatible f

theorem Complexity.FiniteAutomaton.Pairing.ofInvolution_compatible {P : Type u_1} {C : Type u_2} (f : P → P) (hf : Function.Involutive f) (hn : ∀ (p : P), f p ≠ p) (c : P → C) : (ofInvolution f hf hn).Compatible c ↔ ∀ (p : P), c p = c (f p)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.CellNetwork.Slot (Q : Type) : Type

true directs the prospective successor to the right.

Equations

• Complexity.FiniteAutomaton.CellNetwork.Slot Q = (Bool × Q × Q)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.CellNetwork.Port (Q : Type) : Type

A directed transition slot together with one of its two lanes.

Equations

• Complexity.FiniteAutomaton.CellNetwork.Port Q = (Complexity.FiniteAutomaton.CellNetwork.Slot Q × Bool)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.CellNetwork.Boundary (Q : Type) : Type

A transition slot labelled by the side of the cell.

Equations

• Complexity.FiniteAutomaton.CellNetwork.Boundary Q = (Bool × Complexity.FiniteAutomaton.CellNetwork.Slot Q)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.CellNetwork.Incidence (Q : Type) : Type

Boundary incidences and the two ends of stationary-transition edges.

Equations

• Complexity.FiniteAutomaton.CellNetwork.Incidence Q = (Complexity.FiniteAutomaton.CellNetwork.Boundary Q ⊕ (Q × Q) × Bool)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.CellNetwork.Tip (Q : Type) : Type

An incidence together with its lane.

Equations

• Complexity.FiniteAutomaton.CellNetwork.Tip Q = (Complexity.FiniteAutomaton.CellNetwork.Incidence Q × Bool)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.CellNetwork.LocalVertex (Q : Type) : Type

Machine states and unattached incidences within a cell.

Equations

• Complexity.FiniteAutomaton.CellNetwork.LocalVertex Q = (Q ⊕ Complexity.FiniteAutomaton.CellNetwork.Incidence Q)

def Complexity.FiniteAutomaton.CellNetwork.tipRole (side lane : Bool) : Bool

A lane's absolute label changes its incoming/outgoing role between opposite sides of a cell.

Equations

• Complexity.FiniteAutomaton.CellNetwork.tipRole side lane = (side ^^ lane)

@[simp]

theorem Complexity.FiniteAutomaton.CellNetwork.tipRole_twice (s l : Bool) : tipRole s (tipRole s l) = l

@[simp]

theorem Complexity.FiniteAutomaton.CellNetwork.tipRole_ne (s l : Bool) : tipRole (!s) l = !tipRole s l

def Complexity.FiniteAutomaton.CellNetwork.laneMate (Q : Type) : Boundary Q × Bool ⊕ Tip Q → Boundary Q × Bool ⊕ Tip Q

All stay candidates are allowed locally; a nontransition candidate will be attached to a fresh leaf. This leaves the external degree unchanged.

Equations

• Complexity.FiniteAutomaton.CellNetwork.laneMate Q (Sum.inl (b, l)) = Sum.inr (Sum.inl b, Complexity.FiniteAutomaton.CellNetwork.tipRole b.1 l)
• Complexity.FiniteAutomaton.CellNetwork.laneMate Q (Sum.inr (Sum.inl b, t)) = Sum.inl (b, Complexity.FiniteAutomaton.CellNetwork.tipRole b.1 t)
• Complexity.FiniteAutomaton.CellNetwork.laneMate Q (Sum.inr (Sum.inr (pq, r), t)) = Sum.inr (Sum.inr (pq, !r), !t)

theorem Complexity.FiniteAutomaton.CellNetwork.laneMate_involutive (Q : Type) : Function.Involutive (laneMate Q)

theorem Complexity.FiniteAutomaton.CellNetwork.laneMate_ne (Q : Type) (p : Boundary Q × Bool ⊕ Tip Q) : laneMate Q p ≠ p

def Complexity.FiniteAutomaton.CellNetwork.lanes (Q : Type) : Pairing (Boundary Q × Bool ⊕ Tip Q)

The pairing connecting boundary lanes and stationary-transition tips.

Equations

• Complexity.FiniteAutomaton.CellNetwork.lanes Q = Complexity.FiniteAutomaton.Pairing.ofInvolution (Complexity.FiniteAutomaton.CellNetwork.laneMate Q) ⋯ ⋯

def Complexity.FiniteAutomaton.CellNetwork.joinMate (Q : Type) (r : Equiv.Perm (Incidence Q)) : Tip Q → Tip Q

Join a forward tip to its successor and a backward tip to its predecessor.

Equations

• Complexity.FiniteAutomaton.CellNetwork.joinMate Q r (i, false) = (r i, true)
• Complexity.FiniteAutomaton.CellNetwork.joinMate Q r (i, true) = ((Equiv.symm r) i, false)

theorem Complexity.FiniteAutomaton.CellNetwork.joinMate_involutive (Q : Type) (r : Equiv.Perm (Incidence Q)) : Function.Involutive (joinMate Q r)

theorem Complexity.FiniteAutomaton.CellNetwork.joinMate_ne (Q : Type) (r : Equiv.Perm (Incidence Q)) (p : Tip Q) : joinMate Q r p ≠ p

def Complexity.FiniteAutomaton.CellNetwork.joins (Q : Type) (r : Equiv.Perm (Incidence Q)) : Pairing (Tip Q)

The tip pairing induced by the cyclic incidence order.

Equations

• Complexity.FiniteAutomaton.CellNetwork.joins Q r = Complexity.FiniteAutomaton.Pairing.ofInvolution (Complexity.FiniteAutomaton.CellNetwork.joinMate Q r) ⋯ ⋯

theorem Complexity.FiniteAutomaton.CellNetwork.lanes_compatible (Q : Type) (c : Boundary Q × Bool → Bool) (f : Tip Q → Bool) : (lanes Q).Compatible (Sum.elim c f) ↔ (∀ (b : Boundary Q) (l : Bool), c (b, l) = f (Sum.inl b, tipRole b.1 l)) ∧ ∀ (pq : Q × Q) (r t : Bool), f (Sum.inr (pq, r), t) = f (Sum.inr (pq, !r), !t)

theorem Complexity.FiniteAutomaton.CellNetwork.joins_compatible (Q : Type) (r : Equiv.Perm (Incidence Q)) (f : Tip Q → Bool) : (joins Q r).Compatible f ↔ ∀ (i : Incidence Q), f (i, false) = f (r i, true)

def Complexity.FiniteAutomaton.CellNetwork.portsEquiv (Q : Type) : Boundary Q × Bool ≃ Port Q ⊕ Port Q

The two sides use exactly the same slot/lane labels.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.FiniteAutomaton.CellNetwork.diagram (Q : Type) [Fintype Q] (r : Equiv.Perm (Incidence Q)) : Pairing (Port Q ⊕ Port Q)

Close the internal tips to obtain the cell boundary pairing.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.FiniteAutomaton.CellNetwork.diagram_compatible (Q : Type) [Fintype Q] (r : Equiv.Perm (Incidence Q)) (left right : Port Q → Bool) : (diagram Q r).Compatible (Sum.elim left right) ↔ ∃ (f : Tip Q → Bool), (∀ (s : Bool) (slot : Slot Q) (l : Bool), (if s = true then right else left) (slot, l) = f (Sum.inl (s, slot), tipRole s l)) ∧ (∀ (pq : Q × Q) (role t : Bool), f (Sum.inr (pq, role), t) = f (Sum.inr (pq, !role), !t)) ∧ ∀ (i : Incidence Q), f (i, false) = f (r i, true)