One-way-liveness proof: Network

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

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

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.CellNetwork.Edge (Q : Type) (n : ℕ) : Type

Edges of all crossing and stay candidates, together with all outward slots. Every outward slot is an edge to its own external leaf.

Equations

• Complexity.FiniteAutomaton.CellNetwork.Edge Q n = (Fin (n + 1) × Complexity.FiniteAutomaton.CellNetwork.Slot Q ⊕ Fin (n + 2) × Q × Q ⊕ Bool × Complexity.FiniteAutomaton.CellNetwork.Slot Q)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.CellNetwork.WholeInc (Q : Type) (n : ℕ) : Type

All cell incidences, together with the external boundary incidences.

Equations

• Complexity.FiniteAutomaton.CellNetwork.WholeInc Q n = (Fin (n + 2) × Complexity.FiniteAutomaton.CellNetwork.Incidence Q ⊕ Bool × Complexity.FiniteAutomaton.CellNetwork.Slot Q)

def Complexity.FiniteAutomaton.CellNetwork.outCell (n : ℕ) (s : Bool) : Fin (n + 2)

The left or right endmarker position.

Equations

• Complexity.FiniteAutomaton.CellNetwork.outCell n s = if s = true then ⟨n + 1, ⋯⟩ else ⟨0, ⋯⟩

def Complexity.FiniteAutomaton.CellNetwork.edgeInc (Q : Type) (n : ℕ) : Edge Q n × Bool → WholeInc Q n

Locate an oriented incidence in its cell, or at its external leaf.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.FiniteAutomaton.CellNetwork.edgeInc Q n (Sum.inl (j, slot), b) = if (slot.1 ^^ b) = true then Sum.inl (j.castSucc, Sum.inl (true, slot)) else Sum.inl (j.succ, Sum.inl (false, slot))
• Complexity.FiniteAutomaton.CellNetwork.edgeInc Q n (Sum.inr (Sum.inl (i, pq)), b) = Sum.inl (i, Sum.inr (pq, b))

def Complexity.FiniteAutomaton.CellNetwork.incEdge (Q : Type) (n : ℕ) : WholeInc Q n → Edge Q n × Bool

Recover the edge and endpoint corresponding to an incidence.

Equations

• Complexity.FiniteAutomaton.CellNetwork.incEdge Q n (Sum.inl (i, Sum.inl (false, slot))) = if h : ↑i = 0 then (Sum.inr (Sum.inr (false, slot)), true) else (Sum.inl (⟨↑i - 1, ⋯⟩, slot), slot.1)
• Complexity.FiniteAutomaton.CellNetwork.incEdge Q n (Sum.inl (i, Sum.inl (true, slot))) = if h : ↑i = n + 1 then (Sum.inr (Sum.inr (true, slot)), true) else (Sum.inl (⟨↑i, ⋯⟩, slot), !slot.1)
• Complexity.FiniteAutomaton.CellNetwork.incEdge Q n (Sum.inl (i, Sum.inr (pq, b))) = (Sum.inr (Sum.inl (i, pq)), b)
• Complexity.FiniteAutomaton.CellNetwork.incEdge Q n (Sum.inr (s, slot)) = (Sum.inr (Sum.inr (s, slot)), false)

theorem Complexity.FiniteAutomaton.CellNetwork.incEdge_edgeInc (Q : Type) (n : ℕ) (d : Edge Q n × Bool) : incEdge Q n (edgeInc Q n d) = d

theorem Complexity.FiniteAutomaton.CellNetwork.edgeInc_incEdge (Q : Type) (n : ℕ) (d : WholeInc Q n) : edgeInc Q n (incEdge Q n d) = d

def Complexity.FiniteAutomaton.CellNetwork.incidenceEquiv (Q : Type) (n : ℕ) : Edge Q n × Bool ≃ WholeInc Q n

Identify edge endpoints with the full set of incidences.

Equations

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

@[reducible, inline]

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

A complete proposed successor, including its source and target state.

Equations

• Complexity.FiniteAutomaton.CellNetwork.Key Q = (Complexity.FiniteAutomaton.Move × Q × Q)

