Two-way complementation: main

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/TwoWayAutomata/Main.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.complementation_lower_bound (n : ℕ) (hn : 4 ≤ n) : ∃ (A : TwoNFA (SetRel (Fin (n - 2)) (Fin (n - 2))) (Fin n)), ∀ (s : ℕ) (B : TwoNFA (SetRel (Fin (n - 2)) (Fin (n - 2))) (Fin s)), B.language = A.languageᶜ → 2 ^ ((n - 4) / 127) ≤ 2 * (s + 1)

An n-state source language requires exponentially many states for any 2NFA complement.

theorem Complexity.FiniteAutomaton.Complementation.Internal.complementation_lower_bound_finite (n : ℕ) (hn : 4 ≤ n) : ∃ (A : TwoNFA (SetRel (Fin (n - 2)) (Fin (n - 2))) (Fin n)), ∀ (Q : Type u_1) [inst : Fintype Q] (B : TwoNFA (SetRel (Fin (n - 2)) (Fin (n - 2))) Q), B.language = A.languageᶜ → 1 / 2 * 2 ^ ((n - 4) / 127) - 1 ≤ ↑(Fintype.card Q)

The real-valued lower bound for arbitrary finite target state sets.

theorem Complexity.FiniteAutomaton.Complementation.Internal.tapeSymbol_map {Sigma : Type u_1} {Gamma : Type u_2} (f : Sigma → Gamma) (w : List Sigma) (p : Fin (w.length + 2)) : tapeSymbol (List.map f w) ⟨↑p, ⋯⟩ = Sum.map id f (tapeSymbol w p)

Letter maps commute with tape lookup and preserve the two endmarkers.

def Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.pullAlphabet {Sigma : Type u_1} {Gamma : Type u_2} {Q : Type u_3} (A : TwoNFA Gamma Q) (f : Sigma → Gamma) : TwoNFA Sigma Q

Pull an automaton back along a letter map, preserving its state set.

Equations

• A.pullAlphabet f = { initial := A.initial, accepting := A.accepting, transition := fun (q : Q) (symbol : Fin 2 ⊕ Sigma) => A.transition q (Sum.map id f symbol) }

theorem Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.pullAlphabet_language {Sigma : Type u_1} {Gamma : Type u_2} {Q : Type u_3} (A : TwoNFA Gamma Q) (f : Sigma → Gamma) (w : List Sigma) : w ∈ (A.pullAlphabet f).language ↔ List.map f w ∈ A.language

Letter pullback accepts exactly the words whose images the original machine accepts.

theorem Complexity.FiniteAutomaton.Complementation.Internal.polynomial_not_bound_two_pow (p : Polynomial ℝ) : ¬∀ (n : ℕ), 2 ^ n ≤ Polynomial.eval (↑n) p

No real polynomial bounds the powers of two at all natural inputs.

theorem Complexity.FiniteAutomaton.Complementation.Internal.no_polynomial_complementation : ¬∃ (p : Polynomial ℝ), ∀ (n k : ℕ) (A : TwoNFA (Fin k) (Fin n)), ∃ (s : ℕ) (B : TwoNFA (Fin k) (Fin s)), B.language = A.languageᶜ ∧ ↑s ≤ Polynomial.eval (↑n) p

There is no polynomial state bound for complementation over all finite alphabets.