Two-way complementation: image bound

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/TwoWayAutomata/ImageBound.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.single_edge_cost (h : ℕ) {A : Type u} {H : Type v} [Monoid A] [Finite A] [Finite H] {m : ℕ} : Nat.card H = h → 2 ≤ h → ∀ (ι : A →ₙ* Diagram m) (φ : A →* RelationMonoid H), Function.Surjective ⇑φ → (∀ (a b : A), (ι a, ι b) ∈ Diagram.inclusion m → (φ b).toRel ⊆ (φ a).toRel) → (∀ (σ : Equiv.Perm H), ∃ (p : Aˣ), φ ↑p = ↑(permutationUnit σ)) → ∀ (a : A), IsIdempotentElem a → ∀ (x y : H), x ≠ y → (φ a).toRel = SetRel.id ∪ {(x, y)} → lossBound h ≤ ((ι 1).missing (ι a)).ncard

Exponential cost of a single edge for every finite source monoid and label type.

theorem Complexity.FiniteAutomaton.Complementation.Internal.minimal_unital_corner {A : Type u_1} {M : Type u_2} [Semigroup A] [Finite A] [Monoid M] (θ : A →ₙ* M) (hθ : Function.Surjective ⇑θ) : ∃ (d : A) (hd : IsIdempotentElem d) (ψ : hd.Corner →* M), Function.Surjective ⇑ψ ∧ (∀ (w : hd.Corner), ψ w = θ ↑w) ∧ ∀ (u : Mˣ), ∃ (p : hd.Cornerˣ), ψ ↑p = ↑u

A surjection has a unital identity corner with unit lifts for every target unit.

theorem Complexity.FiniteAutomaton.Complementation.Internal.identity_pair_idempotent {H : Type u_1} (x y : H) : IsIdempotentElem (RelationMonoid.ofRel (SetRel.id ∪ {(x, y)}))

Identity plus a single pair is always an idempotent relation.

theorem Complexity.FiniteAutomaton.Complementation.Internal.order_reversing_image_bound_finite {H : Type u_1} [Finite H] (m : ℕ) (_hm : 1 ≤ m) (hh : 2 ≤ Nat.card H) (S : Set (Diagram m)) (hidentity : Diagram.identity m ∈ S) (hclosed : ∀ ⦃a b : Diagram m⦄, a ∈ S → b ∈ S → a.comp b ∈ S) (φ : ↑S → SetRel H H) (hsurj : Function.Surjective φ) (hmul : ∀ (a b : ↑S), φ ⟨(↑a).comp ↑b, ⋯⟩ = (φ a).comp (φ b)) (hreverse : ∀ (a b : ↑S), (↑a, ↑b) ∈ Diagram.inclusion m → φ b ⊆ φ a) : lossBound (Nat.card H) ≤ 2 * m

A surjective order-reversing multiplicative image has exponential cost.

theorem Complexity.FiniteAutomaton.Complementation.Internal.order_reversing_image_bound (m h : ℕ) (_hm : 1 ≤ m) (hh : 2 ≤ h) (S : Set (Diagram m)) (hidentity : Diagram.identity m ∈ S) (hclosed : ∀ ⦃a b : Diagram m⦄, a ∈ S → b ∈ S → a.comp b ∈ S) (φ : ↑S → SetRel (Fin h) (Fin h)) (hsurj : Function.Surjective φ) (hmul : ∀ (a b : ↑S), φ ⟨(↑a).comp ↑b, ⋯⟩ = (φ a).comp (φ b)) (hreverse : ∀ (a b : ↑S), (↑a, ↑b) ∈ Diagram.inclusion m → φ b ⊆ φ a) : lossBound h ≤ 2 * m

The order-reversing image bound for a finite label domain.