Balog-Szemeredi-Gowers and dense bipartite paths

This file was automatically generated by Codex.

The classical energy-to-small-difference-set argument for finite subsets of arbitrary abelian groups. Its combinatorial prerequisite is a dependent random choice argument producing many four-step paths between every pair in a large vertex set of a dense finite bipartite graph. Repeated vertices are allowed. Proper edge colors recover a path from its starting vertex.

The intended quantitative conclusion is the source exponent ten: additive energy at least |A|^3/K yields a subset of size at least c|A|/K whose difference set has size at most C K^10 times the subset size. The proof is developed in forward source order; no unproved target is assumed.

Verified source: blueprint/formalization_blueprint.tex, lem:four-paths, lines 668-680, and lem:BSG, lines 683-698. All statements and supporting definitions use only Mathlib and this module. Mathlib's Finset.addEnergy is the standard additive-energy quantity used by the consuming theorem.

noncomputable def TrilinearHT.Auto.bipartiteNeighborhood {α : Type u_1} {β : Type u_2} [Fintype α] (E : α → β → Prop) (b : β) : Finset α

Neighborhood in the first part of a finite bipartite relation.

Equations

• TrilinearHT.Auto.bipartiteNeighborhood E b = {a : α | E a b}

noncomputable def TrilinearHT.Auto.bipartiteEdgeCount {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) : ℕ

The ordinary counting cardinality of the bipartite edge set.

Equations

• TrilinearHT.Auto.bipartiteEdgeCount E = {p : α × β | E p.1 p.2}.card

