FiberEnergyLemmas.lean`

54 declarations, 0 contain sorry, 0 declared as axioms

Energy after merging a bounded number of frequencies

This finite ordered-ring theorem supplies the Cauchy–Schwarz step in (A.10). Its fiber-cardinality hypothesis is explicit.

theorem OAI.UniqueGamesTheorem.Appendix.FiberEnergy.finite_fiber_energy line 30

Source documentation

The energy of a sum of merged coefficients is bounded by the largest fiber size times the original coefficient energy. Signs and cancellations are unrestricted; no injectivity assumption is made.

theorem finite_fiber_energy (s : Finset α) (compress : α → β) (a : α → R)
    (bound : R) (hbound : ∀ z,
      ((s.filter (fun y => compress y = z)).card : R) ≤ bound) :
    (∑ z, (∑ y ∈ s.filter (fun y => compress y = z), a y) ^ 2) ≤
      bound * ∑ y ∈ s, a y ^ 2 := by
…

theorem OAI.UniqueGamesTheorem.Appendix.F1Gram.gram_energy_le line 64
Source documentation
The squared entries of a Gram matrix are bounded by the squared total energy of its underlying rows. This is a pairwise Cauchy–Schwarz argument.
```
theorem gram_energy_le {R C : Type*} [Fintype R] [Fintype C] (p : R → C → ℝ) :
    (∑ r, ∑ s, (∑ c, p r c * p s c)^2) ≤
      (∑ r, ∑ c, p r c^2)^2 := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.F1Gram.sum_subtype_eq line 79
theorem OAI.UniqueGamesTheorem.Appendix.F1Gram.sum_comp_le line 96

theorem OAI.UniqueGamesTheorem.Appendix.Induction.outer_order_cutoff line 115

Source documentation

The corrected outer-order cutoff (A.14), with natural subtraction explicit.

theorem outer_order_cutoff (d i j k a b : Nat)
    (ha : i + k ≤ a) (hb : j + k ≤ b) (ht : i + j + k ≤ d)
    (ho : (a - i - k) + (b - j - k) ≤ d - (i + j + k)) :
    a + b ≤ d + k := by
…

theorem OAI.UniqueGamesTheorem.Appendix.Induction.complement_dimension_bounds line 122
Source documentation
Each complementary-space dimension is at most the original degree.
```
theorem complement_dimension_bounds (d i j k a b : Nat)
    (ha : i + k ≤ a) (hb : j + k ≤ b) (h : a + b ≤ d + k) :
    a - i ≤ d ∧ b - j ≤ d := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Induction.recombined_order_cutoff line 128
Source documentation
Recombination preserves the required derivative degree cutoff.
```
theorem recombined_order_cutoff (d k a b : Nat)
    (ha : k ≤ a) (hb : k ≤ b) (h : a + b ≤ d + k) :
    (a - k) + (b - k) + k ≤ d := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Induction.square_remainder_budget line 133
theorem OAI.UniqueGamesTheorem.Appendix.Induction.induction_exponent_budget line 144
Source documentation
The exponent inequality preceding (A.16), with negative exponents moved to the left side so natural subtraction cannot hide an invalid inequality.
```
theorem induction_exponent_budget (d t k : Nat) (ht : t ≤ d) (hk : k ≤ t) :
    100 * ((d - t) * (d - t)) + 27 * (d * t) + 6 * (d * k) +
      63 * (d * t) + 4 * (d * k) ≤ 100 * (d * d) := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Induction.antecedent_exponent_budget line 151
theorem OAI.UniqueGamesTheorem.Appendix.Induction.first_triangle_exponent_budget line 162
Source documentation
The factor from the fourth-power triangle inequality fits inside the 12d(i+j) budget used before (A.13).
```
theorem first_triangle_exponent_budget (d i j : Nat) (hi : i ≤ d) :
    7 * (d * (i + j)) + 3 * (i * j) ≤ 12 * (d * (i + j)) := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Induction.initial_order_bound line 169
