V_RS_quartic_canonical
plain-language theorem explainer
The theorem states that the quartic Taylor truncation of the recognition-cost potential equals the sum of its quadratic and canonical quartic coefficients times the appropriate powers of the field. Effective-field theorists matching scalar potentials to collider data would invoke this identity to equate recognition-derived coefficients with Standard-Model parameters. The proof is a direct algebraic reduction: unfold the three definitions, confirm the nonzero powers of v, then simplify by field operations.
Claim. Let $V_{RS,quartic}(Λ,v,h)$ be the quartic truncation $Λ^4·((h/v)^2/2+(h/v)^4/24)$. Then $V_{RS,quartic}(Λ,v,h)=q(Λ,v)·h^2+c(Λ,v)·h^4$ for all real $Λ,h$ whenever $v≠0$, where $q$ and $c$ are the quadratic and canonical quartic coefficients extracted from the same truncation.
background
The module constructs the first link of the RS-to-Standard-Model dictionary. The recognition-cost potential is defined as $V_{RS}(Λ,v,h):=Λ^4·J(exp(h/v))$ with the canonical cost $J(x)=(x+x^{-1})/2-1$. Its Taylor expansion about the vacuum yields the quartic truncation $V_{RS,quartic}(Λ,v,h):=Λ^4·((h/v)^2/2+(h/v)^4/24)$. The sibling definitions quadratic_coefficient and quartic_coefficient_canonical are precisely the prefactors $Λ^4/(2v^2)$ and $Λ^4/(24v^4)$ that appear once the expression is written in canonical Higgs-EFT form. Upstream, the expansion itself rests on the identity $J(e^ε)=cosh ε-1$ proved in Cost.Jcost_exp_cosh.
proof idea
The term proof unfolds V_RS_quartic together with the two coefficient definitions. It records the auxiliary facts $v^2≠0$ and $v^4≠0$ by direct application of pow_ne_zero. Field_simp then cancels the common denominator $v^4$ and equates the resulting rational expression with the target quadratic-plus-quartic polynomial.
why it matters
This identity supplies the explicit coefficient map required by the module's Standard-Model dictionary: $m_H^2=Λ^4/v^2$ and $λ_{SM}=(1/6)Λ^4/v^4$. It therefore closes the first two arrows of the RS-cost-geometry to canonical-Higgs-EFT chain described in the module header. The remaining open step is the collider normalisation that would fix $Λ(v)$ from the φ-ladder yardstick; the theorem leaves that hypothesis explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.