higgsRungCert
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.