z_mass_bounds
plain-language theorem explainer
The theorem shows that the predicted Z boson mass lies strictly between 91075.09 and 91075.10 MeV. Researchers modeling electroweak masses via the phi-ladder in Recognition Science cite this interval to anchor the Z placement at rung 1. The tactic proof substitutes the explicit formula for the prediction and verifies the bounds through division rewriting together with arithmetic comparisons that invoke pre-established inequalities on phi to the 51st power.
Claim. $91075.09 < m_Z^{pred} < 91075.10$ (in MeV), where the prediction is given by $m_Z^{pred} = 2 phi^{51} / 10^6$.
background
Electroweak boson masses are assigned to discrete rungs on the phi-ladder. The Z boson occupies rung 1 in this sector, yielding the mass formula $m_Z = 2 phi^{51} / 10^6$ MeV. The module differentiates Z from W and Higgs by applying the Weinberg angle relation derived from the Recognition Composition Law, with $sin^2 theta_W = (3 - phi)/6$. Upstream structures supply the J-cost calibration and ledger factorization that ground the discrete tiers used in the ladder.
proof idea
The proof first rewrites the Z prediction via its defining equality. It splits the conjunction into separate lower and upper bounds. Each bound is reduced by applying the division inequality rule, followed by a calculation chain that invokes norm_num for exact arithmetic and nlinarith on the pre-proved lower and upper bounds for phi to the 51st power.
why it matters
This bound is collected inside the electroweak certification theorem that also packages the relative error to experiment and the W/Z ratio equality. It realizes the mass formula at rung 1 for the Z boson, consistent with the self-similar fixed point phi from T6 and the eight-tick octave from T7. The result closes numerical verification for the electroweak sector without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.