HiggsRungCert
plain-language theorem explainer
HiggsRungCert packages five numerical checks that place the Recognition Science Higgs-mass prediction inside the observed 125.2 GeV value to within 5 percent. Model builders comparing RS spectra to LHC data cite the certificate when they need a compact record of the Weinberg-angle interval, the level-2 and level-3 mass windows, the rung assignment, and the relative-error bound. The structure is assembled by direct substitution of the already-proved interval lemmas; no further reduction is performed.
Claim. A structure asserting $0.228 < sin^2 theta_W < 0.232$, $110 < m_{H, level2} < 125$, $120 < m_{H, level3} < 130$, $w < r_H < w+1$ for the assigned rung $r_H$, and $|m_{H, level3} - 125.2|/125.2 < 0.05$.
background
Recognition Science obtains the Higgs mass from the phi-ladder after Q3 geometry fixes the electroweak vev and the Weinberg angle. The module states that $m_H^2 = sin^2 theta_W * v^2$ with the one-loop factor $1 + 1/16$, where $sin^2 theta_W = (3-phi)/6$. The structure collects the resulting interval statements, the rung placement between consecutive integers, and the 5 percent agreement test against the observed mass. Upstream lemmas supply the rung function and the J-cost curvature that forces lambda = 1/2 before the symmetry-breaking correction is applied.
proof idea
The declaration is a plain structure definition. Its five fields are filled by direct reference to the pre-proved theorems sin2ThetaW_RS_approx, mH_rs_level2_in_range, mH_prediction_in_interval, higgs_rung_in_range and mH_within_5_percent_of_observed. No tactics or reductions occur inside the structure itself.
why it matters
The certificate is the final packaging step consumed by the theorem higgsRungCert, which closes the Higgs-mass section of the Standard Model table. It realizes the module hypothesis that m_H lies in (120, 130) GeV and thereby completes the mass assignment after the eight-tick octave and D = 3 forcing steps. The 5 percent empirical anchor is required before the mass formula can be exported to astrophysical or cosmological calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.