HiggsEFTBridgeCert
plain-language theorem explainer
The HiggsEFTBridgeCert packages the analytic properties of the recognition potential V_RS(Λ, v, h) = Λ⁴ (cosh(h/v) - 1), specifically its vanishing at h=0, non-negativity, exact cosh expression, and a sextic-error bound on the quartic Taylor approximation for |h| ≤ v/2. It further records that the quadratic and quartic coefficients match the Standard-Model Higgs mass term and coupling λ_SM under the normalisation hypothesis Λ⁴ = m_H² v². A collider phenomenologist embedding recognition geometry into the Higgs sector would cite this certificate.
Claim. A structure consisting of: vacuum_zero: ∀ Λ, v, V_RS(Λ, v, 0) = 0; nonneg: ∀ Λ, v, h, V_RS(Λ, v, h) ≥ 0; cosh_form: ∀ Λ, v, h, V_RS(Λ, v, h) = Λ⁴ (cosh(h/v) - 1); quartic_remainder: ∀ Λ, v, h with 0 < v and |h| ≤ v/2, |V_RS(Λ, v, h) - V_RS_quartic(Λ, v, h)| ≤ |Λ|⁴ exp(|h/v|) |h/v|⁶; mass_term_match: under NormalizationHypothesis(Λ, v, m_H) with 0 < v, quadratic_coefficient(Λ, v) = m_H²/2; quartic_match: under the same hypothesis, 4 · quartic_coefficient_canonical(Λ, v) = m_H²/(6 v²). Here V_RS(Λ, v, h) := Λ⁴ J(exp(h/v)) with J(x) = ½(x + x⁻¹) - 1 and NormalizationHypothesis(Λ, v, m_H) asserts Λ⁴ = m_H² v².
background
The module formalises the first link RS cost geometry → effective scalar coordinate → canonical Higgs EFT. The potential is V_RS(Λ, v, h) := Λ⁴ J(exp(h/v)), where J(x) = ½(x + x⁻¹) - 1 equals cosh(h/v) - 1. Expanded about the vacuum this yields (Λ⁴/(2 v²)) h² + (Λ⁴/(24 v⁴)) h⁴ + O(h⁶). Matching to the SM form ½ m_H² h² + (λ_SM/4) h⁴ produces the dictionary m_H² = Λ⁴/v² and λ_SM = (1/6) Λ⁴/v⁴. The normalisation hypothesis Λ⁴ = m_H² v² is left explicit as the open collider-normalisation step.
proof idea
This is a structure definition that directly packages prior lemmas: vacuum_zero from V_RS_at_vacuum, nonneg from V_RS_nonneg, cosh_form from V_RS_eq_cosh, quartic_remainder from V_RS_quartic_error, and the two conditional matches from mass_term_matches_SM together with the quartic_coefficient_canonical lemma. No new reasoning is introduced; the declaration simply names the assembled interface.
why it matters
The certificate supplies the explicit first arrow of the RS cost geometry to Higgs EFT map, feeding directly into higgsEFTBridgeCert and the composite HiggsEFTLowEnergyLimitCert. It closes the mapping from the J-cost functional (T5 J-uniqueness) to SM parameters under the explicit normalisation hypothesis, which remains open for derivation from the phi-ladder yardstick. The quartic remainder bound keeps the approximation controlled inside the electroweak regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.