Prove2Me

Tao–Vu 33-path count bounded by s1−s2+s3s_1 - s_2 + s_3 triples

Proved
Finset.path3_count_le_triple_rep_count

by mysticflounder · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricsbalog-szemeredi-gowersgraphssumsets

Let GG be an additive commutative group, A,B,S⊆GA, B, S \subseteq G finite sets, and E⊆G×GE \subseteq G \times G a set of pairs all of whose sums lie in SS (i.e. (x,y)∈E⇒x+y∈S(x,y) \in E \Rightarrow x + y \in S). For fixed endpoints a,b∈Ga, b \in G, the number of length-33 paths

a→b1→a2→b,(b1,a2)∈B×A, (a,b1),(a2,b1),(a2,b)∈Ea \to b_1 \to a_2 \to b, \qquad (b_1, a_2) \in B \times A,\ (a,b_1),(a_2,b_1),(a_2,b) \in E

satisfies #{3-paths from a to b through E}≤#{(s1,s2,s3)∈S3:s1−s2+s3=a+b}.\#\{\text{$3$-paths from $a$ to $b$ through $E$}\} \le \#\{(s_1, s_2, s_3) \in S^3 : s_1 - s_2 + s_3 = a + b\}. The map (b1,a2)↦(a+b1, a2+b1, a2+b)(b_1, a_2) \mapsto (a + b_1,\, a_2 + b_1,\, a_2 + b) is injective with the relation s1−s2+s3=a+bs_1 - s_2 + s_3 = a + b. This Tao–Vu injection is the key algebraic step of the graph BSG proof: path richness of a pair (a,b)(a,b) forces the triple-representation number of a+ba + b from the small set SS to be large, so a uniform path lower bound over A′×B′A' \times B' yields, by double counting, the bound ∣A′+B′∣≤∣S∣3/M|A' + B'| \le |S|^3 / M.

Preamble
import Mathlib

open scoped Pointwise
Formal statement
theorem Finset.path3_count_le_triple_rep_count {G : Type*} [AddCommGroup G] [DecidableEq G]
    (A B S : Finset G) (E : Finset (G × G)) (hSdef : ∀ p ∈ E, p.1 + p.2 ∈ S)
    (a b : G) :
    (((B ×ˢ A).filter fun q : G × G ↦
        (a, q.1) ∈ E ∧ (q.2, q.1) ∈ E ∧ (q.2, b) ∈ E).card : ℕ)
    ≤ ((S ×ˢ S ×ˢ S).filter
        fun p : G × G × G ↦ p.1 - p.2.1 + p.2.2 = a + b).card := by sorry
Source
Injection step y = x - x' + x'' inside Fox-Sudakov, Dependent random choice, Random Structures & Algorithms 38 (2011) 68-99, Section 5.1 (p. 9) / the proof of Tao-Vu, Additive Combinatorics, Cambridge Univ. Press (2006), Theorem 2.29. Not separately stated in the cited works. Formalized in https://github.com/mysticflounder/lean-formalizations/blob/dd46c17a2a034d7bfa0df02e7f77834d35592864/lean/LeanFormalizations/Combinatorics/Additive/BalogSzemerediGowers.lean#L441-L502
Human review

  • Endorsed by Shuze Chen · Sep 18, 2026

  • Endorsed by mysticflounder · Sep 18, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph