One-way-liveness proof: Main

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

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

theorem Complexity.FiniteAutomaton.oneWayLiveness_state_bounds_proof (h : ℕ) (hh : 2 ≤ h) : (∃ (N : NMachine (Alphabet h) (h + 3)), N.NoLeft ∧ ∀ (positive : Bool), N.Recognizes positive (oneWayLiveness h)) ∧ ∀ (positive : Bool) (s : ℕ) (D : DMachine (Alphabet h) s), D.Recognizes positive (oneWayLiveness h) → 2 ^ ((h - 2) / 31) ≤ 4 * (s + if positive = true then 2 else 1) ^ 2

The one-way nondeterministic upper bound and two-way deterministic lower bound, under both acceptance conventions.

theorem Complexity.FiniteAutomaton.no_oneWay_polynomial_simulation_proof (positive : Bool) : ¬OneWayPolynomialSimulation positive

No alphabet-independent polynomial deterministic simulation exists, under either acceptance convention.