HiggsMassScoreCardCert
plain-language theorem explainer
HiggsMassScoreCardCert packages the two inequalities that place the Recognition Science level-3 Higgs mass inside the open interval (120,130) GeV and within 5 percent of the observed 125.2 GeV value. A physicist checking the RS mass ladder against PDG data would cite the certificate when documenting the P2-HIGGS scorecard. The declaration is a pure structure definition that simply bundles the interval and relative-error predicates with no computational steps.
Claim. Let $m_H^{(3)}$ denote the Recognition Science level-3 Higgs mass prediction and $m_H^obs$ the observed value 125.2 GeV. The certificate asserts $120 < m_H^{(3)} < 130$ and $|m_H^{(3)} - m_H^obs| / m_H^obs < 0.05$.
background
The module Physics.HiggsMassScoreCard implements the phase-2 Higgs mass scorecard. The upstream definition mH_obs supplies the constant observed mass 125.2 GeV. The companion definition mH_rs_level3 supplies the RS prediction $m_H = v · √(sin²θ_W · 17/16)$, where the factor 17/16 encodes the Q₃ mode budget (16 addressing modes plus the physical Higgs singlet). The module doc states that v = 246 GeV remains a display anchor while sin²θ_W = (3-φ)/6 is taken from the RS forcing chain.
proof idea
The declaration is a structure definition with an empty proof body. It directly encodes the two field predicates mass_interval and five_percent by referencing the upstream constants mH_rs_level3 and mH_obs; no lemmas or tactics are applied.
why it matters
The structure is the certificate object constructed inside the downstream theorem higgsMassScoreCardCert_holds, which proves the structure is inhabited. This step closes the numerical verification portion of the P2-HIGGS scorecard, confirming the phi-derived prediction lies near the observed mass while leaving the vev as a display parameter. It therefore supplies the concrete data check required by the Recognition Science mass-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.