higgs_rung_in_range
plain-language theorem explainer
The theorem establishes that the predicted Higgs boson rung on the phi-ladder lies strictly between 21 and 22. Researchers completing the Recognition Science mass table for Standard Model particles would cite this when certifying the Higgs tier assignment. The proof reduces the interval claim to logarithmic inequalities by unfolding the prediction, invoking the positivity of log phi, and applying linarith together with the golden-ratio identity phi squared equals phi plus one.
Claim. Let $r_H = (1 / log phi) * log (m_{H,RS} / 80.4)$ denote the predicted Higgs rung. Then $21 < r_H < 22$.
background
In Recognition Science, masses occupy discrete rungs on the phi-ladder via the formula yardstick times phi to the power (rung minus 8 plus gap). The Higgs assignment uses the Q3 geometry and the Weinberg angle sin squared theta_W equals (3 minus phi) over 6, together with a one-loop correction factor of order 1/16, to place m_H near 125 GeV. The module derives the interval (120, 130) GeV as a hypothesis that closes the mass table. Upstream lemmas supply the strict lower bound phi greater than 1.61 and the identity phi squared equals phi plus one, both required to bound the logarithm that defines the rung.
proof idea
The tactic proof unfolds higgs_rung_from_prediction, w_rung and mW_obs. It obtains positivity of log phi from the lemma phi_gt_onePointSixOne. From mH_prediction_in_interval it derives the ratio mH_rs_level3 over 80.4 exceeds 1. The lower bound follows by linarith on the quotient of the two logs. For the upper bound the proof invokes phi_sq_eq to obtain phi greater than 1.617, shows the ratio is less than phi, applies Real.log_lt_log, and concludes via linarith that the rung increment is less than 1.
why it matters
The result supplies the rung-range field inside the downstream theorem higgsRungCert, which also records the Weinberg angle, the level-2 and level-3 mass intervals, and the five-percent agreement with the observed 125.2 GeV. It thereby completes the RS particle-mass table and discharges the open question on the Higgs interval stated in the module documentation. The argument rests on the phi-forcing chain (T5 J-uniqueness and T6 self-similar fixed point) and the eight-tick octave structure that fixes D equals 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.