NormalizationHypothesis

formal source

 198    scale `Λ` and the SM electroweak scale `v`.  Closing this hypothesis
 199    from the φ-ladder yardstick is the open collider-normalisation problem
 200    flagged in the companion paper. -/
 201def NormalizationHypothesis (Λ v m_H : ℝ) : Prop :=
 202  Λ ^ 4 = m_H ^ 2 * v ^ 2
 203
 204/-- Under the normalisation hypothesis, the SM kinetic-normalised Higgs mass
 205    appears as the coefficient of `½ h²` in the RS quartic Taylor potential. -/
 206theorem mass_term_matches_SM
 207    (Λ v m_H : ℝ) (hv : 0 < v) (hΛ : NormalizationHypothesis Λ v m_H) :
 208    quadratic_coefficient Λ v = m_H ^ 2 / 2 := by
 209  unfold quadratic_coefficient
 210  unfold NormalizationHypothesis at hΛ
 211  have hv2 : v ^ 2 ≠ 0 := pow_ne_zero 2 (ne_of_gt hv)
 212  rw [hΛ]
 213  field_simp
 214
 215/-- Under the normalisation hypothesis, the canonical SM quartic coupling is
 216    `λ_SM = (1/6) · m_H² / v²`.
 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