def Complexity.FiniteAutomaton.CellNetwork.sourceInc (Q : Type) : Key Q → Incidence Q

The incidence associated with the source of a potential transition.

Equations

• Complexity.FiniteAutomaton.CellNetwork.sourceInc Q (Complexity.FiniteAutomaton.Move.left, p, q) = Sum.inl (false, false, p, q)
• Complexity.FiniteAutomaton.CellNetwork.sourceInc Q (Complexity.FiniteAutomaton.Move.stay, p, q) = Sum.inr ((p, q), false)
• Complexity.FiniteAutomaton.CellNetwork.sourceInc Q (Complexity.FiniteAutomaton.Move.right, p, q) = Sum.inl (true, true, p, q)

theorem Complexity.FiniteAutomaton.CellNetwork.sourceInc_injective (Q : Type) : Function.Injective (sourceInc Q)

noncomputable def Complexity.FiniteAutomaton.CellNetwork.sourceAttach {Q Alpha : Type} (M : Machine Alpha Q) (b : Symbol Alpha) (k : Key Q) : LocalVertex Q

Attach an enabled transition to its source state; otherwise leave it unattached.

Equations

• Complexity.FiniteAutomaton.CellNetwork.sourceAttach M b k = if M.transition k.2.1 b = some (k.2.2, k.1) then Sum.inl k.2.1 else Sum.inr (Complexity.FiniteAutomaton.CellNetwork.sourceInc Q k)

theorem Complexity.FiniteAutomaton.CellNetwork.sourceAttach_injective {Q Alpha : Type} (M : Machine Alpha Q) (b : Symbol Alpha) : Function.Injective (sourceAttach M b)

theorem Complexity.FiniteAutomaton.CellNetwork.sourceAttach_eq_state {Q Alpha : Type} (M : Machine Alpha Q) (b : Symbol Alpha) (k : Key Q) (p : Q) : sourceAttach M b k = Sum.inl p ↔ k.2.1 = p ∧ M.transition p b = some (k.2.2, k.1)

def Complexity.FiniteAutomaton.CellNetwork.outward {Alpha : Type} : Symbol Alpha → Bool → Bool

Only the side facing away from the input is outward.

Equations

• Complexity.FiniteAutomaton.CellNetwork.outward Complexity.FiniteAutomaton.Symbol.left x✝ = !x✝
• Complexity.FiniteAutomaton.CellNetwork.outward Complexity.FiniteAutomaton.Symbol.right x✝ = x✝
• Complexity.FiniteAutomaton.CellNetwork.outward (Complexity.FiniteAutomaton.Symbol.letter a) x✝ = false

def Complexity.FiniteAutomaton.CellNetwork.testSlot {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) : Slot Q

The external test slot connecting the initial state to the selected final state.

Equations

• Complexity.FiniteAutomaton.CellNetwork.testSlot M finish = (true, M.initial, finish)

