Word encodings preserve the complementation lower bound

Feed the diagram of each encoded word into OpenAI's order-reversing relation image theorem. Code lengths do not enter the state bound. The existing binary liveness NFA then gives a fixed-alphabet lower bound for the full complement language, and exponential growth rules out a polynomial complementation bound.

def Complexity.FiniteAutomaton.Complementation.Internal.fromSetRel {H : Type} (R : SetRel H H) : BRel H

Curried form of a binary relation.

Equations

• Complexity.FiniteAutomaton.Complementation.Internal.fromSetRel R = { holds := fun (x y : H) => (x, y) ∈ R }

theorem Complexity.FiniteAutomaton.Complementation.Internal.fromSetRel_product {H : Type} (w : List (SetRel H H)) : (List.map fromSetRel w).prod = fromSetRel (relationProduct w)

theorem Complexity.FiniteAutomaton.Complementation.Internal.live_map_fromSetRel {H : Type} (w : List (SetRel H H)) : BRel.Live (List.map fromSetRel w) ↔ Set.Nonempty (relationProduct w)

theorem Complexity.FiniteAutomaton.Complementation.Internal.encoded_complement_lower_bound {Alpha : Type} (h : ℕ) (hh : 2 ≤ h) (code : Alphabet h → List Alpha) (s : ℕ) (M : NMachine Alpha s) (hM : ∀ (w : List (Alphabet h)), M.Accepts false (List.flatMap code w) ↔ w ∉ oneWayLiveness h) : 2 ^ ((h - 2) / 127) ≤ 2 * (s + 1)

theorem Complexity.FiniteAutomaton.Complementation.Internal.binary_complement_lower_bound (n s : ℕ) (M : NMachine Bool s) (hM : M.Recognizes false (binaryLivenessNFA n).acceptsᶜ) : 2 ^ (n / 127) ≤ 2 * (s + 1)

theorem Complexity.FiniteAutomaton.Complementation.Internal.liveness_complement_lower_bound (h : ℕ) (hh : 2 ≤ h) (s : ℕ) (M : NMachine (Alphabet h) s) (hM : M.Recognizes false (livenessNFA h).acceptsᶜ) : 2 ^ ((h - 2) / 127) ≤ 2 * (s + 1)

theorem Complexity.FiniteAutomaton.Complementation.Internal.no_binary_polynomial_complementation : ¬∃ (p : Polynomial ℝ), ∀ (Q : Type) [inst : Fintype Q] (A : NFA Bool Q), ∃ (s : ℕ) (M : NMachine Bool s), M.Recognizes false A.acceptsᶜ ∧ ↑s ≤ Polynomial.eval (↑(Fintype.card Q)) p