IV.R87 — Range proof from Lean

The Lean module CouplingFormulas proves 2*kappa(C;3) in (0.119, 0.122) via native_decide on 6-digit rational approximations of iota_tau, bracketing the PDG value alpha_s(M_Z) = 0.1180 with a 2.4% overshoot at leading order.