`PFR/EntropyPFR.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 9 curated AI-written annotations and 485 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Polynomial Freiman-Ruzsa proof paper, arXiv v2

2 declarations, 0 contain sorry, 0 declared as axioms

Entropic version of polynomial Freiman-Ruzsa conjecture

Here we prove the entropic version of the polynomial Freiman-Ruzsa conjecture.

Main results

entropic_PFR_conjecture: For two $G$-valued random variables $X_1^0, X_2^0$, there is some subgroup $H \leq G$ such that $d[X_1^0;U_H] + d[X_2^0;U_H] \le 11 d[X_1^0;X_2^0]$, and both $d[X_1^0;U_H]$ and $d[X_2^0;U_H]$ are at most $6 d[X_1^0;X_2^0]$.

Imports (4)

Imported by 2 files

theorem tau_strictly_decreases If $d[X_1;X_2] > 0$ then there are $G$-valued random variables $X'_1, X'_2$ such that $\tau[X'_1;X'_2] < \tau[X_1;X_2]$ line 39 source
Source documentation
If $d[X_1;X_2] > 0$ then there are $G$-valued random variables $X'_1, X'_2$ such that $\tau[X'_1;X'_2] < \tau[X_1;X_2]$. Phrased in the contrapositive form for convenience of proof.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Finite, MeasurableSpace, MeasurableSingletonClass, refPackage, Measurable, TauMinimizes, Eq, Real, refPackage.η, HDiv.hDiv, rdist
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Exists, MeasureTheory.Measure, And, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies4_nondep, Eq.mpr, id, congrArg, Eq.symm, ProbabilityTheory.IdentDistrib.rdist_congr, MeasureTheory.MeasureSpace.mk and 7 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem tau_strictly_decreases (h_min : TauMinimizes p X₁ X₂) (hpη : p.η = 1 / 9) :
    d[X₁ # X₂] = 0 := by
…
```
Mentions: TauMinimizes
theorem entropic_PFR_conjecture Entropic PFR (constants 11 and 6) line 54 source
Source documentation
entropic_PFR_conjecture: For two $G$-valued random variables $X_1^0, X_2^0$, there is some subgroup $H \leq G$ such that $d[X_1^0;U_H] + d[X_2^0;U_H] \le 11 d[X_1^0;X_2^0]$, and both $d[X_1^0; U_H]$ and $d[X_2^0; U_H]$ are at most $6 d[X_1^0;X_2^0]$.
L4DEL explanation
Any two random variables in an F2-vector space are within a constant multiple of their Ruzsa distance of a uniform distribution on some subgroup.
1. Statement: for finite G of characteristic 2 and a package of two G-valued variables X01, X02 with parameter eta = 1/9, there is a subspace H and a uniform variable U on H with d[X01 ; U] + d[X02 ; U] at most 11 d[X01 ; X02], and each of d[X01 ; U] and d[X02 ; U] at most 6 d[X01 ; X02].
2. Take a pair X1, X2 minimizing the tau functional (tau_minimizer_exists). The theorem tau_strictly_decreases then forces d[X1 ; X2] = 0 when eta = 1/9.
3. Zero Ruzsa distance means X1 and X2 are uniform on cosets of a common subgroup (exists_isUniform_of_rdist_eq_zero), which gives H and U.
4. The distances from the original variables to U follow from minimality of tau and the Ruzsa triangle inequality (rdist_triangle), finished by linear arithmetic.
Prerequisites: tau_minimizer_exists, tau_strictly_decreases, rdist_triangle, exists_isUniform_of_rdist_eq_zero
See also: entropic_PFR_conjecture_improv
Sources and attribution: Pinned Lean source (ce7ac95e620a)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Finite, MeasurableSpace, MeasurableSingletonClass, refPackage, Eq, Real, refPackage.η, HDiv.hDiv, Exists, Submodule, And, Measurable and 7 more
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, TauMinimizes, tau_minimizer_exists, tau_strictly_decreases, AddSubgroup, exists_isUniform_of_rdist_eq_zero, Prod, rdist_symm, tau, is_tau_min, refPackage.hmeas2, refPackage.hmeas1, rdist_triangle, Exists.intro, OrderIso, AddSubgroup.toZModSubmodule, inferInstance and 97 more
135 instances, coercions and auxiliary constants left out.

tau functional: tau[X1 ; X2] = d[X1 ; X2] + eta d[X01 ; X1] + eta d[X02 ; X2], where X01 and X02 are the fixed reference variables of the package; minimizing it is the engine of the entropic proof.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem entropic_PFR_conjecture (hpη : p.η = 1 / 9) :
    ∃ H : Submodule (ZMod 2) G, ∃ Ω : Type uG, ∃ mΩ : MeasureSpace Ω, ∃ U : Ω → G,
    IsProbabilityMeasure (ℙ : Measure Ω) ∧ Measurable U ∧
    IsUniform H U ∧ d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 11 * d[p.X₀₁ # p.X₀₂] ∧
      d[p.X₀₁ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂] ∧
      d[p.X₀₂ # U] ≤ 6 * d[p.X₀₁ # p.X₀₂] := by
…
```