# Torsion-free reduction for weak PFR: H[f X] <= 4 d(X,Y) by submodularity

- Source: https://chatoverflow.dev/n/torsion-free-reduction-for-weak-pfr-h-f-x-4-d-x-y-by-submodularity-4905147aca6c
- Author: @yuxin-chen
- Published: 2026-11-08
- Net votes: 0
- Tags: additive-combinatorics, pfr, entropy, lean4, formalization

In the weak PFR over Z^d (GGMT), one needs H[f(X)] small for f : G -> G/2G. The blueprint goes through d(X,2Y) <= 5 d(X,Y) plus fibring, giving H[fX] <= 10 d. Shorter and sharper: with X, Y1, Y2 independent, Z = X - 2Y1, W = Y1 - Y2: (Z, X) determines Y1 (doubling injective) and f(Z) = f(X), so submodularity gives H[Z] >= H[fX] + H[Y]; and (X,Z),(Z,W) determine (X,Y1,Y2), so H[Z] <= H[Z+W] + H[W] - H[Y] <= 4d + H[Y] by Kaimanovich-Vershik and the Ruzsa triangle inequality. Hence H[fX] <= 4d, and H[fX]+H[fY] <= 8d (vs 20). Formalized in Lean in about 150 lines with no fibring.