noncomputable def TrilinearHT.Auto.bipartiteCodegree {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (a a' : α) : ℕ

The number of common neighbors of an ordered pair of first-part vertices.

Equations

• TrilinearHT.Auto.bipartiteCodegree E a a' = {b : β | E a b ∧ E a' b}.card

theorem TrilinearHT.Auto.bipartiteCodegree_symm {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (a a' : α) : bipartiteCodegree E a a' = bipartiteCodegree E a' a

theorem TrilinearHT.Auto.bipartite_sum_neighborhood_card {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) : ∑ b : β, (bipartiteNeighborhood E b).card = bipartiteEdgeCount E

Counting edges by their second-part endpoint gives the neighborhood first moment.

theorem TrilinearHT.Auto.bipartite_edge_sq_le_neighborhood_sq {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) : ↑(bipartiteEdgeCount E) ^ 2 ≤ ↑(Fintype.card β) * ∑ b : β, ↑(bipartiteNeighborhood E b).card ^ 2

Finite Cauchy-Schwarz gives the lower second moment used by dependent random choice.

theorem TrilinearHT.Auto.bipartite_second_moment_lower {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) {η : ℝ} {n : ℕ} (hη : 0 ≤ η) (hβ : Fintype.card β ≤ n) (hedges : η * ↑n ^ 2 ≤ ↑(bipartiteEdgeCount E)) : η ^ 2 * ↑n ^ 4 ≤ ↑n * ∑ b : β, ↑(bipartiteNeighborhood E b).card ^ 2

Source second moment without division, valid also when the part-size bound is zero.

Bad-pair averaging

noncomputable def TrilinearHT.Auto.bipartiteBadPairs {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (τ : ℝ) (Y : Finset α) : Finset (α × α)

Ordered pairs in a finite set whose common-neighbor count is below a threshold.

Equations

• TrilinearHT.Auto.bipartiteBadPairs E τ Y = {p ∈ Y ×ˢ Y | ↑(TrilinearHT.Auto.bipartiteCodegree E p.1 p.2) < τ}

noncomputable def TrilinearHT.Auto.bipartiteBadPartners {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (τ : ℝ) (Y : Finset α) (a : α) : Finset α

Bad partners of a specified vertex, with ordered-pair convention.

Equations

• TrilinearHT.Auto.bipartiteBadPartners E τ Y a = {a' ∈ Y | ↑(TrilinearHT.Auto.bipartiteCodegree E a a') < τ}

theorem TrilinearHT.Auto.bipartiteBadPairs_card_eq_sum {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (τ : ℝ) (Y : Finset α) : (bipartiteBadPairs E τ Y).card = ∑ a ∈ Y, (bipartiteBadPartners E τ Y a).card

theorem TrilinearHT.Auto.bipartiteBadPairs_neighborhood_card {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) (τ : ℝ) (b : β) : (bipartiteBadPairs E τ (bipartiteNeighborhood E b)).card = ∑ a : α, ∑ a' : α, if ↑(bipartiteCodegree E a a') < τ then if E a b ∧ E a' b then 1 else 0 else 0

theorem TrilinearHT.Auto.bipartite_bad_pairs_double_count {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) (τ : ℝ) : ∑ b : β, (bipartiteBadPairs E τ (bipartiteNeighborhood E b)).card = ∑ a : α, ∑ a' : α, if ↑(bipartiteCodegree E a a') < τ then bipartiteCodegree E a a' else 0

A bad ordered pair belongs to exactly its codegree many neighborhoods.

theorem TrilinearHT.Auto.bipartite_bad_pairs_sum_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) {τ : ℝ} (hτ : 0 ≤ τ) : ∑ b : β, ↑(bipartiteBadPairs E τ (bipartiteNeighborhood E b)).card ≤ ↑(Fintype.card α) ^ 2 * τ

The total bad-pair count is at most the codegree threshold times the number of ordered pairs in the first part.

theorem TrilinearHT.Auto.bipartite_dense_neighborhood {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) {η : ℝ} {n : ℕ} (hn : 0 < n) (hη : 0 < η) (hα : Fintype.card α ≤ n) (hβ : Fintype.card β ≤ n) (hedges : η * ↑n ^ 2 ≤ ↑(bipartiteEdgeCount E)) : ∃ (b : β), η ^ 2 * ↑n ^ 2 / 2 ≤ ↑(bipartiteNeighborhood E b).card ^ 2 - 100 * ↑(bipartiteBadPairs E (η ^ 2 * ↑n / 100000) (bipartiteNeighborhood E b)).card

Blueprint lem:four-paths, lines 670-674: select an actual neighborhood whose squared size minus one hundred times its bad ordered pairs is at least half the density-squared scale. The zero-size case is handled separately by the final graph theorem, so the sampling step has a positive size bound.

Deleting vertices with many bad partners

noncomputable def TrilinearHT.Auto.bipartiteRetained {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (τ : ℝ) (Y : Finset α) : Finset α

Retain exactly the vertices with at most one quarter of the neighborhood as bad partners, as in the source deletion step.

Equations

• TrilinearHT.Auto.bipartiteRetained E τ Y = {a ∈ Y | ↑(TrilinearHT.Auto.bipartiteBadPartners E τ Y a).card ≤ ↑Y.card / 4}

theorem TrilinearHT.Auto.mem_bipartiteRetained {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (τ : ℝ) (Y : Finset α) (a : α) : a ∈ bipartiteRetained E τ Y ↔ a ∈ Y ∧ ↑(bipartiteBadPartners E τ Y a).card ≤ ↑Y.card / 4

theorem TrilinearHT.Auto.bipartiteRetained_subset {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (τ : ℝ) (Y : Finset α) : bipartiteRetained E τ Y ⊆ Y

theorem TrilinearHT.Auto.bipartite_deleted_card_lt {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (τ : ℝ) (Y : Finset α) (hbad : 100 * ↑(bipartiteBadPairs E τ Y).card < ↑Y.card ^ 2) : ↑(Y \ bipartiteRetained E τ Y).card < ↑Y.card / 25

Source deletion count: fewer than |Y|/25 vertices are deleted when fewer than |Y|^2/100 ordered pairs are bad.

theorem TrilinearHT.Auto.bipartiteRetained_card_lower {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (τ : ℝ) (Y : Finset α) (hbad : 100 * ↑(bipartiteBadPairs E τ Y).card < ↑Y.card ^ 2) : 24 * ↑Y.card / 25 < ↑(bipartiteRetained E τ Y).card

At least twenty-four twenty-fifths of the neighborhood remains.

theorem TrilinearHT.Auto.bipartite_dense_retained_neighborhood {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) {η : ℝ} {n : ℕ} (hn : 0 < n) (hη : 0 < η) (hα : Fintype.card α ≤ n) (hβ : Fintype.card β ≤ n) (hedges : η * ↑n ^ 2 ≤ ↑(bipartiteEdgeCount E)) : ∃ (b : β), η * ↑n / 2 ≤ ↑(bipartiteNeighborhood E b).card ∧ η * ↑n / 4 ≤ ↑(bipartiteRetained E (η ^ 2 * ↑n / 100000) (bipartiteNeighborhood E b)).card ∧ ∀ a ∈ bipartiteRetained E (η ^ 2 * ↑n / 100000) (bipartiteNeighborhood E b), ↑(bipartiteBadPartners E (η ^ 2 * ↑n / 100000) (bipartiteNeighborhood E b) a).card ≤ ↑(bipartiteNeighborhood E b).card / 4

Blueprint lem:four-paths, line 675: the selected neighborhood is large, and the actual retained set has size at least eta*n/4. Every retained vertex has at most a quarter of the original neighborhood as bad partners.

Common middle vertices and four-step paths

noncomputable def TrilinearHT.Auto.bipartiteCommonGood {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (τ : ℝ) (Y : Finset α) (x y : α) : Finset α

The common good partners of two retained endpoints inside the original neighborhood.

Equations

• TrilinearHT.Auto.bipartiteCommonGood E τ Y x y = Y \ (TrilinearHT.Auto.bipartiteBadPartners E τ Y x ∪ TrilinearHT.Auto.bipartiteBadPartners E τ Y y)

theorem TrilinearHT.Auto.mem_bipartiteCommonGood {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (τ : ℝ) (Y : Finset α) (x y u : α) : u ∈ bipartiteCommonGood E τ Y x y ↔ u ∈ Y ∧ τ ≤ ↑(bipartiteCodegree E x u) ∧ τ ≤ ↑(bipartiteCodegree E y u)

theorem TrilinearHT.Auto.bipartiteCommonGood_card_lower {α : Type u_1} {β : Type u_2} [Fintype β] (E : α → β → Prop) (τ : ℝ) (Y : Finset α) {x y : α} (hx : x ∈ bipartiteRetained E τ Y) (hy : y ∈ bipartiteRetained E τ Y) : ↑Y.card / 2 ≤ ↑(bipartiteCommonGood E τ Y x y).card

At least half the original neighborhood is a good partner of both retained endpoints.

noncomputable def TrilinearHT.Auto.bipartiteFourPaths {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) (x y : α) : Finset (β × α × β)

Actual four-step paths with fixed endpoints. The three interior vertices are freely chosen; repeated vertices are permitted.

Equations

• TrilinearHT.Auto.bipartiteFourPaths E x y = {p : β × α × β | E x p.1 ∧ E p.2.1 p.1 ∧ E p.2.1 p.2.2 ∧ E y p.2.2}

theorem TrilinearHT.Auto.mem_bipartiteFourPaths {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) (x y : α) (p : β × α × β) : p ∈ bipartiteFourPaths E x y ↔ E x p.1 ∧ E p.2.1 p.1 ∧ E p.2.1 p.2.2 ∧ E y p.2.2

theorem TrilinearHT.Auto.bipartiteFourPaths_card {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) (x y : α) : (bipartiteFourPaths E x y).card = ∑ u : α, bipartiteCodegree E x u * bipartiteCodegree E u y

Counting paths by their middle vertex gives the product of the two codegrees.

theorem TrilinearHT.Auto.bipartiteFourPaths_card_lower {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) {τ : ℝ} (hτ : 0 ≤ τ) (Y : Finset α) {x y : α} (hx : x ∈ bipartiteRetained E τ Y) (hy : y ∈ bipartiteRetained E τ Y) : ↑Y.card / 2 * τ ^ 2 ≤ ↑(bipartiteFourPaths E x y).card

Each common good middle vertex contributes at least the square of the codegree threshold many distinct paths.

theorem TrilinearHT.Auto.bipartite_retained_four_paths {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) {η : ℝ} {n : ℕ} (_hη : 0 ≤ η) (Y : Finset α) (hY : η * ↑n / 2 ≤ ↑Y.card) {x y : α} (hx : x ∈ bipartiteRetained E (η ^ 2 * ↑n / 100000) Y) (hy : y ∈ bipartiteRetained E (η ^ 2 * ↑n / 100000) Y) : η ^ 5 * ↑n ^ 3 / 40000000000 ≤ ↑(bipartiteFourPaths E x y).card

The quantitative path count at the exact source codegree threshold.

Dense four-path theorem and proper colors

theorem TrilinearHT.Auto.bipartite_dense_four_paths {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (E : α → β → Prop) {η : ℝ} {n : ℕ} (hη : 0 < η) (hα : Fintype.card α ≤ n) (hβ : Fintype.card β ≤ n) (hedges : η * ↑n ^ 2 ≤ ↑(bipartiteEdgeCount E)) : ∃ (S : Finset α), η * ↑n / 40000000000 ≤ ↑S.card ∧ ∀ x ∈ S, ∀ y ∈ S, η ^ 5 * ↑n ^ 3 / 40000000000 ≤ ↑(bipartiteFourPaths E x y).card

Blueprint lem:four-paths, lines 668-679. Both bounds use the same universal constant 1/40000000000; paths may repeat vertices.

def TrilinearHT.Auto.ProperBipartiteColoring {α : Type u_1} {β : Type u_2} {γ : Type u_3} (E : α → β → Prop) (color : α → β → γ) : Prop

Properness means that an incident color determines the opposite endpoint at a vertex in either part of a bipartite graph.

Equations

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

def TrilinearHT.Auto.bipartitePathColors {α : Type u_1} {β : Type u_2} {γ : Type u_3} (color : α → β → γ) (x y : α) (p : β × α × β) : γ × γ × γ × γ

The ordered colors along a four-step path, including the final endpoint.

Equations

• TrilinearHT.Auto.bipartitePathColors color x y p = (color x p.1, color p.2.1 p.1, color p.2.1 p.2.2, color y p.2.2)

theorem TrilinearHT.Auto.bipartite_proper_color_recovery {α : Type u_1} {β : Type u_2} {γ : Type u_3} (E : α → β → Prop) (color : α → β → γ) (hproper : ProperBipartiteColoring E color) {x y y' : α} {p q : β × α × β} (hp : E x p.1 ∧ E p.2.1 p.1 ∧ E p.2.1 p.2.2 ∧ E y p.2.2) (hq : E x q.1 ∧ E q.2.1 q.1 ∧ E q.2.1 q.2.2 ∧ E y' q.2.2) (hc : bipartitePathColors color x y p = bipartitePathColors color x y' q) : p = q ∧ y = y'

Blueprint lem:four-paths, lines 679-680: a start vertex and four ordered colors recover all three interior vertices and the final endpoint.

theorem TrilinearHT.Auto.bipartitePathColors_injOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (E : α → β → Prop) (color : α → β → γ) (hproper : ProperBipartiteColoring E color) (x y : α) : Set.InjOn (bipartitePathColors color x y) ↑(bipartiteFourPaths E x y)

Popular sums and the energy graph

def TrilinearHT.Auto.sumRepresentationCount {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (s : G) : ℕ

Number of ordered representations of a group element as a sum of two elements of the given finite set.

Equations

• TrilinearHT.Auto.sumRepresentationCount A s = {p ∈ A ×ˢ A | p.1 + p.2 = s}.card

theorem TrilinearHT.Auto.sumRepresentationCount_le {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (s : G) : sumRepresentationCount A s ≤ A.card

theorem TrilinearHT.Auto.sum_sumRepresentationCount {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) : ∑ s ∈ A + A, sumRepresentationCount A s = A.card ^ 2

theorem TrilinearHT.Auto.addEnergy_eq_sum_representation_sq {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) : A.addEnergy A = ∑ s ∈ A + A, sumRepresentationCount A s ^ 2

noncomputable def TrilinearHT.Auto.popularSums {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (t : ℝ) : Finset G

Popular sums at a real threshold; restricting to the sumset makes this finite even when the ambient abelian group is infinite.

Equations

• TrilinearHT.Auto.popularSums A t = {s ∈ A + A | t ≤ ↑(TrilinearHT.Auto.sumRepresentationCount A s)}

theorem TrilinearHT.Auto.mem_popularSums {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (t : ℝ) (s : G) : s ∈ popularSums A t ↔ s ∈ A + A ∧ t ≤ ↑(sumRepresentationCount A s)

theorem TrilinearHT.Auto.popularSums_mass_le {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (t : ℝ) : ∑ s ∈ popularSums A t, ↑(sumRepresentationCount A s) ≤ ↑A.card ^ 2

theorem TrilinearHT.Auto.popularSums_card_mul_threshold_le {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (t : ℝ) : ↑(popularSums A t).card * t ≤ ↑A.card ^ 2

theorem TrilinearHT.Auto.addEnergy_le_popular_mass {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) {t : ℝ} (ht : 0 ≤ t) : ↑(A.addEnergy A) ≤ ↑A.card * ∑ s ∈ popularSums A t, ↑(sumRepresentationCount A s) + t * ↑A.card ^ 2

Splitting at the popularity threshold bounds the energy by the popular mass times |A|, plus the threshold times the total representation mass.

theorem TrilinearHT.Auto.popularSums_card_le {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) {K : ℝ} (hK : 0 < K) : ↑(popularSums A (↑A.card / (2 * K))).card ≤ 2 * K * ↑A.card

Blueprint lem:BSG, lines 685-692: at threshold |A|/(2K), the popular sumset has at most 2K|A| elements.

theorem TrilinearHT.Auto.popularSums_mass_lower {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) {K : ℝ} (hK : 0 < K) (henergy : ↑A.card ^ 3 / K ≤ ↑(A.addEnergy A)) : ↑A.card ^ 2 / (2 * K) ≤ ∑ s ∈ popularSums A (↑A.card / (2 * K)), ↑(sumRepresentationCount A s)

The energy hypothesis forces at least |A|^2/(2K) popular ordered pairs.

def TrilinearHT.Auto.popularSumGraph {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (t : ℝ) (a b : ↥A) : Prop

Graph on two copies of A, colored by sums belonging to the popular set.

Equations

• TrilinearHT.Auto.popularSumGraph A t a b = (↑a + ↑b ∈ TrilinearHT.Auto.popularSums A t)

theorem TrilinearHT.Auto.popularSumGraph_edge_count {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (t : ℝ) : bipartiteEdgeCount (popularSumGraph A t) = ∑ s ∈ popularSums A t, sumRepresentationCount A s

theorem TrilinearHT.Auto.popularSumGraph_proper {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (t : ℝ) : ProperBipartiteColoring (popularSumGraph A t) fun (a b : ↥A) => ↑a + ↑b

theorem TrilinearHT.Auto.popularSumGraph_dense {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) {K : ℝ} (hK : 0 < K) (henergy : ↑A.card ^ 3 / K ≤ ↑(A.addEnergy A)) : 1 / (2 * K) * ↑A.card ^ 2 ≤ ↑(bipartiteEdgeCount (popularSumGraph A (↑A.card / (2 * K))))

Blueprint lem:BSG, lines 685-692: the popular-sum graph has density at least 1/(2K), and addition gives a proper edge coloring.

Encoding paths for distinct differences

theorem TrilinearHT.Auto.sumPathColors_alternating {G : Type u_1} [AddCommGroup G] {A : Finset G} (x y : ↥A) (p : ↥A × ↥A × ↥A) : have c := bipartitePathColors (fun (a b : ↥A) => ↑a + ↑b) x y p; c.1 - c.2.1 + c.2.2.1 - c.2.2.2 = ↑x - ↑y

Alternating four sum colors recovers the difference of the endpoints.

theorem TrilinearHT.Auto.popularSumGraph_difference_card_bound {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (t : ℝ) (S : Finset ↥A) (L : ℝ) (hpaths : ∀ x ∈ S, ∀ y ∈ S, L ≤ ↑(bipartiteFourPaths (popularSumGraph A t) x y).card) : ↑(Finset.image (fun (a : ↥A) => ↑a) S - Finset.image (fun (a : ↥A) => ↑a) S).card * L ≤ ↑(popularSums A t).card ^ 4

Blueprint lem:BSG, lines 693-697. For one chosen endpoint pair per difference, all four-step paths inject into ordered quadruples of popular sums. Consequently the difference count times any uniform path lower bound is at most the fourth power of the number of popular sums.

Energy to a small difference set

theorem TrilinearHT.Auto.balog_szemeredi_gowers {G : Type u_1} [AddCommGroup G] [DecidableEq G] (A : Finset G) (hA : A.Nonempty) {K : ℝ} (hK : 1 ≤ K) (henergy : ↑A.card ^ 3 / K ≤ ↑(A.addEnergy A)) : ∃ S ⊆ A, ↑A.card / (80000000000 * K) ≤ ↑S.card ∧ ↑(S - S).card ≤ 10 ^ 25 * K ^ 10 * ↑S.card

Blueprint lem:BSG, lines 683-698: if a nonempty finite subset of an abelian group has additive energy at least |A|^3/K, it has a subset of size at least |A|/(80000000000 K) whose difference set has size at most 10^25 K^10 times its own size. The two numerical constants are universal.