higgsRungCert
The declaration certifies the Higgs rung assignment by confirming the RS-predicted Higgs mass lies in (120, 130) GeV, the Weinberg angle satisfies the interval (0.228, 0.232), and the prediction stays within 5% of the observed 125.2 GeV. Particle physicists comparing phi-ladder mass formulas to LHC data would cite this result. The proof is a term-mode record construction that directly substitutes four upstream interval theorems and the sin2ThetaW_RS_approx lemma into the HiggsRungCert structure.
claimThe RS Higgs mass satisfies $120 < m_{H,RS} < 130$ GeV, the Weinberg angle obeys $0.228 < sin^2 theta_W < 0.232$, the level-2 mass lies in (110, 125) GeV, the rung index satisfies $w < r_H < w+1$, and $|m_{H,RS} - 125.2|/125.2 < 0.05$.
background
The module derives the Higgs mass from the phi-ladder using Q3 geometry. Key quantities are mH_rs_level3 (the level-3 prediction incorporating the 17/16 correction), mH_rs_level2 (the base prediction v * sqrt(sin^2 theta_W)), sin2ThetaW_RS (equal to (3-phi)/6), and higgs_rung_from_prediction (the rung index on the mass ladder). The local setting is the broken-phase potential where lambda_physical = lambda_RS * sin^2 theta_W, yielding m_H = v * sqrt(sin^2 theta_W * (1 + 1/16)). Upstream results supply the interval theorems: mH_prediction_in_interval proves the (120,130) bound via nlinarith on phi bounds; mH_rs_level2_in_range uses linarith on (3-phi)/6; higgs_rung_in_range applies Real.log_pos; and sin2ThetaW_RS_approx establishes the 0.228-0.232 interval.
proof idea
The proof is a term-mode record construction. It populates the four fields of the HiggsRungCert structure by direct assignment: weinberg_angle from sin2ThetaW_RS_approx, level2_range from mH_rs_level2_in_range, level3_range from mH_prediction_in_interval, higgs_rung_range from higgs_rung_in_range, and within_5_percent from mH_within_5_percent_of_observed. No tactics are applied beyond the implicit unfolding in the referenced theorems.
why it matters in Recognition Science
This theorem completes the RS particle mass table for the Higgs boson and closes the hypothesis interval stated in the module doc-comment. It feeds the claim that the observed 125.2 GeV value emerges from the phi-ladder without additional free parameters beyond the T5 J-uniqueness and T6 self-similar fixed point. The result relies on the Q3Representations module for the Weinberg angle and supports the eight-tick octave structure in the mass formula. It touches the open question of formalizing the exact one-loop EW correction factor Delta lambda / lambda.
scope and limits
- Does not derive the Higgs self-coupling from the J-cost potential curvature.
- Does not include higher-order loop corrections beyond the 1/16 factor.
- Does not prove uniqueness of the rung assignment on the phi-ladder.
- Does not compute the full particle spectrum or mixing angles.
formal statement (Lean)
209theorem higgsRungCert : HiggsRungCert where
210 weinberg_angle := sin2ThetaW_RS_approx
proof body
Term-mode proof.
211 level2_range := mH_rs_level2_in_range
212 level3_range := mH_prediction_in_interval
213 higgs_rung_range := higgs_rung_in_range
214 within_5_percent := mH_within_5_percent_of_observed
215
216end
217end HiggsRungAssignment
218end StandardModel
219end IndisputableMonolith