One-way-liveness proof: Recognition

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

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

theorem Complexity.FiniteAutomaton.scanned_list {Alpha : Type} (w : List Alpha) : List.ofFn (scanned w) = Symbol.left :: (List.map Symbol.letter w ++ [Symbol.right])

The scanned cells are the two fixed markers surrounding the ordinary word.

theorem Complexity.FiniteAutomaton.CellNetwork.fullDiagram_markers {Alpha Q : Type} [Fintype Q] (M : Machine Alpha Q) (finish : Q) (w : List Alpha) : fullDiagram M finish w = bodyDiagram M finish Symbol.left * (List.map (fun (a : Alpha) => bodyDiagram M finish (Symbol.letter a)) w).prod * bodyDiagram M finish Symbol.right

noncomputable def Complexity.FiniteAutomaton.CellNetwork.recognitionTest {Alpha Q : Type} [Fintype Q] (M : Machine Alpha Q) (finish : Q) (a : Pairing (Port Q ⊕ Port Q)) : Prop

A diagram accepts when no compatible coloring separates its test ports.

Equations

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

theorem Complexity.FiniteAutomaton.CellNetwork.recognitionTest_iff {Alpha Q : Type} [Fintype Q] (M : Machine Alpha Q) (finish : Q) (ht : M.transition finish Symbol.right = none) (w : List Alpha) : recognitionTest M finish (List.map (fun (a : Alpha) => bodyDiagram M finish (Symbol.letter a)) w).prod ↔ Relation.ReflTransGen (M.Step w) (outCell w.length false, M.initial) (outCell w.length true, finish)

theorem Complexity.FiniteAutomaton.Machine.liveness_rank_bound {H Q : Type} [Fintype H] [Fintype Q] (M : Machine (BRel H) Q) (hM : ∀ (w : List (BRel H)), M.Accepts false w ↔ BRel.Live w) (x y : H) (hxy : x ≠ y) : rankLoss (Fintype.card H) ≤ 4 * (Fintype.card Q + 1) ^ 2

theorem Complexity.FiniteAutomaton.deterministic_lower_bound (h : ℕ) (hh : 2 ≤ h) (positive : Bool) (s : ℕ) (D : DMachine (Alphabet h) s) (hD : D.Recognizes positive (oneWayLiveness h)) : 2 ^ ((h - 2) / 31) ≤ 4 * (s + if positive = true then 2 else 1) ^ 2

The representation uses four ports per ordered state pair. One sink state suffices under reflexive acceptance; a fresh initial row handles positive runs.