row_mH_within_five_percent
plain-language theorem explainer
The theorem asserts that the Recognition Science level-3 Higgs mass prediction lies within five percent of the observed 125.2 GeV value. Particle physicists comparing RS mass ladders to PDG data would cite this scorecard entry. The proof is a one-line simpa wrapper that substitutes the codata alias for the observed mass into the upstream interval theorem.
Claim. $ |m_{H,RS}^{(3)} - m_{H,obs}| / m_{H,obs} < 0.05 $, where $ m_{H,RS}^{(3)} = v · √(sin²θ_W · 17/16) $ with $ v = 246 $ GeV and $ sin²θ_W = (3-φ)/6 $.
background
The module supplies a Phase 2 scorecard for the Higgs mass under Recognition Science. The level-3 prediction is defined as vev times the square root of sin²θ_W times 17/16; the factor 17/16 encodes the Q₃ mode budget of 16 addressing modes plus the physical Higgs singlet. The observed mass 125.2 GeV is aliased via row_mH_codata for uniform row formatting. Upstream, mH_within_5_percent_of_observed proves the same inequality directly against mH_obs by unfolding the observed value and applying the interval bounds (120,130) GeV.
proof idea
The proof is a one-line wrapper that applies simpa with the row_mH_codata substitution and then invokes the upstream theorem mH_within_5_percent_of_observed.
why it matters
This declaration supplies the 5% proximity check required by the HiggsMassScoreCardCert. It confirms the RS prediction against observation inside the (120,130) GeV window given in the module doc-comment. The result closes one scorecard row in the P2-HIGGS chain while leaving the vev display anchor open for later unification with the Fermi-constant row.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.