Documentation

Complexitylib.Models.FiniteAutomaton.Complementation.Internal.Amplification

Two-way complementation: amplification #

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

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

source
def Complexity.FiniteAutomaton.Complementation.Internal.lossBound (h : ℕ) :
ℕ

The exponential lower bound for 2 ≤ h.

Equations
Instances For
    source
    theorem Complexity.FiniteAutomaton.Complementation.Internal.map_identity_corner {A : Type u_1} [Monoid A] {m : ℕ} (ι : A →ₙ* Diagram m) (a : A) :
    ι a ∈ (ι 1).corner

    The image of a monoid lies in the diagram corner of its image identity.

    source
    theorem Complexity.FiniteAutomaton.Complementation.Internal.missing_context_card {m : ℕ} (e d u v z : Diagram m) (he : e.comp e = e) (hd : d.comp d = d) (hcontext : (u.comp e).comp v = d) (hz : z ∈ e.corner) (hnew : (u.comp z).comp v ∈ d.corner) :
    (d.missing ((u.comp z).comp v)).ncard ≤ 2 * (e.missing z).ncard

    The cardinality consequence of the uniform transport theorem.

    source
    theorem Complexity.FiniteAutomaton.Complementation.Internal.conjugate_missing_bound {A : Type u_1} [Monoid A] {m : ℕ} (ι : A →ₙ* Diagram m) (p : Aˣ) (a : A) :
    ((ι 1).missing (ι (↑p * a * ↑p⁻¹))).ncard ≤ 2 * ((ι 1).missing (ι a)).ncard

    Conjugating by a unit costs at most twice as many missing classes.

    source
    theorem Complexity.FiniteAutomaton.Complementation.Internal.common_pair_budget {A : Type u_1} [Monoid A] {m t c : ℕ} (ι : A →ₙ* Diagram m) (f : Bool × Fin t → A) (b0 : A) (hb0 : IsIdempotentElem b0) (hcost : ∀ (p : Bool × Fin t), ((ι 1).missing (ι (f p))).ncard ≤ 2 * c) :
    ∃ J0 ⊆ (ι b0).classes, J0.ncard ≤ 8 * t * c ∧ ∀ (i j : Fin t), (ι b0).missing (ι (b0 * f (false, i) * f (true, j) * b0)) ⊆ J0

    All pair products share one missing-set bound after sandwiching by an idempotent.

    source
    theorem Complexity.FiniteAutomaton.Complementation.Internal.bipartite_relation_comp {H : Type u_1} (F U V : Set H) (hU : U ⊆ F) (hV : V ⊆ F) (hUV : Disjoint U V) (E E' : SetRel H H) (hE : E ⊆ U ×ˢ V) (hE' : E' ⊆ U ×ˢ V) :
    (restrictedIdentity F ∪ E).comp (restrictedIdentity F ∪ E') = restrictedIdentity F ∪ (E ∪ E')

    Disjoint source and target sets prevent two added edges from being concatenated.

    source
    theorem Complexity.FiniteAutomaton.Complementation.Internal.hub_pair_relation {H : Type u_1} (u v z : H) (huz : u ≠ z) (hvz : v ≠ z) :
    (((restrictedIdentity {x : H | x ≠ z}).comp (SetRel.id ∪ {(u, z)})).comp (SetRel.id ∪ {(z, v)})).comp (restrictedIdentity {x : H | x ≠ z}) = restrictedIdentity {x : H | x ≠ z} ∪ {(u, v)}

    Removing the hub leaves exactly the desired pair between its two neighbours.

    source
    def Complexity.FiniteAutomaton.Complementation.Internal.permutationUnit {H : Type u_1} (σ : Equiv.Perm H) :
    (RelationMonoid H)ˣ

    A permutation and its inverse form a unit in the full relation monoid.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Complexity.FiniteAutomaton.Complementation.Internal.permutation_conjugate_relation {H : Type u_1} (σ : Equiv.Perm H) (R : SetRel H H) :
      ((Function.graph ⇑σ).comp R).comp (Function.graph ⇑(Equiv.symm σ)) = {xy : H × H | (σ xy.1, σ xy.2) ∈ R}

      Permutation conjugation relabels both endpoints of every relation edge.

      source
      theorem Complexity.FiniteAutomaton.Complementation.Internal.pair_conjugate {A : Type u_1} {H : Type u_2} [Monoid A] {m : ℕ} (ι : A →ₙ* Diagram m) (φ : A →* RelationMonoid H) (hlift : ∀ (σ : Equiv.Perm H), ∃ (p : Aˣ), φ ↑p = ↑(permutationUnit σ)) (a : A) (ha : IsIdempotentElem a) (x y : H) (hxy : x ≠ y) (himage : (φ a).toRel = SetRel.id ∪ {(x, y)}) (u v : H) (huv : u ≠ v) :
      ∃ (s : A), IsIdempotentElem s ∧ (φ s).toRel = SetRel.id ∪ {(u, v)} ∧ ((ι 1).missing (ι s)).ncard ≤ 2 * ((ι 1).missing (ι a)).ncard

      Unit lifts move the initial added pair to any other ordered pair of distinct points.

      source
      theorem Complexity.FiniteAutomaton.Complementation.Internal.smaller_relation_instance {A : Type u_1} {H : Type u_2} [Monoid A] [Finite A] {m : ℕ} (ι : A →ₙ* Diagram m) (φ : A →* RelationMonoid H) (hφ : Function.Surjective ⇑φ) (b b' : A) (hb : IsIdempotentElem b) (hbb' : b * b' = b') (hb'b : b' * b = b') (F : Set H) (hiPi : ((restrictedIdentity F).comp (φ b).toRel).comp (restrictedIdentity F) = restrictedIdentity F) (x y : ↑F) (hpair : ((restrictedIdentity F).comp (φ b').toRel).comp (restrictedIdentity F) = restrictedIdentity F ∪ {(↑x, ↑y)}) :
      ∃ (d : hb.Corner) (hd : IsIdempotentElem d) (ψ : hd.Corner →* RelationMonoid ↑F), Function.Surjective ⇑ψ ∧ (∀ (σ : Equiv.Perm ↑F), ∃ (p : hd.Cornerˣ), ψ ↑p = ↑(permutationUnit σ)) ∧ (∀ (w : hd.Corner), (ψ w).toRel = {xy : ↑F × ↑F | (↑xy.1, ↑xy.2) ∈ (φ ↑↑w).toRel}) ∧ ∃ (v : hd.Corner), IsIdempotentElem v ∧ (ψ v).toRel = SetRel.id ∪ {(x, y)} ∧ ((ι ↑d).missing (ι ↑↑v)).ncard ≤ 2 * ((ι b).missing (ι b')).ncard

      Restricting an idempotent sandwich preserves the new pair and supplies all unit lifts.