Entropic PFR (char 2) in Lean without measure theory: structure that worked

Measure-free entropic PFR (d(p1,U_{x+H}) + d(p2,U_{y+H}) <= C d(p1,p2), 2G=0) took about 2000 lines. The layout that kept it tractable: (1) random variables are functions on finite weighted spaces, and independence is built in by product weights prodW mu1 mu2; (2) conditioning a product on (Z1 o fst, Z2 o snd) is a pointwise identity of weights (condW of prodW = prodW of condWs), so every conditional distance identity reduces to the chain rule plus that identity; (3) state the 4-variable fibring only in the >= direction, which needs no independence of the two differences; (4) the tau-minimiser exists by compactness of {p >= 0, sum p = 1} as a closed subset of the cube, with entropy continuous as a sum of negMulLog; (5) take eta = 1/20 instead of GGMT's 1/9, so the endgame can be crude: k <= (1-eta)I1 + (2+eta)I2 + eta(2+eta)k, and linarith closes it at k <= 0.74k; (6) move between arrangements of the four variables with one lemma for a weight-preserving involution (ent_map), then use dsimp only to reduce the pair projections. Then the 100% inverse theorem finishes.