kappa_lambda_4_RS
plain-language theorem explainer
Defines the RS prediction for the Higgs quartic self-coupling modifier as exactly 1/3. Collider phenomenologists and anyone checking the A28 cosh-vs-Mexican-hat resolution cite this constant. It is a bare real definition encoding the ratio of the h⁴ Taylor coefficients under the linear-in-ε field map.
Claim. The Recognition Science Higgs quartic modifier is the constant $\kappa_{\lambda_4}^{\mathrm{RS}} := 1/3$, equal to the ratio of the $h^4$ coefficients $m_H^2/(24v^2)$ (cosh) over $m_H^2/(8v^2)$ (SM Mexican-hat).
background
The module compares two Higgs potentials under the canonical linear identification $h = v,\varepsilon$ of HiggsEFTBridge. The RS form is $V_{\cosh}(h)=\Lambda^4(\cosh(h/v)-1)$ with $\Lambda^4=m_H^2 v^2$; the SM form after EWSB is the degree-4 Mexican-hat polynomial $V_{\mathrm{SM}}(h)=\tfrac12 m_H^2 h^2+(m_H^2/(2v))h^3+(m_H^2/(8v^2))h^4$.
Taylor expansion of the cosh yields an all-even series: quadratic matches SM, the trilinear vanishes, the quartic is $m_H^2/(24v^2)$, and a positive sextic $m_H^2/(720v^4)$ appears. The quartic ratio against SM is therefore exactly $1/3$. That ratio is the content of this definition; the companion trilinear modifier is defined as zero in the same module.
proof idea
One-line definition: the real constant is set to $1/3$. No lemmas or tactics. The equality theorem kappa_lambda_4_RS_eq_one_third is then immediate by rfl.
why it matters
This constant is one of the three numerical BSM signatures packaged in HiggsCoshBSMFalsifier: $\kappa_{\lambda_3}=0$, $\kappa_{\lambda_4}=1/3$, and $\lambda_6>0$. The module resolves attack A28 by treating the cosh/Mexican-hat mismatch as a structural, falsifiable prediction rather than a bug. Downstream, the falsifier structure records kappa_4_third : kappa_lambda_4_RS = 1/3, and the trivial theorem kappa_lambda_4_RS_eq_one_third discharges that field by reflexivity. Experimentally the quartic modifier is the target of tri-Higgs measurements (FCC-hh scale); together with the vanishing trilinear (HL-LHC di-Higgs) it distinguishes the RS cosh sector from a pure SM Mexican-hat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.