noncomputable def Complexity.FiniteAutomaton.CellNetwork.localVertex {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (b : Symbol Alpha) : Incidence Q → LocalVertex Q

Attach enabled transitions and designated test ports to their local states.

Equations

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

def Complexity.FiniteAutomaton.CellNetwork.edgeKey (Q : Type) (n : ℕ) : Edge Q n → Fin (n + 2) × Key Q ⊕ Bool × Slot Q

An edge is uniquely determined by the cell, move and states of its source proposal, or by its outward slot.

Equations

• Complexity.FiniteAutomaton.CellNetwork.edgeKey Q n (Sum.inl (j, true, p, q)) = Sum.inl (j.castSucc, Complexity.FiniteAutomaton.Move.right, p, q)
• Complexity.FiniteAutomaton.CellNetwork.edgeKey Q n (Sum.inl (j, false, p, q)) = Sum.inl (j.succ, Complexity.FiniteAutomaton.Move.left, p, q)
• Complexity.FiniteAutomaton.CellNetwork.edgeKey Q n (Sum.inr (Sum.inl (i, p, q))) = Sum.inl (i, Complexity.FiniteAutomaton.Move.stay, p, q)
• Complexity.FiniteAutomaton.CellNetwork.edgeKey Q n (Sum.inr (Sum.inr z)) = Sum.inr z

theorem Complexity.FiniteAutomaton.CellNetwork.edgeKey_injective (Q : Type) (n : ℕ) : Function.Injective (edgeKey Q n)

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.CellNetwork.Vertex (Q : Type) (n : ℕ) : Type

Local vertices in each cell, together with the external test ports.

Equations

• Complexity.FiniteAutomaton.CellNetwork.Vertex Q n = (Fin (n + 2) × Complexity.FiniteAutomaton.CellNetwork.LocalVertex Q ⊕ Bool × Complexity.FiniteAutomaton.CellNetwork.Slot Q)

noncomputable def Complexity.FiniteAutomaton.CellNetwork.decorate {Q Alpha : Type} (M : Machine Alpha Q) (w : List Alpha) : Fin (w.length + 2) × Key Q ⊕ Bool × Slot Q → Vertex Q w.length

Map source keys and external incidences into the global vertex set.

Equations

• Complexity.FiniteAutomaton.CellNetwork.decorate M w (Sum.inl (i, k)) = Sum.inl (i, Complexity.FiniteAutomaton.CellNetwork.sourceAttach M (Complexity.FiniteAutomaton.scanned w i) k)
• Complexity.FiniteAutomaton.CellNetwork.decorate M w (Sum.inr z) = Sum.inr z

theorem Complexity.FiniteAutomaton.CellNetwork.decorate_injective {Q Alpha : Type} (M : Machine Alpha Q) (w : List Alpha) : Function.Injective (decorate M w)

noncomputable def Complexity.FiniteAutomaton.CellNetwork.destination {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) : Edge Q w.length → Vertex Q w.length

The target vertex of a transition or external boundary edge.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.FiniteAutomaton.CellNetwork.destination M finish w (Sum.inl (j, true, _p, q)) = Sum.inl (j.succ, Sum.inl q)
• Complexity.FiniteAutomaton.CellNetwork.destination M finish w (Sum.inl (j, false, _p, q)) = Sum.inl (j.castSucc, Sum.inl q)
• Complexity.FiniteAutomaton.CellNetwork.destination M finish w (Sum.inr (Sum.inl (i, _p, q))) = Sum.inl (i, Sum.inl q)

noncomputable def Complexity.FiniteAutomaton.CellNetwork.graph {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) : FunctionalEdges (Vertex Q w.length) (Edge Q w.length)

The functional graph encoding the machine run and its test ports.

Equations

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

noncomputable def Complexity.FiniteAutomaton.CellNetwork.wholeVertex {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) : WholeInc Q w.length → Vertex Q w.length

The graph vertex associated with each cell or boundary incidence.

Equations

• Complexity.FiniteAutomaton.CellNetwork.wholeVertex M finish w (Sum.inl (i, j)) = Sum.inl (i, Complexity.FiniteAutomaton.CellNetwork.localVertex M finish (Complexity.FiniteAutomaton.scanned w i) j)
• Complexity.FiniteAutomaton.CellNetwork.wholeVertex M finish w (Sum.inr z) = Sum.inr z

theorem Complexity.FiniteAutomaton.CellNetwork.outward_internal {Alpha : Type} (w : List Alpha) (j : Fin (w.length + 1)) : outward (scanned w j.castSucc) true = false ∧ outward (scanned w j.succ) false = false

theorem Complexity.FiniteAutomaton.CellNetwork.graph_vertex {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (d : Edge Q w.length × Bool) : (graph M finish w).vertex d = wholeVertex M finish w (edgeInc Q w.length d)

def Complexity.FiniteAutomaton.CellNetwork.wholePerm {Q Alpha : Type} (w : List Alpha) (r : Symbol Alpha → Equiv.Perm (Incidence Q)) : Equiv.Perm (WholeInc Q w.length)

The same local cyclic orders are used at every occurrence of a symbol.

Equations

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

theorem Complexity.FiniteAutomaton.CellNetwork.wholePerm_pow {Q Alpha : Type} (w : List Alpha) (r : Symbol Alpha → Equiv.Perm (Incidence Q)) (n : ℕ) (i : Fin (w.length + 2)) (j : Incidence Q) : (wholePerm w r ^ n) (Sum.inl (i, j)) = Sum.inl (i, (r (scanned w i) ^ n) j)

noncomputable def Complexity.FiniteAutomaton.CellNetwork.orders {Q Alpha : Type} (M : Machine Alpha Q) [Fintype Q] (finish : Q) (b : Symbol Alpha) : CyclicOrder (localVertex M finish b)

Choose a cyclic order for every local-vertex incidence fiber.

Equations

• Complexity.FiniteAutomaton.CellNetwork.orders M finish b = Complexity.FiniteAutomaton.CyclicOrder.choose (Complexity.FiniteAutomaton.CellNetwork.localVertex M finish b)

noncomputable def Complexity.FiniteAutomaton.CellNetwork.wholeOrder {Q Alpha : Type} (M : Machine Alpha Q) [Fintype Q] (finish : Q) (w : List Alpha) : CyclicOrder (wholeVertex M finish w)

Combine the local cyclic incidence orders over the whole input.

Equations

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

noncomputable def Complexity.FiniteAutomaton.CellNetwork.graphOrder {Q Alpha : Type} (M : Machine Alpha Q) [Fintype Q] (finish : Q) (w : List Alpha) : (graph M finish w).Rotation

Transport the incidence order to a rotation system on graph edge endpoints.

Equations

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

theorem Complexity.FiniteAutomaton.CellNetwork.graphOrder_apply {Q Alpha : Type} (M : Machine Alpha Q) [Fintype Q] (finish : Q) (w : List Alpha) (d : Edge Q w.length × Bool) : edgeInc Q w.length ((graphOrder M finish w).perm d) = (wholeOrder M finish w).perm (edgeInc Q w.length d)

def Complexity.FiniteAutomaton.CellNetwork.stateVertex {Q Alpha : Type} (w : List Alpha) (c : Machine.Config w) : Vertex Q w.length

State configurations embed without identifying any added leaves.

Equations

• Complexity.FiniteAutomaton.CellNetwork.stateVertex w c = Sum.inl (c.1, Sum.inl c.2)

theorem Complexity.FiniteAutomaton.CellNetwork.stateVertex_injective {Q Alpha : Type} (w : List Alpha) : Function.Injective (stateVertex w)

theorem Complexity.FiniteAutomaton.CellNetwork.graph_step_from_state {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (c : Machine.Config w) (v : Vertex Q w.length) : (graph M finish w).Step (stateVertex w c) v ↔ ∃ (c' : Machine.Config w), v = stateVertex w c' ∧ M.Step w c c'

theorem Complexity.FiniteAutomaton.CellNetwork.graph_reach_state {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (c c' : Machine.Config w) : (graph M finish w).Reach (stateVertex w c) (stateVertex w c') ↔ Relation.ReflTransGen (M.Step w) c c'

theorem Complexity.FiniteAutomaton.CellNetwork.graph_terminal {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (t : Machine.Config w) (ht : M.transition t.2 (scanned w t.1) = none) (e : Edge Q w.length) : (graph M finish w).src e ≠ stateVertex w t

theorem Complexity.FiniteAutomaton.CellNetwork.scanned_outCell {Alpha : Type} (w : List Alpha) (s : Bool) : scanned w (outCell w.length s) = if s = true then Symbol.right else Symbol.left

theorem Complexity.FiniteAutomaton.CellNetwork.test_destination {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (s : Bool) : (graph M finish w).dst (Sum.inr (Sum.inr (s, testSlot M finish))) = stateVertex w (outCell w.length s, if s = true then finish else M.initial)

theorem Complexity.FiniteAutomaton.CellNetwork.test_step {Q Alpha : Type} (M : Machine Alpha Q) (finish : Q) (w : List Alpha) (s : Bool) : (graph M finish w).Step (Sum.inr (s, testSlot M finish)) (stateVertex w (outCell w.length s, if s = true then finish else M.initial))