Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Dense bipartite graph contains a 333-path-rich rectangle

Proved
Finset.dense_bipartite_has_path3_rectangle

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

additive-combinatoricsbalog-szemeredi-gowersdependent-random-choicegraphs

Let GGG be an additive commutative group, let 0<δ≤10 < \delta \le 10<δ≤1, and let A,B⊆GA, B \subseteq GA,B⊆G be finite sets with AAA nonempty and ∣A∣=∣B∣|A| = |B|∣A∣=∣B∣. Let E⊆A×BE \subseteq A \times BE⊆A×B be a set of edges with

∣E∣≥δ ∣A∣ ∣B∣.|E| \ge \delta\,|A|\,|B|.∣E∣≥δ∣A∣∣B∣.

Then there exist A′⊆AA' \subseteq AA′⊆A and B′⊆BB' \subseteq BB′⊆B with

∣A′∣≥δ8 ∣A∣,∣B′∣≥δ8 ∣A∣,|A'| \ge \tfrac{\delta}{8}\,|A|, \qquad |B'| \ge \tfrac{\delta}{8}\,|A|,∣A′∣≥8δ​∣A∣,∣B′∣≥8δ​∣A∣,

such that for every a∈A′a \in A'a∈A′ and every b∈B′b \in B'b∈B′,

#{(b1,a2)∈B×A:(a,b1)∈E, (a2,b1)∈E, (a2,b)∈E} ≥ δ5212 ∣A∣2.\#\{(b_1, a_2) \in B \times A : (a,b_1) \in E,\ (a_2,b_1) \in E,\ (a_2,b) \in E\} \ \ge\ \tfrac{\delta^5}{2^{12}}\,|A|^2.#{(b1​,a2​)∈B×A:(a,b1​)∈E, (a2​,b1​)∈E, (a2​,b)∈E} ≥ 212δ5​∣A∣2.

This is the rectangle lemma that the Balog-Szemeredi-Gowers argument in this project consumes, proved along the Fox-Sudakov dependent-random-choice route: degree pruning, one application of pair dependent random choice, a Markov refinement on rows, and a rare/popular split on columns. It is not a transcription of Fox-Sudakov, Dependent random choice, Lemma 5.2; it departs from that lemma in two ways, recorded here.

Deviation 1: the counted set carries no distinctness conditions. Fox-Sudakov count genuine paths of length three. Their proof produces at least c2n/32−1c^2n/32 - 1c2n/32−1 neighbours a2≠aa_2 \ne aa2​=a of bbb in the core set, and for each of those at least c3n/32−1c^3n/32 - 1c3n/32−1 common neighbours b1≠bb_1 \ne bb1​=b; the two "−1-1−1" terms are exactly those distinctness corrections, and the product of the two factors is what is bounded below by 2−12c5n22^{-12}c^5n^22−12c5n2. The set counted in the statement above is the plain filter of B×AB \times AB×A by the three edge conditions, with no requirement a2≠aa_2 \ne aa2​=a or b1≠bb_1 \ne bb1​=b, so degenerate pairs are admitted. The count above therefore ranges over a strictly larger set and the conclusion is weaker than Lemma 5.2's: Lemma 5.2's bound implies the bound above, while the bound above does not give Lemma 5.2's. The weaker form is sound for the Balog-Szemeredi-Gowers use, because the representation consumed downstream,

y  =  a+b  =  (a+b1)−(a2+b1)+(a2+b)  =  x−x′+x′′,y \;=\; a + b \;=\; (a + b_1) - (a_2 + b_1) + (a_2 + b) \;=\; x - x' + x'',y=a+b=(a+b1​)−(a2​+b1​)+(a2​+b)=x−x′+x′′,

is valid for degenerate paths too: it needs only that the three pairs are edges, never that the vertices are distinct.

