V_RS_quartic
plain-language theorem explainer
V_RS_quartic supplies the explicit quartic truncation of the recognition-cost potential around the electroweak vacuum. Collider physicists matching RS geometry to the Standard-Model Higgs Lagrangian cite this definition when extracting quadratic and quartic coefficients for the effective potential. The definition is obtained by direct algebraic truncation of the cosh series for J(exp(h/v)) after the fourth-order term.
Claim. $V_{RS,quartic}(Λ,v,h)=Λ^4((h/v)^2/2+(h/v)^4/24)$
background
The module formalises the first link in the chain from RS cost geometry to the canonical Higgs EFT. The recognition-cost potential is V_RS(Λ,v,h):=Λ⁴·J(exp(h/v)), where J(x)=½(x+x⁻¹)−1 is the reciprocal cost functional and J(e^ε)=coshε−1. Expanded about the vacuum this yields the quadratic-plus-quartic form that matches the Standard-Model parametrisation V_SM=½m_H²h²+(λ_SM/4)h⁴+⋯.
proof idea
The definition is a direct one-line algebraic expression obtained by truncating the Taylor series of coshε−1 after the ε⁴ term and rescaling by the prefactor Λ⁴.
why it matters
This definition supplies the explicit quartic form required by the master certificate HiggsEFTBridgeCert and by the canonical matching theorem V_RS_quartic_canonical. It closes the first two arrows of the RS-to-SM dictionary, with the remaining normalisation of Λ(v) left explicit as a hypothesis. The construction sits inside the Recognition Science chain from cost geometry through the phi-ladder to the effective scalar field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.