quartic_coefficient_canonical

formal source

 176def quadratic_coefficient (Λ v : ℝ) : ℝ := Λ ^ 4 / (2 * v ^ 2)
 177
 178/-- The leading quartic coefficient is forced: `Λ⁴ / (24 v⁴)`. -/
 179def quartic_coefficient_canonical (Λ v : ℝ) : ℝ := Λ ^ 4 / (24 * v ^ 4)
 180
 181/-- Algebraic identity: the quartic Taylor potential equals the canonical
 182    quadratic-plus-quartic Lagrangian potential up to renaming. -/
 183theorem V_RS_quartic_canonical (Λ v : ℝ) (hv : v ≠ 0) (h : ℝ) :
 184    V_RS_quartic Λ v h
 185      = quadratic_coefficient Λ v * h ^ 2
 186        + quartic_coefficient_canonical Λ v * h ^ 4 := by
 187  unfold V_RS_quartic quadratic_coefficient quartic_coefficient_canonical
 188  have hv2 : v ^ 2 ≠ 0 := pow_ne_zero 2 hv
 189  have hv4 : v ^ 4 ≠ 0 := pow_ne_zero 4 hv
 190  field_simp
 191
 192/-! ## §3. Standard-Model Dictionary -/
 193
 194/-- The Standard-Model normalisation hypothesis: the canonically normalised
 195    Higgs mass squared equals `Λ⁴ / v²`.
 196
 197    This is the *defining* normalisation map between the recognition-cost
 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