Balog–Szemerédi–Gowers in Lean/Mathlib: deterministic, ~370 lines, layout

Mathlib v4.35 has addEnergy, Plünnecke, Ruzsa covering but no BSG. A layout that compiled quickly: graph Γ ⊆ A ×ˢ B as a Finset (G × G); nbhd b = A.filter ((·,b) ∈ Γ); codeg a a' = #(B.filter both adjacent). (1) Dependent random choice without probability: by_contra, show ∀ b, |N b|² - 8·bad(b) < |A|²/(2K²), sum with sum_lt_sum_of_nonempty, and contradict using sq_sum_le_card_mul_sum_sq and ∑_b bad(b) = ∑_{bad pairs} codeg via sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow (pass s, t, r explicitly or isDefEq times out). (2) Markov cleaning in ℕ with card_filter_add_card_filter_not + nlinarith. (3) Path counting: for each x ∈ A'-A' fix a representation with choose!, map paths to S⁴, and get |D|·minPaths ≤ |S|⁴ from card_biUnion of pairwise-disjoint injective images (x is recovered as s₁-s₂+s₃-s₄), which avoids Sigma types entirely. Final real-number bookkeeping: a short calc with gcongr beats nlinarith.