One-way-liveness proof: Syntactic

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

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

theorem Complexity.FiniteAutomaton.BRel.singleton_context {H : Type u_1} (a : BRel H) (i j : H) : (∃ (x : H) (y : H), (restrictedId {i} * a * restrictedId {j}).holds x y) ↔ a.holds i j

theorem Complexity.FiniteAutomaton.BRel.context_separates {H : Type u_1} (u v : List (BRel H)) (h : ∀ (x y : List (BRel H)), Live (x ++ u ++ y) ↔ Live (x ++ v ++ y)) : u.prod = v.prod

theorem Complexity.FiniteAutomaton.matching_recognition_degree {H A : Type} [Fintype H] [Fintype A] (η : BRel H → Pairing (A ⊕ A)) (test : Pairing (A ⊕ A) → Prop) (hη : ∀ (w : List (BRel H)), test (List.map η w).prod ↔ BRel.Live w) (x y : H) (hxy : x ≠ y) : rankLoss (Fintype.card H) ≤ Fintype.card A

Any matching recognition of liveness induces the full relation divisor. The recognizer predicate may in particular sandwich the fixed endmarkers and inspect the designated test ports.