higgs_rung_prediction
plain-language theorem explainer
The declaration defines the fractional rung offset Δ such that the physical Higgs mass satisfies m_H/m_W = φ^Δ in the Q₃ representation of electroweak breaking. Recognition Science model builders cite it when placing the spin-0 Higgs mode on the φ-ladder relative to the W boson at rung 21. The definition evaluates Δ by direct arithmetic: bind sin²θ_W to (3-φ)/6, form the ratio 2 sin²θ_W (v/m_W)²/(1-2 sin²θ_W) with v=246 GeV and m_W≈80.4 GeV, then take the base-φ logarithm.
Claim. Δ := log_φ (2 sin²θ_W (v/m_W)² / (1-2 sin²θ_W)) where sin²θ_W = (3-φ)/6, v=246 GeV and m_W=80.377 GeV, so that m_H/m_W = φ^Δ.
background
The module treats the quaternion group Q₃ as the symmetry of the eight-tick recognition cycle. Under SU(2)×U(1)→U(1) the Higgs doublet splits into three Goldstone modes (longitudinal W,Z) carrying the spin-1 Casimir eigenvalue 2 and one physical spin-0 Higgs carrying eigenvalue 0. The rung offset Δ arises from the curvature J''(1)=1 of the recognition potential together with the gauge coupling expressed through sin²θ_W.
proof idea
The definition is a direct term-mode computation. It lets s2 := sin2ThetaW_RS, computes ratio_sq := 2s2(246/80.4)²/(1-2*s2), and returns Real.log ratio_sq / Real.log phi. No external lemmas are invoked beyond the field operations and the logarithm; the numerical constants are the conventional electroweak vacuum expectation value and W mass.
why it matters
It supplies the explicit Δ required by the Q₃ spin-0/spin-1 mass formula and is invoked by the downstream theorem higgs_rung_prediction_pos to prove positivity. In the Recognition Science chain it realizes the T7 eight-tick octave and the φ-ladder placement of the Higgs once the loop-renormalized quartic coupling is inserted; the module doc-comment notes that the exact observed ratio still needs the full one-loop electroweak correction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.