row_WZ_ratio_bracket
plain-language theorem explainer
The row_WZ_ratio_bracket theorem certifies that the W to Z boson mass ratio from PDG inputs satisfies 0.87 < m_W/m_Z < 0.89. It is cited by the WZBosonRatioScoreCardCert construction in the same module when assembling experimental brackets for Recognition Science comparisons. The proof is a one-line wrapper that directly references the numeric bound theorem in StandardModel.WZMassRatio.
Claim. The W/Z boson mass ratio satisfies $0.87 < m_W/m_Z < 0.89$.
background
The module supplies numeric bounds on m_W/m_Z and sin²θ_W using PDG display values m_W = 80.377 GeV and m_Z = 91.1876 GeV. massRatio is defined as m_W/m_Z in StandardModel.WZMassRatio. This declaration acts as a data-interface certificate for Phase 2 P2-WZ, distinct from the RS-derived Weinberg angle formula sin²θ_W = (3-φ)/6 proved in Q3Representations and WeinbergAngleScoreCard.
proof idea
One-line wrapper that directly invokes the mass_ratio_value theorem from IndisputableMonolith.StandardModel.WZMassRatio, which unfolds the definitions of massRatio, m_W and m_Z then applies norm_num to obtain the strict inequalities.
why it matters
It supplies the mass_ratio field to wzBosonRatioScoreCardCert_holds, which builds the scorecard certificate. The bracket anchors experimental input for Recognition Science comparisons to phi-ladder mass formulas and the eight-tick octave. The RS-specific sin²θ_W formula is handled elsewhere; this file only certifies the PDG-derived interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.