mass_ratio_value
plain-language theorem explainer
Electroweak modelers cite the bound 0.87 < m_W/m_Z < 0.89 when validating Recognition Science predictions for the Weinberg angle. The declaration supplies this interval using the module's numerical mass assignments. Its term proof unfolds the ratio definition and checks the bounds directly with norm_num.
Claim. $0.87 < m_W / m_Z < 0.89$, where $m_W = 80.377$ GeV and $m_Z = 91.1876$ GeV.
background
The StandardModel.WZMassRatio module assigns the experimental values 80.377 GeV and 91.1876 GeV to the W and Z boson masses. It defines the mass ratio as their quotient and places the result inside the SM-003 section on W/Z mass ratio from phi-structure, where the ratio equals cos of the Weinberg angle. Upstream massRatio definitions appear in GaugeBosonMassesFromRS as 6/(3 + phi) and in ThreeGenerations as phi, supplying the phi-based context for this numerical verification.
proof idea
The term proof unfolds massRatio to the quotient of the two mass definitions, splits the conjunction with constructor, and verifies each side of the interval with norm_num on the concrete reals.
why it matters
The result supplies the concrete bound used by row_WZ_ratio_bracket in the WZBosonRatioScoreCard module. It fills the numerical verification step in the SM-003 paper proposition on electroweak parameters from RS, linking to the phi-constrained gauge mixing and the observed ratio near 0.881. It touches the open question of deriving the exact masses from the phi-ladder rather than inserting experimental values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.