wz_ratio_exp_comparison
plain-language theorem explainer
The theorem verifies that the squared experimental ratio of W to Z boson masses lies strictly between 0.7765 and 0.7775. Particle physicists checking electroweak mass anchors against PDG data in the Recognition Science setting would cite this numerical bound. The proof is a short tactic script that substitutes the imported constants and applies numerical normalization to confirm both sides of the inequality.
Claim. Let $r = (m_W^{exp}/m_Z^{exp})^2$. Then $0.7765 < r < 0.7775$.
background
This result appears in the BosonVerification module, whose module documentation states that experimental PDG values are quarantined constants rather than outputs of the Recognition Science derivation. The local setting imports m_W_exp and m_Z_exp as raw reals (80377 and 91188) while the sibling ElectroweakMasses module supplies slightly different rounded figures. Upstream results supply only these two constant definitions; no J-cost, defectDist, or phi-ladder computation enters the statement.
proof idea
The tactic proof first rewrites with the definitions of m_W_exp and m_Z_exp, then splits the conjunction and invokes norm_num on each side to discharge the concrete real-number inequalities.
why it matters
The bound supplies an empirical consistency check for the electroweak sector formula m(EW,r) = 2 φ^{50+r}/10^6 MeV and the Weinberg-angle relation sin²θ_W = (3-φ)/6. It anchors the imported constants used by any later comparison of phi-ladder predictions to measured W and Z masses, though the module explicitly marks these values as non-derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.