Section 15.3: The finite sparse-count lemma

This file was automatically generated by Claude.

Formalization of blueprint Section 15, "Common heights and concentration of the core terms" (sec:core), subsection 3, "The finite sparse-count lemma" (lines 2584-2707) of blueprint/formalization_blueprint.tex.

The finite sparse-count lemma (lem:sparse-count, blueprint lines 2587-2705)

theorem TrilinearHT.Auto.minimal_growth_iteration {G : Type u_1} [AddCommGroup G] [DecidableEq G] (X B : Finset G) (hmin : ∀ X' ⊆ X, (X + B).card * X'.card ≤ (X' + B).card * X.card) (m : ℕ) : ↑(X + m • B).card ≤ (↑(X + B).card / ↑X.card) ^ m * ↑X.card

Blueprint lines 2668-2674 (minimal-growth iteration): if X minimizes |X' + B|/|X'| among its nonempty subsets, then |X + mB| ≤ (|X + B|/|X|)^m |X| for the m-fold sumset (from the Plünnecke–Petridis inequality).

theorem TrilinearHT.Auto.count_balance_bound {J₀ L ℓ τ : ℝ} (hL : 1 ≤ L) (hℓ : 1 ≤ ℓ) (hτ : 0 < τ) (hJ0 : 0 ≤ J₀) (hJ : J₀ ≤ 3 * L * τ⁻¹ ^ 2) : J₀ * τ ^ 3 + √L * τ + ℓ * L * J₀ ^ 4 * (τ ^ 3 / L)⁻¹ ^ 7 * τ ^ 30 ≤ 85 * ℓ * L ^ 12 * τ

Blueprint eq:count-balance (lines 2700-2703): with J₀ ≤ 3Lτ^{-2}, η = τ³/L, L ≥ 1, ℓ ≥ 1 and τ > 0, J₀ τ³ + √L τ + ℓ L J₀⁴ η^{-7} τ^{30} ≤ 85 ℓ L^{12} τ.

Verification of the counting hypotheses (tested-counts, blueprint lines 2707-2744)

theorem TrilinearHT.Auto.pair_determination {u v s₁ s₂ e₁ e₂ w ε : ℝ} {a b c d : ℤ} (h₁ : ↑a * u + ↑b * v = s₁ + e₁) (h₂ : ↑c * u + ↑d * v = s₂ + e₂) (hD : a * d - b * c ≠ 0) (hw : ↑d * s₁ - ↑b * s₂ = ↑(a * d - b * c) * w) (he₁ : |e₁| ≤ ε) (he₂ : |e₂| ≤ ε) : |u - w| ≤ (|↑d| + |↑b|) * ε

Blueprint lines 2711-2712 (pair determination): if two label differences u, v satisfy a u + b v = s₁ + e₁, c u + d v = s₂ + e₂ with integer coefficients, nonzero determinant D = ad - bc, shifts with d s₁ - b s₂ = D w (the reserved shifts are divisible by the denominators 1, 2, 3) and errors at most ε, then |u - w| ≤ (|d| + |b|) ε.

theorem TrilinearHT.Auto.many_four_paths {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] (P : Finset X) (Q : Finset Y) (E : Finset (X × Y)) (hE : E ⊆ P ×ˢ Q) {M η : ℝ} (hM : 0 < M) (hPM : ↑P.card ≤ M) (hQM : ↑Q.card ≤ M) (hη : 0 < η) (hEη : η * M ^ 2 ≤ ↑E.card) : ∃ B₀ ⊆ P, η * M / 3 ≤ ↑B₀.card ∧ ∀ a ∈ B₀, ∀ a' ∈ B₀, η ^ 5 * M ^ 3 / 160000 ≤ ↑(bipFourPaths P Q E a a').card

Blueprint lines 2608-2609 (many four-step paths): in a bipartite graph with parts of size at most M and at least η M² edges, some subset B₀ of the first part with |B₀| ≥ η M / 3 has at least η⁵ M³ / 160000 four-step paths between any two of its vertices (repetitions allowed).

theorem TrilinearHT.Auto.bipFourPaths_colors_injOn {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] {C : Type u_3} (P : Finset X) (Q : Finset Y) (E : Finset (X × Y)) (col : X × Y → C) (hpx : ∀ (x : X) (y y' : Y), (x, y) ∈ E → (x, y') ∈ E → col (x, y) = col (x, y') → y = y') (hpy : ∀ (x x' : X) (y : Y), (x, y) ∈ E → (x', y) ∈ E → col (x, y) = col (x', y) → x = x') (a a' : X) : Set.InjOn (fun (p : Y × X × Y) => (col (a, p.1), col (p.2.1, p.1), col (p.2.1, p.2.2), col (a', p.2.2))) ↑(bipFourPaths P Q E a a')

Blueprint line 2609: for a proper edge coloring, the four-step paths between fixed endpoints have distinct ordered color sequences.

Difference covers and shift boxes (lem:sparse-count, blueprint lines 2618-2626)

theorem TrilinearHT.Auto.difference_cover_of_sequences {G : Type u_1} {C : Type u_2} [AddCommGroup G] [DecidableEq G] (B₀ : Finset G) (Cs : Finset C) (W : G → G → Finset C) (hW : ∀ a ∈ B₀, ∀ a' ∈ B₀, W a a' ⊆ Cs) {κ : ℕ} (hκ : ∀ a ∈ B₀, ∀ a' ∈ B₀, κ ≤ (W a a').card) (q : C → G) (U₁ U₂ : Finset G) (hq : ∀ a ∈ B₀, ∀ a' ∈ B₀, ∀ c ∈ W a a', a - a' - q c ∈ U₁) (hU : ∀ u ∈ U₁, ∀ v ∈ U₁, u - v ∈ U₂) (hneg : ∀ u ∈ U₂, -u ∈ U₂) (h0 : 0 ∈ U₂) : ∃ P ⊆ B₀ - B₀, P.card * κ ≤ Cs.card ∧ ∀ x ∈ B₀ - B₀, ∃ p ∈ P, x - p ∈ U₂

Blueprint lines 2622-2624 (packing by color sequences): if every pair (a, a') of B₀ has at least κ witness sequences c ∈ W a a' ⊆ Cs with a - a' - q c ∈ U₁, and U₁ - U₁ ⊆ U₂ with U₂ symmetric, then B₀ - B₀ is covered by translates p + U₂ of at most |Cs|/κ packed differences.

def TrilinearHT.Auto.shiftDot {d : ℕ} (n ζ : Fin d → ℤ) : ℤ

The pure shift n · ζ of an integer index vector.

Equations

• TrilinearHT.Auto.shiftDot n ζ = ∑ k : Fin d, n k * ζ k

theorem TrilinearHT.Auto.shiftDot_add {d : ℕ} (n m ζ : Fin d → ℤ) : shiftDot (n + m) ζ = shiftDot n ζ + shiftDot m ζ

theorem TrilinearHT.Auto.shiftDot_neg {d : ℕ} (n ζ : Fin d → ℤ) : shiftDot (-n) ζ = -shiftDot n ζ

theorem TrilinearHT.Auto.shiftDot_smul {d : ℕ} (c : ℤ) (n ζ : Fin d → ℤ) : shiftDot (c • n) ζ = c * shiftDot n ζ

def TrilinearHT.Auto.shiftBox {d : ℕ} (ζ : Fin d → ℤ) (N ε t : ℕ) : Finset ℤ

Blueprint line 2620: the shift box U(t) = {6 n · ζ + u : |n|_∞ ≤ t N, u ∈ ℤ, |u| ≤ t ε} (integer form after rescaling to the grid).

Equations

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

theorem TrilinearHT.Auto.mem_shiftBox {d : ℕ} {ζ : Fin d → ℤ} {N ε t : ℕ} {x : ℤ} : x ∈ shiftBox ζ N ε t ↔ ∃ (n : Fin d → ℤ), (∀ (k : Fin d), |n k| ≤ ↑(t * N)) ∧ ∃ (u : ℤ), |u| ≤ ↑(t * ε) ∧ x = 6 * shiftDot n ζ + u

theorem TrilinearHT.Auto.zero_mem_shiftBox {d : ℕ} (ζ : Fin d → ℤ) (N ε t : ℕ) : 0 ∈ shiftBox ζ N ε t

theorem TrilinearHT.Auto.add_mem_shiftBox {d : ℕ} {ζ : Fin d → ℤ} {N ε t t' : ℕ} {x y : ℤ} (hx : x ∈ shiftBox ζ N ε t) (hy : y ∈ shiftBox ζ N ε t') : x + y ∈ shiftBox ζ N ε (t + t')

theorem TrilinearHT.Auto.neg_mem_shiftBox {d : ℕ} {ζ : Fin d → ℤ} {N ε t : ℕ} {x : ℤ} (hx : x ∈ shiftBox ζ N ε t) : -x ∈ shiftBox ζ N ε t

theorem TrilinearHT.Auto.sub_mem_shiftBox {d : ℕ} {ζ : Fin d → ℤ} {N ε t t' : ℕ} {x y : ℤ} (hx : x ∈ shiftBox ζ N ε t) (hy : y ∈ shiftBox ζ N ε t') : x - y ∈ shiftBox ζ N ε (t + t')

theorem TrilinearHT.Auto.shiftBox_mono {d : ℕ} (ζ : Fin d → ℤ) (N ε : ℕ) {t t' : ℕ} (h : t ≤ t') : shiftBox ζ N ε t ⊆ shiftBox ζ N ε t'

theorem TrilinearHT.Auto.exists_coarse_index {n : ℤ} {N t : ℕ} (h : |n| ≤ ↑(t * N)) : ∃ (j : ℤ), |j| ≤ ↑t ∧ |n - j * ↑N| ≤ ↑N

Integer division with a bounded quotient: |n| ≤ tN gives |j| ≤ t and |n - jN| ≤ N.

theorem TrilinearHT.Auto.card_shiftBox_le {d : ℕ} (ζ : Fin d → ℤ) (N ε t : ℕ) : (shiftBox ζ N ε t).card ≤ (2 * t + 1) ^ (d + 1) * (shiftBox ζ N ε 1).card

Blueprint line 2650: U(t) is covered by (2t + 1)^{d+1} translates of U(1).

theorem TrilinearHT.Auto.small_growth_numeric {D : ℕ} (hD : 1 ≤ D) : (2000 * D ^ 2 + 3) ^ (3 * D) < 2 ^ (500 * D ^ 2)

(2000 D² + 3)^{3D} < 2^{500 D²} for D ≥ 1.

theorem TrilinearHT.Auto.exists_small_growth_scale {α : Type u_1} (U : Fin 3 → ℕ → Finset α) {D : ℕ} (hD : 1 ≤ D) (hmono : ∀ (i : Fin 3) (t t' : ℕ), t ≤ t' → U i t ⊆ U i t') (hne : ∀ (i : Fin 3), (U i 1).Nonempty) (hcard : ∀ (i : Fin 3) (t : ℕ), (U i t).card ≤ (2 * t + 1) ^ D * (U i 1).card) : ∃ (k : ℕ), 2 * k + 1 ≤ 1000 * D ^ 2 ∧ ∀ (i : Fin 3), (U i (2 * k + 3)).card ≤ 2 * (U i (2 * k + 1)).card

Blueprint lines 2650-2651 (one small-growth scale): three increasing families of finite sets with |U_i(t)| ≤ (2t+1)^D |U_i(1)| and U_i(1) nonempty have a common odd scale H = 2k + 1 ≤ 1000 D² with |U_i(H + 2)| ≤ 2 |U_i(H)| for all three.

Packings and minimal growth (lem:sparse-count, blueprint lines 2652-2676)

theorem TrilinearHT.Auto.exists_packing_cover {G : Type u_1} [AddCommGroup G] (S U : Finset G) (h0 : 0 ∈ U) (hneg : ∀ x ∈ U, -x ∈ U) : ∃ P ⊆ S, (∀ p ∈ P, ∀ p' ∈ P, p - p' ∈ U → p = p') ∧ ∀ x ∈ S, ∃ p ∈ P, x - p ∈ U

A maximal packing of a finite set by a symmetric neighborhood U ∋ 0 is a cover.

theorem TrilinearHT.Auto.neg_mem_nsmul_neg {G : Type u_1} [AddCommGroup G] [DecidableEq G] {B : Finset G} {m : ℕ} {x : G} (hx : x ∈ m • B) : -x ∈ m • -B

theorem TrilinearHT.Auto.growth_packing_bound {G : Type u_1} [AddCommGroup G] [DecidableEq G] (U : ℕ → Finset G) (hU0 : ∀ (t : ℕ), 0 ∈ U t) (hadd : ∀ (t t' : ℕ) (x y : G), x ∈ U t → y ∈ U t' → x + y ∈ U (t + t')) (hneg : ∀ (t : ℕ), ∀ x ∈ U t, -x ∈ U t) (B B₀ P : Finset G) (hB₀ : B₀ ⊆ B) (hB₀ne : B₀.Nonempty) (H : ℕ) (hsep : ∀ a ∈ B₀, ∀ a' ∈ B₀, a - a' ∈ U (H + H) → a = a') (hcov : ∀ a ∈ B, ∀ b ∈ B, ∃ p ∈ P, a - b - p ∈ U 2) (hdouble : (U (H + 2)).card ≤ 2 * (U H).card) (m : ℕ) (P' : Finset G) (hP' : P' ⊆ m • B) (hpack : ∀ p ∈ P', ∀ p' ∈ P', p - p' ∈ U (H + H) → p = p') : ↑P'.card ≤ (2 * ↑P.card / ↑B₀.card) ^ m * ↑B₀.card

Blueprint lines 2652-2676 (one role): let U be an additive family of symmetric finite sets, B₀ ⊆ B a nonempty anchor set whose translates by U(H) are disjoint, B - B ⊆ P + U(2), and |U(H + 2)| ≤ 2|U(H)|. Then every packing P' ⊆ mB with pairwise differences outside U(2H) satisfies |P'| ≤ (2|P|/|B₀|)^m |B₀| (minimal growth of Z = B₀ + U(H) and one anchor translate).

The slab cover (lem:sparse-count, blueprint lines 2678-2687)

theorem TrilinearHT.Auto.abs_cofactor_le {α β : ℤ} (h : α * β = 6) : |β| ≤ 6 ∧ α ≠ 0

theorem TrilinearHT.Auto.mem_shiftBox_real {d : ℕ} {ζ : Fin d → ℤ} {N ε t : ℕ} {x : ℤ} (hx : x ∈ shiftBox ζ N ε t) : ∃ (n : Fin d → ℤ), (∀ (i : Fin d), |↑(n i)| ≤ ↑t * ↑N) ∧ ∃ (u : ℤ), |↑u| ≤ ↑t * ↑ε ∧ x = 6 * shiftDot n ζ + u

Elements of a shift box with real bounds.

theorem TrilinearHT.Auto.div_close {d : ℕ} {ζ : Fin d → ℤ} {α β x : ℤ} (hαβ : α * β = 6) (k : Fin d → ℤ) {E : ℝ} (h : |↑(α * x - 6 * shiftDot k ζ)| ≤ E) : |↑(x - shiftDot (β • k) ζ)| ≤ E

Dividing a close relation |α x - 6 k · ζ| ≤ E by α (αβ = 6): |x - (β k) · ζ| ≤ E.

theorem TrilinearHT.Auto.anchor_sep_shiftBox {d : ℕ} {ζ : Fin d → ℤ} {N ε H : ℕ} {B₀ : Finset ℤ} {Q S : ℝ} (hanch : ∀ a ∈ B₀, ∀ a' ∈ B₀, ∀ (k : Fin d → ℤ), (∀ (i : Fin d), |↑(k i)| ≤ Q) → |↑(a - a' - shiftDot k ζ)| ≤ S → a = a') (hQ : 12 * (↑H * ↑N) ≤ Q) (hS : 2 * (↑H * ↑ε) ≤ S) (a : ℤ) : a ∈ B₀ → ∀ a' ∈ B₀, a - a' ∈ shiftBox ζ N ε (H + H) → a = a'

Anchor separation implies disjointness of anchor translates by U(H).

theorem TrilinearHT.Auto.column_packing_bound {d : ℕ} (ζ : Fin d → ℤ) (N ε H : ℕ) (B B₀ P : Finset ℤ) (hB₀ : B₀ ⊆ B) (hB₀ne : B₀.Nonempty) (hcov : ∀ a ∈ B, ∀ b ∈ B, ∃ p ∈ P, a - b - p ∈ shiftBox ζ N ε 2) (hdouble : (shiftBox ζ N ε (H + 2)).card ≤ 2 * (shiftBox ζ N ε H).card) {Q S : ℝ} (hanch : ∀ a ∈ B₀, ∀ a' ∈ B₀, ∀ (k : Fin d → ℤ), (∀ (i : Fin d), |↑(k i)| ≤ Q) → |↑(a - a' - shiftDot k ζ)| ≤ S → a = a') {α β : ℤ} (hαβ : α * β = 6) (hα : |α| ≤ 3) (Lc : Finset ℤ) (hLc : Lc ⊆ 2 • B) {Kc Ec : ℝ} (hclose : ∀ x ∈ Lc, ∀ x' ∈ Lc, ∃ (k : Fin d → ℤ), (∀ (i : Fin d), |↑(k i)| ≤ Kc) ∧ |↑(α * (x - x') - 6 * shiftDot k ζ)| ≤ Ec) (hQ : 6 * (Kc + 6 * (↑H * ↑N)) ≤ Q) (hQ' : 12 * (↑H * ↑N) ≤ Q) (hS : Ec + 6 * (↑H * ↑ε) ≤ S) (hS' : 2 * (↑H * ↑ε) ≤ S) (P₃ : Finset ℤ) (hP₃ : P₃ ⊆ Lc) (hpack : ∀ p ∈ P₃, ∀ p' ∈ P₃, p - p' ∈ shiftBox ζ N ε (H + H) → p = p') : ↑P₃.card ≤ (2 * ↑P.card / ↑B₀.card) ^ 3

Blueprint lines 2681-2687 (local third-coordinate packing): if the pairwise differences of a column set Lc ⊆ 2B satisfy |α(x - x') - 6 k · ζ| ≤ E_c with |k|_∞ ≤ K_c, and anchors are separated, then any packing of Lc outside U(2H) has at most (2|P|/|B₀|)³ elements: the sums B₀ + P₃ ⊆ 3B form a packing with distinct sums.

Separation of translated triples (lem:sparse-count, blueprint lines 2689-2692)

theorem TrilinearHT.Auto.shiftDot_sum {d : ℕ} {κ : Type u_1} (s : Finset κ) (c : κ → ℤ) (k : κ → Fin d → ℤ) (ζ : Fin d → ℤ) : shiftDot (∑ j ∈ s, c j • k j) ζ = ∑ j ∈ s, c j * shiftDot (k j) ζ

def TrilinearHT.Auto.tripleResidual {d : ℕ} (ζ : Fin d → ℤ) (α x : Fin 3 → ℤ) (n : Fin d → ℤ) : ℤ

The annular residual Σ_j α_j x_j + 36 n · ζ of a triple.

Equations

• TrilinearHT.Auto.tripleResidual ζ α x n = ∑ j : Fin 3, α j * x j + 36 * TrilinearHT.Auto.shiftDot n ζ

theorem TrilinearHT.Auto.translated_triples_gap {d : ℕ} (ζ : Fin d → ℤ) (α : Fin 3 → ℤ) (hα3 : ∀ (j : Fin 3), |α j| ≤ 3) (x x' y y' : Fin 3 → ℤ) (nx nx' ny ny' : Fin d → ℤ) (k : Fin 3 → Fin d → ℤ) (w : Fin 3 → ℤ) (hdiff : ∀ (j : Fin 3), x j + y j - (x' j + y' j) = 6 * shiftDot (k j) ζ + w j) {μ ν R e₁ e₂ Bw Kb Q : ℝ} (hR : 0 ≤ μ * R) (hx : μ * R ≤ |↑(tripleResidual ζ α x nx)|) (hx' : |↑(tripleResidual ζ α x nx)| ≤ ν * R) (hx'' : |↑(tripleResidual ζ α x' nx')| ≤ e₁) (hy : |↑(tripleResidual ζ α y ny)| ≤ e₁) (hy' : |↑(tripleResidual ζ α y' ny')| ≤ e₁) (hw : ∀ (j : Fin 3), |↑(w j)| ≤ e₂) (herr : 3 * e₁ + 9 * e₂ ≤ μ * R / 100) (hn : ∀ (i : Fin d), |↑(nx i)| ≤ Bw ∧ |↑(nx' i)| ≤ Bw ∧ |↑(ny i)| ≤ Bw ∧ |↑(ny' i)| ≤ Bw) (hk : ∀ (j : Fin 3) (i : Fin d), |↑(k j i)| ≤ Kb) (hQ : 144 * Bw + 54 * Kb ≤ Q) (hgap : ∀ (m : Fin d → ℤ), (∀ (i : Fin d), |↑(m i)| ≤ Q) → ¬(μ * R / 50 ≤ |↑(shiftDot m ζ)| ∧ |↑(shiftDot m ζ)| ≤ 50 * ν * R)) : False

Blueprint lines 2690-2692: two translated triples x + y, x' + y' whose coordinates differ by box elements 6 k_j · ζ + w_j, where the residual of x is annular at the big scale μR ≤ |ρ_x| ≤ νR and all other residuals and the scalars w_j are small, produce a pure shift m · ζ of size between μR/50 and 50νR; the gap hypothesis excludes it.

theorem TrilinearHT.Auto.tripleResidual_add {d : ℕ} (ζ : Fin d → ℤ) (α x y : Fin 3 → ℤ) (n m : Fin d → ℤ) : tripleResidual ζ α (x + y) (n + m) = tripleResidual ζ α x n + tripleResidual ζ α y m