One-way-liveness proof: RankLoss

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

Module and namespace names, imports, and formatting are adapted to complexitylib. The machine definitions are shared through Models.FiniteAutomaton.Defs.

def Complexity.FiniteAutomaton.rankLoss (h : ℕ) : ℕ

The exponential rank-loss threshold for relations on h points.

Equations

• Complexity.FiniteAutomaton.rankLoss h = 2 ^ ((h - 2) / 31)

def Complexity.FiniteAutomaton.RankLossAt (h : ℕ) : Prop

A simultaneous rank-loss bound for relation quotients with unit lifts.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.FiniteAutomaton.rank_drop_step {H A M : Type} [Fintype A] [Monoid M] [Finite M] (ρ : M →* Pairing (A ⊕ A)) (hρ : Function.Injective ⇑ρ) (φ : M →* BRel H) (hφ : Function.Surjective ⇑φ) (e : M) (he : e * e = e) (b : Corner e he) (hb : b * b = b) (P N : BRel H) (heP : φ e = P) (hbN : φ b.val = N) (F : Set H) [Fintype ↑F] (hF : BRel.restrictedId F * P * BRel.restrictedId F = BRel.restrictedId F) (hPN : P * N = N) (hNP : N * P = N) (x y : ↑F) (hxy : x ≠ y) (hN : ∀ (i j : ↑F), N.holds ↑i ↑j ↔ (BRel.addEdge x y).holds i j) (hIH : RankLossAt (Fintype.card ↑F)) : rankLoss (Fintype.card ↑F) ≤ 2 * ((ρ e).rank - (ρ b.val).rank)

One new relation pair forces the inductive rank loss, after two genuine corner reductions. The support budget loses only the factor two.

noncomputable def Complexity.FiniteAutomaton.RectangleFrame.deleted {H I J : Type} [Fintype I] [Fintype J] (F : RectangleFrame H I J) (i : I) (j : J) : Finset H

Frame vertices removed except for the selected row and column, together with the hub.

Equations

• F.deleted i j = Finset.image F.left (Finset.univ.erase i) ∪ Finset.image F.right (Finset.univ.erase j) ∪ {F.hub}

def Complexity.FiniteAutomaton.RectangleFrame.retained {H I J : Type} [Fintype I] [Fintype J] (F : RectangleFrame H I J) (i : I) (j : J) : Set H

The vertices that survive the frame deletion.

Equations

• F.retained i j = {x : H | x ∉ F.deleted i j}

theorem Complexity.FiniteAutomaton.RectangleFrame.deleted_card {H I J : Type} [Fintype I] [Fintype J] (F : RectangleFrame H I J) (i : I) (j : J) : (F.deleted i j).card = Fintype.card I - 1 + (Fintype.card J - 1) + 1

theorem Complexity.FiniteAutomaton.RectangleFrame.retained_card {H I J : Type} [Fintype I] [Fintype J] (F : RectangleFrame H I J) [Fintype H] (i : I) (j : J) : Fintype.card ↑(F.retained i j) = Fintype.card H - (Fintype.card I - 1 + (Fintype.card J - 1) + 1)

theorem Complexity.FiniteAutomaton.RectangleFrame.retained_ne_hub {H I J : Type} [Fintype I] [Fintype J] (F : RectangleFrame H I J) (i : I) (j : J) (x : H) (hx : x ∈ F.retained i j) : x ≠ F.hub

@[simp]

theorem Complexity.FiniteAutomaton.RectangleFrame.left_mem_retained {H I J : Type} [Fintype I] [Fintype J] (F : RectangleFrame H I J) (i k : I) (j : J) : F.left k ∈ F.retained i j ↔ k = i

@[simp]

theorem Complexity.FiniteAutomaton.RectangleFrame.right_mem_retained {H I J : Type} [Fintype I] [Fintype J] (F : RectangleFrame H I J) (i : I) (j k : J) : F.right k ∈ F.retained i j ↔ k = j

theorem Complexity.FiniteAutomaton.RectangleFrame.old_avoids_retained {H I J : Type} [Fintype I] [Fintype J] (F : RectangleFrame H I J) {E : Set (I × J)} {i : I} {j : J} (h : (i, j) ∉ E) (p : I × J) : p ∈ E → F.left p.1 ∉ F.retained i j ∨ F.right p.2 ∉ F.retained i j

theorem Complexity.FiniteAutomaton.RectangleFrame.exists_frame {H : Type} [Fintype H] (h : 33 ≤ Fintype.card H) : Nonempty (RectangleFrame H (Fin 16) (Fin 16))

theorem Complexity.FiniteAutomaton.rectangle_chain {H A M I J : Type} [Fintype H] [Fintype A] [Fintype I] [Fintype J] [Monoid M] [Finite M] (ρ : M →* Pairing (A ⊕ A)) (hρ : Function.Injective ⇑ρ) (φ : M →* BRel H) (hφ : Function.Surjective ⇑φ) (F : RectangleFrame H I J) (L : ℕ) (hL : ∀ (i : I) (j : J), rankLoss (Fintype.card ↑(F.retained i j)) = L) (hIH : ∀ (i : I) (j : J), RankLossAt (Fintype.card ↑(F.retained i j))) (e : M) (he : e * e = e) (heφ : φ e = F.base) (g : I × J → Corner e he) (hg : ∀ (p : I × J), φ (g p).val = F.rel {p}) (K : Finset ↥(ρ e).lefts) (hgK : ∀ (p : I × J), ((Pairing.reduceHom ρ e he) (g p)).support ⊆ K) (E : Finset (I × J)) : ∃ (b : Corner e he), b * b = b ∧ φ b.val = F.rel ↑E ∧ ((Pairing.reduceHom ρ e he) b).support ⊆ K ∧ E.card * L ≤ 2 * ((ρ e).rank - (ρ b.val).rank)

theorem Complexity.FiniteAutomaton.rankLoss_recurrence {h : ℕ} (hh : 33 ≤ h) : rankLoss h = 2 * rankLoss (h - 31)

theorem Complexity.FiniteAutomaton.rankLoss_all (h : ℕ) : RankLossAt h

Exponential rank loss by 256-addition amplification, simultaneously in the relation alphabet and the ambient diagram degree.

def Complexity.FiniteAutomaton.Corner.oneEquiv {M : Type u_1} [Monoid M] : Corner 1 ⋯ ≃* M

The corner at the identity is equivalent to the original monoid.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.FiniteAutomaton.relation_divisor_degree {H A M : Type} [Fintype H] [Fintype A] [Monoid M] [Finite M] (ρ : M →* Pairing (A ⊕ A)) (hρ : Function.Injective ⇑ρ) (φ : M →* BRel H) (hφ : Function.Surjective ⇑φ) (x y : H) (hxy : x ≠ y) : rankLoss (Fintype.card H) ≤ Fintype.card A

No permutation-lift hypothesis remains in the divisor degree bound.