One-way-liveness proof: Diagrams

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Automata/Diagrams.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.prod_compatible_chain {A : Type} [Fintype A] (as : List (Pairing (A ⊕ A))) (l r : A → Bool) : as.prod.Compatible (Sum.elim l r) ↔ ∃ (b : ℕ → A → Bool), b 0 = l ∧ b as.length = r ∧ ∀ (i : ℕ) (hi : i < as.length), as[i].Compatible (Sum.elim (b i) (b (i + 1)))

theorem Complexity.FiniteAutomaton.Pairing.ofFn_compatible_chain {A : Type} [Fintype A] {n : ℕ} (as : Fin n → Pairing (A ⊕ A)) (l r : A → Bool) : (List.ofFn as).prod.Compatible (Sum.elim l r) ↔ ∃ (b : ℕ → A → Bool), b 0 = l ∧ b n = r ∧ ∀ (i : Fin n), (as i).Compatible (Sum.elim (b ↑i) (b (↑i + 1)))

structure Complexity.FiniteAutomaton.CellNetwork.ColorData {Q Alpha : Type} [Fintype Q] (M : Machine Alpha Q) (finish : Q) (w : List Alpha) : Type

Boundary and tip colorings compatible with every local pairing and join.

• boundary : ℕ → Port Q → Bool

  Colors assigned to ports along each cell boundary.

• tip : Fin (w.length + 2) → Tip Q → Bool

  Colors assigned to the two tips of each cell incidence.

• port_eq (i : Fin (w.length + 2)) (s : Bool) (slot : Slot Q) (l : Bool) : (if s = true then self.boundary (↑i + 1) else self.boundary ↑i) (slot, l) = self.tip i (Sum.inl (s, slot), tipRole s l)
• stay_eq (i : Fin (w.length + 2)) (pq : Q × Q) (role t : Bool) : self.tip i (Sum.inr (pq, role), t) = self.tip i (Sum.inr (pq, !role), !t)
• join_eq (i : Fin (w.length + 2)) (j : Incidence Q) : self.tip i (j, false) = self.tip i ((orders M finish (scanned w i)).perm j, true)

noncomputable def Complexity.FiniteAutomaton.CellNetwork.bodyDiagram {Q Alpha : Type} [Fintype Q] (M : Machine Alpha Q) (finish : Q) (b : Symbol Alpha) : Pairing (Port Q ⊕ Port Q)

The boundary pairing for one scanned symbol and chosen terminal state.

Equations

• Complexity.FiniteAutomaton.CellNetwork.bodyDiagram M finish b = Complexity.FiniteAutomaton.CellNetwork.diagram Q (Complexity.FiniteAutomaton.CellNetwork.orders M finish b).perm

noncomputable def Complexity.FiniteAutomaton.CellNetwork.fullDiagram {Q Alpha : Type} [Fintype Q] (M : Machine Alpha Q) (finish : Q) (w : List Alpha) : Pairing (Port Q ⊕ Port Q)

The product of all cell diagrams, including the two endmarkers.

Equations

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