Source documentation
The derivative order t is at least half the original pair order.
```
theorem initial_order_bound (i j k : Nat) (hi : k ≤ i) (hj : k ≤ j) :
    i + j ≤ 2 * (i + j - k) := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Induction.positive_rank_geometric_slack line 174
Source documentation
For positive k the geometric-series exponent has at least d of slack.
```
theorem positive_rank_geometric_slack (d k : Nat) (hk : 1 ≤ k) :
    31 * (d * (k + 1)) + d ≤ 63 * (d * k) := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Induction.corrected_weight_exponent line 181
Source documentation
The rank-dependent decay in (A.16) contains the corrected 8dk weight.
```
theorem corrected_weight_exponent (d k : Nat) :
    31 * (d * (k + 1)) + 4 * (d * k) =
      31 * d + 27 * (d * k) + 8 * (d * k) := by
…
```

theorem OAI.UniqueGamesTheorem.Appendix.Induction.extension_unique line 190

Source documentation

When B′ plus the prescribed kernel spans the domain, the map on B′ determines its extension. Thus fixing image and kernel in the antecedent count leaves no additional induced-isomorphism choice.

theorem extension_unique {B V : Type} [Add B] [Add V]
    (zero : V) (X₁ X₂ : B → V) (B' K : B → Prop)
    (right_zero : ∀ v : V, v + zero = v)
    (add₁ : ∀ x y, X₁ (x + y) = X₁ x + X₁ y)
    (add₂ : ∀ x y, X₂ (x + y) = X₂ x + X₂ y)
    (span : ∀ x, ∃ b z, B' b ∧ K z ∧ x = b + z)
    (agree : ∀ b, B' b → X₁ b = X₂ b)
    (kill₁ : ∀ z, K z → X₁ z = zero)
    (kill₂ : ∀ z, K z → X₂ z = zero) : X₁ = X₂ := by
…

def OAI.UniqueGamesTheorem.Appendix.Level.rankFilter line 214
Source documentation
The unselected multiplier in factored form, after multiplying numerator and denominator by 2^(2*r). Selected characters have multiplier one.
```
def rankFilter (d r : Nat) (selected : Bool) : Rat :=
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Level.filter_polynomial_algebra line 218
theorem OAI.UniqueGamesTheorem.Appendix.Level.rankFilter_selected line 222
theorem OAI.UniqueGamesTheorem.Appendix.Level.rankFilter_zero_at_d line 225
theorem OAI.UniqueGamesTheorem.Appendix.Level.rankFilter_zero_at_pred line 229
theorem OAI.UniqueGamesTheorem.Appendix.Level.only_two_source_ranks line 235
Source documentation
Only ranks d-1 and d can restrict to rank d-1; no degree bound on the original function is needed.
```
theorem only_two_source_ranks {d r s : Nat} (hd : 1 ≤ d)
    (hlo : s ≤ r) (hhi : r ≤ s + 1) (hs : s + 1 = d) :
    r = d ∨ r = d - 1 := by
…
```

theorem OAI.UniqueGamesTheorem.Appendix.Level.rank_filter_character line 242

Source documentation

Selected characters lose exactly one rank. On an unselected character, the two roots of the filter remove every possible unwanted contribution.

theorem rank_filter_character {d r s : Nat} (hd : 1 ≤ d)
    (selected : Bool) (c : Rat)
    (hlo : s ≤ r) (hhi : r ≤ s + 1)
    (hselected : selected = true → r = s + 1) :
    (if selected then if r = d then c else 0 else 0) =
      (if s + 1 = d then rankFilter d r selected * c else 0) := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.Level.rankFilter

def OAI.UniqueGamesTheorem.Appendix.Level.mergedCoefficient line 262
Source documentation
A finite merged coefficient. phase can incorporate a translation character and the indicator of one restriction fiber.
```
def mergedCoefficient {α : Type} (indices : List α)
    (phase coefficient : α → Rat) : Rat :=
…
```

theorem OAI.UniqueGamesTheorem.Appendix.Level.rank_filter_commutes_with_merge line 268

Source documentation

The character identity survives arbitrary merging, signs, and cancellation. No injectivity of the restriction of frequencies is assumed.

theorem rank_filter_commutes_with_merge {α : Type} (indices : List α)
    (d : Nat) (hd : 1 ≤ d) (rank restrictedRank : α → Nat)
    (selected : α → Bool) (phase coefficient : α → Rat)
    (hlo : ∀ x, restrictedRank x ≤ rank x)
    (hhi : ∀ x, rank x ≤ restrictedRank x + 1)
    (hselected : ∀ x, selected x = true → rank x = restrictedRank x + 1) :
    mergedCoefficient indices phase
        (fun x => if selected x then if rank x = d then coefficient x else 0 else 0) =
      mergedCoefficient indices phase
        (fun x => if restrictedRank x + 1 = d
          then rankFilter d (rank x) (selected x) * coefficient x else 0) := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.Level.mergedCoefficient, OAI.UniqueGamesTheorem.Appendix.Level.rankFilter

theorem OAI.UniqueGamesTheorem.Appendix.Level.higher_ranks_cannot_contaminate line 287
theorem OAI.UniqueGamesTheorem.Appendix.Level.iterated_globality_exponent line 293
Source documentation
Arithmetic in the iterated globality parameter 4^k * 2^(4*k*d - 2*k*(k-1)).
```
theorem iterated_globality_exponent {d k : Nat} (hd : 1 ≤ d) (hk : k ≤ d) :
    2 * k + 4 * k * d - 2 * k * (k - 1) ≤ 10 * d * d := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Level.successor_le_two_pow line 303
theorem OAI.UniqueGamesTheorem.Appendix.Level.selector_multiplicity_bound line 312
Source documentation
A deliberately coarse bound for the number of dimension-indexed selector choices. The geometric subspace count is an explicit hypothesis.
```
theorem selector_multiplicity_bound {d count : Nat} (hd : 1 ≤ d)
    (hcount : count ≤ (d + 1) ^ 2 * 2 ^ (d * d)) :
    count ≤ 2 ^ (3 * d * d) := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Level.final_exponent_slack line 326
Source documentation
The final fourth-root exponent has the advertised slack.
```
theorem final_exponent_slack (d : Nat) : 113 * d * d ≤ 4 * (30 * d * d) := by
…
```
def OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.compress line 341
Source documentation
Restriction in the domain and quotient in the codomain, as actual linear maps. This is the Fourier-frequency map of an affine restriction.
```
def compress (A : Submodule K V) (B : Submodule K W) (Y : W →ₗ[K] V) :
    B →ₗ[K] V ⧸ A := A.mkQ.comp (Y.comp B.subtype)
```
theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.finrank_comap_subtype_le line 344
theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.quotient_rank_bounds line 350
theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.quotient_rank_selected line 361
theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.domain_rank_bounds line 372
theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.domain_rank_selected line 387
theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.hybrid_rank_loss line 398
theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.finrank_comap_subtype_eq_iff line 411
Source documentation
Equality in the dimension bound for a subspace intersection forces the original subspace to lie in the restricting subspace.
```
theorem finrank_comap_subtype_eq_iff (A B : Submodule K V) :
    finrank K (A.comap B.subtype) = finrank K A ↔ A ≤ B := by
…
```
theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.quotient_rank_equality_iff line 424
theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.domain_rank_equality_iff line 438

theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.compression_rank_bounds line 452

Source documentation

Every genuine restriction loses at most its order in Fourier rank.

theorem compression_rank_bounds (A : Submodule K V) (B : Submodule K W)
    (Y : W →ₗ[K] V) :
    finrank K (range (compress A B Y)) ≤ finrank K (range Y) ∧
      finrank K (range Y) ≤
        finrank K (range (compress A B Y)) + finrank K A + finrank K (W ⧸ B) := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.compress

theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.hybrid_rank_loss_iff line 463

theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.line_rank_filter line 488

Source documentation

Instantiation of (A.17)'s rank filter for quotient by an actual line. The only dimension hypothesis is the line's dimension; no rank cutoff is imposed on the original map Y.

theorem line_rank_filter (A : Submodule K V) (Y : W →ₗ[K] V)
    (hline : finrank K A = 1) (d : Nat) (hd : 1 ≤ d) (c : Rat) :
    (if A ≤ range Y then
      if finrank K (range Y) = d then c else 0 else 0) =
      (if finrank K (range (A.mkQ.comp Y)) + 1 = d then
        UniqueGamesTheorem.Appendix.Level.rankFilter d (finrank K (range Y))
          (decide (A ≤ range Y)) * c else 0) := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.Level.rankFilter

theorem OAI.UniqueGamesTheorem.Appendix.Level.LinearRank.hyperplane_rank_filter line 509

Source documentation

The dual order-one instance: restriction to an actual hyperplane.

theorem hyperplane_rank_filter (B : Submodule K W) (Y : W →ₗ[K] V)
    (hhyperplane : finrank K (W ⧸ B) = 1) (d : Nat) (hd : 1 ≤ d) (c : Rat) :
    (if ker Y ≤ B then
      if finrank K (range Y) = d then c else 0 else 0) =
      (if finrank K (range (Y.comp B.subtype)) + 1 = d then
        UniqueGamesTheorem.Appendix.Level.rankFilter d (finrank K (range Y))
          (decide (ker Y ≤ B)) * c else 0) := by
…

Mentions: OAI.UniqueGamesTheorem.Appendix.Level.rankFilter

theorem OAI.UniqueGamesTheorem.Appendix.RankAdditivity.ker_add_of_disjoint line 551

Source documentation

Disjoint images prevent cancellation between the two map values.

theorem ker_add_of_disjoint (f g : W →ₗ[K] V)
    (h : Disjoint (LinearMap.range f) (LinearMap.range g)) :
    LinearMap.ker (f + g) = LinearMap.ker f ⊓ LinearMap.ker g := by
…

theorem OAI.UniqueGamesTheorem.Appendix.RankAdditivity.finrank_add_eq_iff line 573

Source documentation

The exact rank-additivity criterion used to define X ⪯ Y in Appendix A.1.

theorem finrank_add_eq_iff (f g : W →ₗ[K] V) :
    finrank K (LinearMap.range (f + g)) =
        finrank K (LinearMap.range f) + finrank K (LinearMap.range g) ↔
      Disjoint (LinearMap.range f) (LinearMap.range g) ∧
        LinearMap.ker f ⊔ LinearMap.ker g = ⊤ := by
…

theorem OAI.UniqueGamesTheorem.Appendix.RankAdditivity.range_left_le_range_add line 601

Source documentation

The left image is contained in the total image for a rank-additive pair.

theorem range_left_le_range_add (f g : W →ₗ[K] V)
    (h : finrank K (LinearMap.range (f + g)) =
      finrank K (LinearMap.range f) + finrank K (LinearMap.range g)) :
    LinearMap.range f ≤ LinearMap.range (f + g) := by
…

theorem OAI.UniqueGamesTheorem.Appendix.RankAdditivity.ker_add_le_ker_left line 618

Source documentation

The total kernel is contained in the left kernel for a rank-additive pair.

theorem ker_add_le_ker_left (f g : W →ₗ[K] V)
    (h : finrank K (LinearMap.range (f + g)) =
      finrank K (LinearMap.range f) + finrank K (LinearMap.range g)) :
    LinearMap.ker (f + g) ≤ LinearMap.ker f := by
…

def OAI.UniqueGamesTheorem.Appendix.RankAdditivity.RankBelow line 625
theorem OAI.UniqueGamesTheorem.Appendix.RankAdditivity.add_remainder line 630
theorem OAI.UniqueGamesTheorem.Appendix.RankAdditivity.rankBelow_iff line 633
theorem OAI.UniqueGamesTheorem.Appendix.RankAdditivity.range_le_of_rankBelow line 641
theorem OAI.UniqueGamesTheorem.Appendix.RankAdditivity.ker_le_of_rankBelow line 649
theorem OAI.UniqueGamesTheorem.Appendix.RankAdditivity.range_remainder_eq_range_on_kernel line 657
theorem OAI.UniqueGamesTheorem.Appendix.RankAdditivity.mem_ker_of_apply_mem_range_remainder line 680