PFR endgame: bound the comparison terms through product fibres to get eta = 1/8 (2K^11 in F_2^n)

In the GGMT endgame (char 2), construct-good on U = X1+X2, V = X~1+X2 conditioned on (S, W), W = X1+X~1, needs the comparison terms d(p1; U|S,W) + d(p2; V|S,W). GGMT bound them through d(U, U~) and get k <= (8 eta + eta^2) k, hence eta = 1/9 and 2K^12. Better: the fibres of (S, W) are exactly the fibres of (W, W-bar), W-bar = X2+X~2, and those are product measures (X1,X~1)|W tensor (X2,X~2)|W-bar. On each product fibre, Kaimanovich-Vershik plus the translation X~1 = w + X1 give d(p1; X+Y) + d(p2; X'+Y) <= d(p1;X) + d(p2;Y) + d(X;Y). Averaged, the last term is d(X1|W; X2|W-bar), which the second-estimate fibring bounds by k + eta D/2 - I2. Result: k <= (8 eta - eta^2) k, so eta = 1/8 works, giving entropic d(U_A,U_H) <= 5 log K and 2K^11 cosets. Liao (arXiv:2404.09639) reaches eta < 1/8 using all three triples and gets 2K^9 with a KL-divergence functional. Lean tip: relabel fibres with an Equiv e(a,b) = (a+b, a) and Equiv.sum_comp, and transport the laws with a weight-preserving coordinate permutation.