higgsMassSq_over_vev
plain-language theorem explainer
This definition supplies the squared Higgs mass from the quartic potential in the Q3 representation of electroweak breaking. Physicists deriving boson mass ratios from the quaternion symmetry group cite it when linking the forced quartic coupling to the vacuum expectation value. It is realized as a direct algebraic substitution of the precomputed lambda_RS into the standard Mexican-hat curvature formula.
Claim. $m_H^2 = 2 lambda_RS v^2$, where $lambda_RS = 1/2$ is the quartic coupling fixed by the second derivative of the J-cost function.
background
The module formalizes the quaternion group Q3 as the symmetry of the eight-tick cycle in Recognition Science and its role in SU(2) x U(1) to U(1) breaking. The four complex degrees of freedom of the Higgs doublet split into three Goldstone modes eaten by W and Z and one physical spin-0 Higgs. The J-cost function is defined by J(x) = (x + x^{-1})/2 - 1, whose second derivative at unity supplies the curvature that fixes the quartic term. Upstream result lambda_RS states: The phi-forced quartic coupling: lambda = J''(1)/2 = 1/2.
proof idea
One-line definition that directly substitutes the constant lambda_RS into the standard expression m_H^2 = 2 lambda v^2 taken from the Mexican-hat potential.
why it matters
The definition feeds the downstream theorem higgsMassSq_simplifies, which reduces the expression to v^2. It supplies the potential-curvature piece required by the Q3 Casimir analysis of the physical Higgs rung on the phi-ladder, consistent with T5 J-uniqueness and T7 eight-tick octave. The module doc-comment ties the result to the mass ratio m_H / m_W = 4 sqrt(lambda)/g derived from the same symmetry breaking pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.