quartic_coupling_from_normalization

formal source

 217
 218    In the convention `V_SM = ½ m_H² h² + (λ_SM / 4) h⁴`, matching the RS
 219    quartic coefficient `Λ⁴ / (24 v⁴)` to `λ_SM / 4` gives this relation. -/
 220theorem quartic_coupling_from_normalization
 221    (Λ v m_H : ℝ) (hv : 0 < v) (hΛ : NormalizationHypothesis Λ v m_H) :
 222    4 * quartic_coefficient_canonical Λ v = m_H ^ 2 / (6 * v ^ 2) := by
 223  unfold quartic_coefficient_canonical
 224  unfold NormalizationHypothesis at hΛ
 225  have hv2 : v ^ 2 ≠ 0 := pow_ne_zero 2 (ne_of_gt hv)
 226  have hv4 : v ^ 4 ≠ 0 := pow_ne_zero 4 (ne_of_gt hv)
 227  have hv4_eq : (v : ℝ) ^ 4 = v ^ 2 * v ^ 2 := by ring
 228  rw [hΛ, hv4_eq]
 229  field_simp
 230  ring
 231
 232/-! ## §4. Master Bridge Certificate -/
 233
 234/-- Master certificate for the cost-geometry → scalar-EFT map.
 235
 236    Tags: each clause is `THEOREM` except where marked `CONDITIONAL_THEOREM`;
 237    those clauses depend on `NormalizationHypothesis Λ v m_H`. -/
 238structure HiggsEFTBridgeCert where
 239  /-- THEOREM: the RS potential vanishes at the vacuum. -/
 240  vacuum_zero        : ∀ Λ v, V_RS Λ v 0 = 0
 241  /-- THEOREM: the RS potential is non-negative everywhere. -/
 242  nonneg             : ∀ Λ v h, 0 ≤ V_RS Λ v h
 243  /-- THEOREM: the RS potential equals `Λ⁴(cosh − 1)`. -/
 244  cosh_form          : ∀ Λ v h, V_RS Λ v h = Λ ^ 4 * (Real.cosh (h / v) - 1)
 245  /-- THEOREM: the RS potential matches its quartic Taylor approximation up
 246      to a sextic-order remainder bounded uniformly on `|h| ≤ v / 2`. -/
 247  quartic_remainder  :
 248    ∀ Λ v h, 0 < v → |h| ≤ v / 2 →
 249      |V_RS Λ v h - V_RS_quartic Λ v h|
 250        ≤ |Λ| ^ 4 * (Real.exp |h / v| * |h / v| ^ 6)