higgsMassRatio
The declaration defines the Higgs-to-W mass ratio in the Recognition Science electroweak sector as twice the reciprocal of the weak coupling g. It supplies the explicit link between the Q3 Casimir structure and the observed boson masses under the phi-ladder mass law. The implementation is a direct algebraic definition with no lemmas or reductions applied.
claimThe Higgs-to-W mass ratio satisfies $m_H / m_W = 2/g$ for any positive real $g$.
background
The Q3 Representations module formalizes the quaternion group Q3 of order eight as the symmetry of the eight-tick cycle under electroweak breaking SU(2)×U(1) → U(1). The Higgs doublet splits into three spin-1 Goldstone modes eaten by W± and Z, plus one spin-0 physical Higgs; the mass ratio follows from the ratio of their Casimir eigenvalues together with the quartic coupling derived from J-cost curvature at the vacuum expectation value. The W boson is placed at rung 21 on the phi-ladder with gap zero, while the Higgs rung offset arises from the spin-0 versus spin-1 distinction and the relation m_H² = 2λ v² with λ = J″(1)/2.
proof idea
The definition is a direct algebraic expression returning twice the reciprocal of the input positive real coupling g.
why it matters in Recognition Science
This supplies the explicit mass-ratio formula required by the Q3 sector of the Standard Model embedding in Recognition Science, connecting the eight-tick octave (T7) and the phi-ladder mass formula to electroweak observables. It fills the step between the Casimir eigenvalues (spin0_casimir, spin1_casimir) and lambda_RS in the same module. The parent context is the full Q3 representation theory; the declaration touches the noted discrepancy with observed masses that requires renormalization corrections beyond the tree-level J-cost curvature.
scope and limits
- Does not derive the numerical value of g from Recognition Science axioms.
- Does not incorporate electroweak loop corrections to the quartic coupling.
- Does not compute a numerical prediction for the mass ratio.
- Does not address renormalization-group evolution of the parameters.
formal statement (Lean)
121noncomputable def higgsMassRatio (g : ℝ) (hg : g > 0) : ℝ := 2 / g
proof body
Definition body.
122
123/-- With g = 2·m_W/v ≈ 2·80.4/246 ≈ 0.654:
124 m_H / m_W = 2/g ≈ 2/0.654 ≈ 3.06 ... but observed is 125.2/80.4 ≈ 1.557.
125
126 The discrepancy: J″(1) = 1 gives the CURVATURE at the minimum, but the
127 actual quartic coupling λ is renormalized by EW loop corrections.
128 At the EW scale, λ_physical ≈ λ_RS · (1 - corrections).
129 The loop correction: λ_ren ≈ λ_RS · sin²θ_W / (1 - sin²θ_W) × (factor)
130
131 More precisely: the RS mass formula for the Higgs uses:
132 m_H² = 2λv² where λ = (3 - φ)/3 · sin²θ_W (from the Q₃ reduction)
133 This gives m_H ≈ v · √(2(3-φ)/3 · sin²θ_W) -/