theorem Complexity.FiniteAutomaton.CellNetwork.fullDiagram_compatible {Q Alpha : Type} [Fintype Q] (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (l r : Port Q → Bool) : (fullDiagram M finish w).Compatible (Sum.elim l r) ↔ ∃ (C : ColorData M finish w), C.boundary 0 = l ∧ C.boundary (w.length + 2) = r

def Complexity.FiniteAutomaton.CellNetwork.Flat {Q : Type} (c : Port Q → Bool) : Prop

Both lanes of every port slot have the same color.

Equations

• Complexity.FiniteAutomaton.CellNetwork.Flat c = ∀ (slot : Complexity.FiniteAutomaton.CellNetwork.Slot Q), c (slot, false) = c (slot, true)

def Complexity.FiniteAutomaton.CellNetwork.Separated {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (l r : Port Q → Bool) : Prop

Flat boundary colors distinguish the initial and terminal test ports.

Equations

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

def Complexity.FiniteAutomaton.CellNetwork.ColorData.wholeTip {Q Alpha : Type} [Fintype Q] {M : Machine Alpha Q} {finish : Q} {w : List Alpha} (C : ColorData M finish w) : WholeInc Q w.length → Bool → Bool

Restoring a reflection at every outer leaf extends the tip assignment.

Equations

• C.wholeTip (Sum.inl (i, j)) x✝ = C.tip i (j, x✝)
• C.wholeTip (Sum.inr (s, slot)) x✝ = C.boundary (if s = true then w.length + 2 else 0) (slot, Complexity.FiniteAutomaton.CellNetwork.tipRole s !x✝)

theorem Complexity.FiniteAutomaton.CellNetwork.ColorData.wholeTip_join {Q Alpha : Type} [Fintype Q] {M : Machine Alpha Q} {finish : Q} {w : List Alpha} (C : ColorData M finish w) (hl : Flat (C.boundary 0)) (hr : Flat (C.boundary (w.length + 2))) (x : WholeInc Q w.length) : C.wholeTip x false = C.wholeTip ((wholeOrder M finish w).perm x) true

theorem Complexity.FiniteAutomaton.CellNetwork.ColorData.wholeTip_lane {Q Alpha : Type} [Fintype Q] {M : Machine Alpha Q} {finish : Q} {w : List Alpha} (C : ColorData M finish w) (d : Edge Q w.length × Bool) : C.wholeTip (edgeInc Q w.length d) true = C.wholeTip (edgeInc Q w.length ((graph M finish w).flip d)) false

theorem Complexity.FiniteAutomaton.CellNetwork.ColorData.tour_invariant {Q Alpha : Type} [Fintype Q] {M : Machine Alpha Q} {finish : Q} {w : List Alpha} (C : ColorData M finish w) (hl : Flat (C.boundary 0)) (hr : Flat (C.boundary (w.length + 2))) (d : Edge Q w.length × Bool) : C.wholeTip (edgeInc Q w.length ((graphOrder M finish w).tour d)) true = C.wholeTip (edgeInc Q w.length d) true

theorem Complexity.FiniteAutomaton.CellNetwork.reach_excludes_separation {Q Alpha : Type} [Fintype Q] (M : Machine Alpha Q) (finish : Q) (ht : M.transition finish Symbol.right = none) (w : List Alpha) (hp : Relation.ReflTransGen (M.Step w) (outCell w.length false, M.initial) (outCell w.length true, finish)) (C : ColorData M finish w) : ¬Separated M finish (C.boundary 0) (C.boundary (w.length + 2))

theorem Complexity.FiniteAutomaton.CellNetwork.vertex_color_flip {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (c : Vertex Q w.length → Bool) (hc : ∀ (e : Edge Q w.length), c ((graph M finish w).src e) = c ((graph M finish w).dst e)) (d : Edge Q w.length × Bool) : c (wholeVertex M finish w (edgeInc Q w.length d)) = c (wholeVertex M finish w (edgeInc Q w.length ((graph M finish w).flip d)))

A vertex coloring which is constant along all edges also respects all local joins, regardless of cycles in other components.

theorem Complexity.FiniteAutomaton.CellNetwork.vertex_color_adjacent {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (c : Vertex Q w.length → Bool) (hc : ∀ (e : Edge Q w.length), c ((graph M finish w).src e) = c ((graph M finish w).dst e)) (i : Fin (w.length + 1)) (slot : Slot Q) : c (wholeVertex M finish w (Sum.inl (i.castSucc, Sum.inl (true, slot)))) = c (wholeVertex M finish w (Sum.inl (i.succ, Sum.inl (false, slot))))

noncomputable def Complexity.FiniteAutomaton.CellNetwork.boundaryColor {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (c : Vertex Q w.length → Bool) (k : ℕ) (p : Port Q) : Bool

Read a boundary-port color from the corresponding graph vertex.

Equations

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

theorem Complexity.FiniteAutomaton.CellNetwork.boundaryColor_right {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (c : Vertex Q w.length → Bool) (i : Fin (w.length + 2)) (slot : Slot Q) (lane : Bool) : boundaryColor M finish w c (↑i + 1) (slot, lane) = c (wholeVertex M finish w (Sum.inl (i, Sum.inl (true, slot))))

theorem Complexity.FiniteAutomaton.CellNetwork.boundaryColor_left {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (c : Vertex Q w.length → Bool) (hc : ∀ (e : Edge Q w.length), c ((graph M finish w).src e) = c ((graph M finish w).dst e)) (i : Fin (w.length + 2)) (slot : Slot Q) (lane : Bool) : boundaryColor M finish w c ↑i (slot, lane) = c (wholeVertex M finish w (Sum.inl (i, Sum.inl (false, slot))))

noncomputable def Complexity.FiniteAutomaton.CellNetwork.vertexColorData {Q Alpha : Type} [Fintype Q] (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (c : Vertex Q w.length → Bool) (hc : ∀ (e : Edge Q w.length), c ((graph M finish w).src e) = c ((graph M finish w).dst e)) : ColorData M finish w

An edge-constant vertex coloring induces compatible local color data.

Equations

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

theorem Complexity.FiniteAutomaton.CellNetwork.boundaryColor_test {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (c : Vertex Q w.length → Bool) (hc : ∀ (e : Edge Q w.length), c ((graph M finish w).src e) = c ((graph M finish w).dst e)) (s lane : Bool) : boundaryColor M finish w c (if s = true then w.length + 2 else 0) (testSlot M finish, lane) = c (stateVertex w (outCell w.length s, if s = true then finish else M.initial))

theorem Complexity.FiniteAutomaton.CellNetwork.separation_of_not_reach {Q Alpha : Type} [Fintype Q] (M : Machine Alpha Q) (finish : Q) (ht : M.transition finish Symbol.right = none) (w : List Alpha) (hp : ¬Relation.ReflTransGen (M.Step w) (outCell w.length false, M.initial) (outCell w.length true, finish)) : ∃ (C : ColorData M finish w), Separated M finish (C.boundary 0) (C.boundary (w.length + 2))

theorem Complexity.FiniteAutomaton.CellNetwork.diagram_recognizes_reach {Q Alpha : Type} [Fintype Q] (M : Machine Alpha Q) (finish : Q) (ht : M.transition finish Symbol.right = none) (w : List Alpha) : (¬∃ (l : Port Q → Bool) (r : Port Q → Bool), (fullDiagram M finish w).Compatible (Sum.elim l r) ∧ Separated M finish l r) ↔ Relation.ReflTransGen (M.Step w) (outCell w.length false, M.initial) (outCell w.length true, finish)

The Boolean test recovers exactly acceptance, not a halting assumption. Only the normalized distinguished right state is required to be terminal.