Two-way complementation: retained

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/TwoWayAutomata/Retained.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.exists_hub_families {H : Type u_1} [Finite H] (hh : 129 ≤ Nat.card H) : ∃ (u : Fin 64 ↪ H) (v : Fin 64 ↪ H) (z : H), (∀ (i j : Fin 64), u i ≠ v j) ∧ (∀ (i : Fin 64), u i ≠ z) ∧ ∀ (j : Fin 64), v j ≠ z

Select the two 64-point families and a distinct hub.

theorem Complexity.FiniteAutomaton.Complementation.Internal.retained_pair_set {H : Type u_1} [Finite H] (U V : Set H) (hU : U.ncard = 64) (hV : V.ncard = 64) (hUV : Disjoint U V) (z x y : H) (hzU : z ∉ U) (hzV : z ∉ V) (hx : x ∈ U) (hy : y ∈ V) : ∃ (F : Set H), Nat.card ↑F = Nat.card H - 127 ∧ x ∈ F ∧ y ∈ F ∧ z ∉ F ∧ (∀ a ∈ U, a ∈ F → a = x) ∧ ∀ b ∈ V, b ∈ F → b = y

Retaining a new pair and all external points removes exactly 127 points.

theorem Complexity.FiniteAutomaton.Complementation.Internal.mem_restricted_sandwich {H : Type u_1} (F : Set H) (R : SetRel H H) (a b : H) : (a, b) ∈ ((restrictedIdentity F).comp R).comp (restrictedIdentity F) ↔ a ∈ F ∧ b ∈ F ∧ (a, b) ∈ R

Identity sandwiches restrict exactly the two endpoints.

theorem Complexity.FiniteAutomaton.Complementation.Internal.retained_relation_identity {H : Type u_1} (U V F : Set H) (z x y : H) (hz : z ∉ F) (hx : ∀ a ∈ U, a ∈ F → a = x) (hy : ∀ b ∈ V, b ∈ F → b = y) (E : SetRel H H) (hE : E ⊆ U ×ˢ V) (hnew : (x, y) ∉ E) : ((restrictedIdentity F).comp (restrictedIdentity {a : H | a ≠ z} ∪ E)).comp (restrictedIdentity F) = restrictedIdentity F

Before its turn, the selected pair is absent from the retained restriction.

theorem Complexity.FiniteAutomaton.Complementation.Internal.retained_relation_pair {H : Type u_1} (P : SetRel H H) (F : Set H) (hP : ((restrictedIdentity F).comp P).comp (restrictedIdentity F) = restrictedIdentity F) (x y : H) (hx : x ∈ F) (hy : y ∈ F) : ((restrictedIdentity F).comp (P ∪ {(x, y)})).comp (restrictedIdentity F) = restrictedIdentity F ∪ {(x, y)}

At its turn, restriction adds precisely the selected pair to the retained identity.

theorem Complexity.FiniteAutomaton.Complementation.Internal.lossBound_step {h : ℕ} (hh : 129 ≤ h) : lossBound h = 2 * lossBound (h - 127)

The target doubles whenever the induction removes 127 points.

theorem Complexity.FiniteAutomaton.Complementation.Internal.amplification_arithmetic {h c : ℕ} (hh : 129 ≤ h) (δ : Fin 4096 → ℕ) (htotal : ∑ j : Fin 4096, δ j ≤ 1024 * c) (hstep : ∀ (j : Fin 4096), lossBound (h - 127) ≤ 2 * δ j) : lossBound h ≤ c

The numerical conclusion of summing the 4096 inductive lower bounds.

theorem Complexity.FiniteAutomaton.Complementation.Internal.single_edge_base {A : Type u_1} {H : Type u_2} [Monoid A] {m : ℕ} (ι : A →ₙ* Diagram m) (φ : A →* RelationMonoid H) (hreverse : ∀ (a b : A), (ι a, ι b) ∈ Diagram.inclusion m → (φ b).toRel ⊆ (φ a).toRel) (a : A) (x y : H) (hxy : x ≠ y) (himage : (φ a).toRel = SetRel.id ∪ {(x, y)}) (hh : Nat.card H ≤ 128) : lossBound (Nat.card H) ≤ ((ι 1).missing (ι a)).ncard

The base case detects the off-diagonal pair using rectangle coverage and order reversal.

theorem Complexity.FiniteAutomaton.Complementation.Internal.sandwich_power_absorption {A : Type u_1} [Monoid A] (b a : A) (hb : IsIdempotentElem b) (k : ℕ) : b * (b * a * b) ^ (k + 1) = (b * a * b) ^ (k + 1) ∧ (b * a * b) ^ (k + 1) * b = (b * a * b) ^ (k + 1)

Every positive power of a sandwich is absorbed by its idempotent outer factor.