Two-way complementation: tape

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

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

theorem Complexity.FiniteAutomaton.Complementation.Internal.chainSymbol_getElem {Sigma : Type u_1} {m : ℕ} (w : List Sigma) (last : Sigma) (c : ChainNode m w.length) : chainSymbol w last c = (w ++ [last])[c.position]

Chain symbols agree with ordinary zero-based lookup of the nonempty symbol list.

theorem Complexity.FiniteAutomaton.Complementation.Internal.marked_getElem {Sigma : Type u_1} (w : List Sigma) (p : Fin (w.length + 2)) : (Sum.inl 0 :: (List.map Sum.inr w ++ [Sum.inl 1]))[↑p] = tapeSymbol w p

Lookup of the explicitly marked list agrees with the automaton's tape lookup.

noncomputable def Complexity.FiniteAutomaton.Complementation.Internal.ChainNode.exitEquiv (m n : ℕ) : ChainNode m n ⊕ Fin m ≃ Fin m × Fin (n + 2)

Convert the recursively joined cells and one terminal exit into tape coordinates.

Equations

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

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_equiv_iff {V : Type u_1} {W : Type u_2} (e : V ≃ W) (R : SetRel V V) (S : SetRel W W) (h : ∀ (x y : V), (e x, e y) ∈ S ↔ (x, y) ∈ R) (x y : V) : (e x, e y) ∈ relStar S ↔ (x, y) ∈ relStar R

A graph equivalence transports finite paths in both directions.

theorem Complexity.FiniteAutomaton.Complementation.Internal.blockRelation_terminal {V : Type u_1} {Q : Type u_2} (E : SetRel V V) (O : SetRel V Q) (c : V) (q : Q) : (Sum.inl c, Sum.inr q) ∈ relStar (blockRelation E O ∅ ∅) ↔ (c, q) ∈ (relStar E).comp O

A terminal block with no outgoing edges is reached by an internal path and one exit.

theorem Complexity.FiniteAutomaton.Complementation.Internal.chainSymbol_position {Sigma : Type u_1} {m : ℕ} (w : List Sigma) (last : Sigma) (c d : ChainNode m w.length) (hp : c.position = d.position) : chainSymbol w last c = chainSymbol w last d

A cell's scanned symbol depends only on its position.

def Complexity.FiniteAutomaton.Complementation.Internal.chainStep {Sigma : Type u_1} {m : ℕ} (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma) : SetRel (Fin m × Fin (w.length + 2)) (Fin m × Fin (w.length + 2))

Local moves on the bounded tape, with a final terminal position beyond the last cell.

Equations

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

theorem Complexity.FiniteAutomaton.Complementation.Internal.chainStep_exitEquiv {Sigma : Type u_1} {m : ℕ} (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma) (x y : ChainNode m w.length ⊕ Fin m) : ((ChainNode.exitEquiv m w.length) x, (ChainNode.exitEquiv m w.length) y) ∈ chainStep moves w last ↔ (x, y) ∈ blockRelation (chainNetwork moves w last).edge (chainNetwork moves w last).rightOut ∅ ∅

The joined network with terminal exits has exactly the bounded tape's local edges.

theorem Complexity.FiniteAutomaton.Complementation.Internal.chainStep_recognition {Sigma : Type u_1} {m : ℕ} (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma) (q r : Fin m) : ((q, ⟨0, ⋯⟩), r, ⟨w.length + 1, ⋯⟩) ∈ relStar (chainStep moves w last) ↔ (q, r) ∈ (chainNetwork moves w last).summary.forward

The designated forward edge of a diagram product is exactly a successful tape run.