higgsEFTBridgeCert
plain-language theorem explainer
The higgsEFTBridgeCert definition assembles the master certificate that maps the recognition cost potential V_RS to the canonical Higgs EFT by bundling theorem-backed properties. A physicist closing the RS-to-Standard-Model dictionary for the Higgs mass and quartic coupling would cite it when instantiating the bridge structure. It is a direct structure constructor that supplies each field from pre-proved results on vacuum vanishing, non-negativity, cosh equivalence, quartic remainder, and SM matching.
Claim. The Higgs EFT bridge certificate is the structure asserting that the potential $V_{RS}(Λ, v, h) = Λ^4 J(e^{h/v})$ satisfies $V_{RS}(Λ, v, 0) = 0$, $0 ≤ V_{RS}(Λ, v, h)$ for all $h$, $V_{RS}(Λ, v, h) = Λ^4 (cosh(h/v) - 1)$, a uniform sextic remainder bound on the quartic Taylor expansion for $|h| ≤ v/2$, the quadratic coefficient equals $m_H^2/2$ under the normalization hypothesis, and the quartic coefficient yields $λ_{SM} = m_H^2/(6 v^2)$ under the same hypothesis.
background
The module formalizes the chain from RS cost geometry to effective scalar coordinate to canonical Higgs EFT. The dimensionless coordinate is ε = h/v with v the electroweak scale from the recognition substrate; the dimensionful prefactor Λ^4 restores SM normalization. The recognition-cost potential is defined as V_RS Λ v h := Λ^4 · J(exp(h/v)) where J(x) = ½(x + x^{-1}) - 1 is the canonical reciprocal cost functional, equivalently J(e^ε) = cosh ε - 1. Expanded around the vacuum this yields the quadratic and quartic terms that are matched to the SM form ½ m_H² h² + (λ_SM/4) h^4. The structure HiggsEFTBridgeCert records the master certificate whose clauses are theorems except where they depend on the explicit NormalizationHypothesis Λ v m_H.
proof idea
This definition is a direct structure constructor. It supplies vacuum_zero by V_RS_at_vacuum, nonneg by V_RS_nonneg, cosh_form by V_RS_eq_cosh, quartic_remainder by V_RS_quartic_error, mass_term_match by mass_term_matches_SM, and quartic_match by quartic_coupling_from_normalization. Each referenced theorem is already proved in the same module from the Jcost_exp_cosh identity and the cosh Taylor expansion.
why it matters
The certificate closes the first two arrows of the RS cost geometry to SM Higgs EFT map and is used directly by higgsEFTLowEnergyLimitCert to bundle the full low-energy limit. It realizes the mapping from J-uniqueness (T5) through the cosh form to the SM mass and quartic parameters, leaving the normalization hypothesis Λ^4 / v² = m_H² explicit for later substrate closure. The construction confirms that the recognition potential reproduces the SM Higgs sector up to controlled higher-order remainders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.