Deviation 2: a guaranteed lower bound replaces the exact density. After pruning to the rows A1={a∈A:#{b∈B:(a,b)∈E}≥δ2∣B∣}A_1 = \{a \in A : \#\{b \in B : (a,b) \in E\} \ge \tfrac{\delta}{2}|B|\}A1​={a∈A:#{b∈B:(a,b)∈E}≥2δ​∣B∣}, Fox-Sudakov run dependent random choice with the exact edge density c1=e(A1,B)/(∣A1∣ ∣B∣)c_1 = e(A_1, B)/(|A_1|\,|B|)c1​=e(A1​,B)/(∣A1​∣∣B∣). The proof formalized here instead sets

c0  =  (δ/2) ∣A∣∣A1∣c_0 \;=\; \frac{(\delta/2)\,|A|}{|A_1|}c0​=∣A1​∣(δ/2)∣A∣​

and runs dependent random choice with c0c_0c0​. Since e(A1,B)≥δ2∣A∣ ∣B∣e(A_1,B) \ge \tfrac{\delta}{2}|A|\,|B|e(A1​,B)≥2δ​∣A∣∣B∣, one has c0≤c1c_0 \le c_1c0​≤c1​ — this is the lower bound Fox-Sudakov themselves display — so the density hypothesis of the dependent-random-choice lemma is met and the argument is sound, but every bound downstream is stated in terms of c0c_0c0​ rather than c1c_1c1​.

A third, smaller difference: the column bound is stated here as ∣B′∣≥δ8∣A∣|B'| \ge \tfrac{\delta}{8}|A|∣B′∣≥8δ​∣A∣, where Fox-Sudakov state ∣B′∣≥c4n|B'| \ge \tfrac{c}{4}n∣B′∣≥4c​n; only the weaker δ/8\delta/8δ/8 form is claimed.

The conclusion feeds the Tao-Vu triple-count injection, which converts path richness plus a small restricted sumset into a bound on the honest sumset ∣A′+B′∣|A' + B'|∣A′+B′∣.

Preamble
import Mathlib

open scoped Pointwise
Formal statement
theorem Finset.dense_bipartite_has_path3_rectangle {G : Type*} [AddCommGroup G] [DecidableEq G]
    (δ : ℝ) (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1)
    (A B : Finset G) (hA : A.Nonempty) (hAB : A.card = B.card)
    (E : Finset (G × G)) (hE_sub : E ⊆ A ×ˢ B)
    (hE_dense : δ * (A.card : ℝ) * (B.card : ℝ) ≤ (E.card : ℝ)) :
    ∃ A' B' : Finset G, A' ⊆ A ∧ B' ⊆ B ∧
      (δ / 8) * (A.card : ℝ) ≤ (A'.card : ℝ) ∧
      (δ / 8) * (A.card : ℝ) ≤ (B'.card : ℝ) ∧
      ∀ a ∈ A', ∀ b ∈ B',
        (δ^5 / 2^12) * (A.card : ℝ)^2 ≤
          (((B ×ˢ A).filter fun q : G × G ↦
            (a, q.1) ∈ E ∧ (q.2, q.1) ∈ E ∧ (q.2, b) ∈ E).card : ℝ) := by sorry
Source
Fox-Sudakov, Dependent random choice, Random Structures & Algorithms 38 (2011) 68-99, Section 5.1, Lemma 5.2 (p. 9). Formalized with the source's a' != a and b' != b distinctness terms dropped, so the path count admits degenerate paths and the conclusion is weaker than the paper's; sound for the BSG application. Compare Tao-Vu, Additive Combinatorics, Cambridge Univ. Press (2006), Corollary 6.20, which is a different variant with different constants. Formalized in https://github.com/mysticflounder/lean-formalizations/blob/dd46c17a2a034d7bfa0df02e7f77834d35592864/lean/LeanFormalizations/Combinatorics/Additive/BalogSzemerediGowers.lean#L1932-L1970
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, licensed under Apache 2.0.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTermsJoin SlackJoin Zulip© 2026 Prove2Me