higgs_rung_from_prediction
plain-language theorem explainer
The definition computes the Higgs boson rung on the phi-ladder as the W-boson rung plus the base-phi logarithm of the ratio between the level-3 RS mass prediction and the observed W mass. Recognition Science modelers cite it to locate the Higgs within the discrete mass table after the W at rung 21. The assignment is a direct unfolding of the logarithmic offset expression using the supplied mass ratio.
Claim. The Higgs rung is defined by $r_W + {}_φlog(m_{H,3}/m_{W,obs})$, where $r_W$ is the W-boson rung, $m_{H,3}$ the level-3 RS Higgs mass prediction, $m_{W,obs}$ the observed W mass, and $φ$ the golden ratio.
background
The module derives the Higgs mass from the phi-ladder using Q3 geometry to complete the RS particle mass table. The phi-ladder places masses at yardstick times $φ$ raised to (rung minus 8 plus gap), with the W boson fixed at rung 21. The Higgs rung offset follows from the mass ratio after the level-3 prediction incorporates the Weinberg angle $(3-φ)/6$ and the 1/16 Q3 correction. Upstream rung definitions appear in AnchorPolicy and Constants; the level-3 mass $mH_rs_level3$ is supplied by sibling definitions in the same module.
proof idea
This is a direct definition that adds the W rung to the base-phi logarithm of the mass ratio $mH_rs_level3$ over $mW_obs$. No lemmas are invoked beyond the real logarithm and division operations already present in the expression.
why it matters
The definition supplies the rung value consumed by HiggsRungCert to certify the predicted mass lies within 5 percent of the observed 125.2 GeV and by higgs_rung_in_range to prove the position lies strictly between 21 and 22. It fills the final step of the Higgs mass hypothesis in the module document, which closes the (120,130) GeV interval. The construction rests on the phi self-similar fixed point and the mass formula from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.