mass_term_matches_SM
plain-language theorem explainer
The theorem establishes that the quadratic coefficient in the recognition-cost potential equals m_H squared over 2 once the normalisation hypothesis sets Lambda to the fourth power equal to m_H squared times v squared. A physicist matching effective potentials between recognition geometry and the Standard Model Higgs sector would cite this when confirming the mass term dictionary. The proof is a direct algebraic reduction that unfolds the coefficient definition, substitutes the hypothesis, and simplifies.
Claim. Assuming $v > 0$ and the normalisation hypothesis $Λ^4 = m_H^2 v^2$, the quadratic coefficient extracted from the recognition potential satisfies quadratic_coefficient(Λ, v) = m_H² / 2.
background
The module formalises the link from recognition cost geometry to the Higgs effective field theory. The potential is V_RS(Λ, v, h) := Λ⁴ J(exp(h/v)), where J(x) = ½(x + x⁻¹) − 1 is the reciprocal cost functional (equivalent to cosh(ε) − 1 for ε = h/v). Taylor expansion around the vacuum produces the quadratic term (Λ⁴ / (2 v²)) h² together with the quartic term (Λ⁴ / (24 v⁴)) h⁴. The normalisation hypothesis is the defining relation Λ⁴ = m_H² v² that identifies the quadratic prefactor with the SM mass parameter.
proof idea
The proof unfolds quadratic_coefficient and the normalisation hypothesis, introduces the auxiliary fact that v squared is nonzero, rewrites by the hypothesis, and finishes with field simplification.
why it matters
This supplies the mass-term matching clause inside higgsEFTBridgeCert, the certificate that records the full RS-to-SM dictionary. It closes the first two arrows of the chain RS cost geometry to effective scalar coordinate to canonical Higgs EFT. The remaining open question is fixing Λ(v) from the φ-ladder yardstick, left explicit as a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.