quartic_coefficient_canonical
plain-language theorem explainer
The quartic coefficient in the Taylor expansion of the recognition cost potential around the vacuum is given by Λ⁴/(24 v⁴). Physicists matching RS cost geometry to the Standard Model Higgs EFT cite this to fix the interaction term in the effective Lagrangian. It follows directly from the algebraic series expansion of the J-cost functional J(exp(h/v)) = cosh(h/v) - 1.
Claim. The quartic coefficient in the canonical Higgs potential is given by the expression $Λ^4 / (24 v^4)$.
background
The Higgs EFT Bridge module defines the recognition cost potential as V_RS(Λ, v, h) := Λ⁴ J(exp(h/v)), where J(x) = (x + x^{-1})/2 - 1 is the reciprocal cost functional satisfying the Recognition Composition Law. Around the vacuum h = 0 this expands as (Λ⁴/(2 v²)) h² + (Λ⁴/(24 v⁴)) h⁴ + O(h⁶), which is matched to the Standard Model form ½ m_H² h² + (λ_SM/4) h⁴. The module states that the Taylor-coefficient extraction is forced by the cosh expansion from Cost.Jcost_exp_cosh together with Mathlib series results.
proof idea
This is a direct algebraic definition that isolates the h⁴ coefficient from the known Taylor series of cosh. No lemmas are applied beyond the definition of the J-cost functional and the elementary power-series identity for cosh ε - 1.
why it matters
The coefficient is used inside HiggsEFTBridgeCert to certify the full cost-geometry to scalar-EFT map and inside quartic_coupling_from_normalization to obtain λ_SM = m_H²/(6 v²) under the normalization hypothesis. It supplies the explicit link from RS cost geometry (J-uniqueness and the eight-tick octave) to the canonical Higgs EFT, closing the first two arrows of the reviewer chain while leaving the fixing of Λ(v) as an explicit hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.