quadratic_coefficient
plain-language theorem explainer
quadratic_coefficient supplies the prefactor of the h² term in the Taylor expansion of the recognition-cost potential V_RS around the vacuum. A physicist matching the Standard Model Higgs mass term to RS geometry would cite it to read off m_H² = Λ⁴ / v². The definition is a direct algebraic extraction from the known cosh expansion of the J-cost functional.
Claim. The quadratic coefficient of the $h^2$ term in the expansion of the recognition-cost potential $V_{RS}$ is given by $frac{Λ^4}{2 v^2}$.
background
This module formalises the first link in the chain from RS cost geometry to canonical Higgs EFT. The recognition potential is V_RS(Λ, v, h) := Λ⁴ J(exp(h/v)), where J(x) = ½(x + x⁻¹) − 1 is the canonical reciprocal cost functional (equivalent to cosh(ε) − 1 for ε = h/v). Its Taylor expansion around the vacuum h = 0 yields (Λ⁴ / (2 v²)) h² + (Λ⁴ / (24 v⁴)) h⁴ + O(h⁶). The definition isolates the quadratic prefactor to match the SM form ½ m_H² h², with the remaining normalisation hypothesis Λ(v) left explicit.
proof idea
The declaration is a direct definition that extracts the coefficient from the Taylor series of the cosh function applied to the J-cost functional.
why it matters
This definition is invoked by the master certificate HiggsEFTBridgeCert to certify the full cost-geometry to scalar-EFT map and by the matching theorem mass_term_matches_SM to confirm the SM mass term. It realises the first arrow of the RS-to-SM dictionary in the module, relying on the J-cost expansion and the eight-tick structure of the parent framework while leaving the scale-fixing hypothesis open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.