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

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.