IndisputableMonolith.StandardModel.HiggsEFTBridge

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Higgs EFT Bridge from Recognition Cost Geometry
   7
   8This module formalises the first link in the chain
   9
  10    RS cost geometry  →  effective scalar coordinate  →  canonical Higgs EFT
  11
  12The dimensionless RS coordinate is `ε = h / v` where `h` is the canonically
  13normalised collider scalar field of mass dimension one and `v > 0` is the
  14electroweak scale supplied by the recognition substrate.  A dimensionful
  15prefactor `Λ⁴` (with `Λ` of mass dimension one) is required to match the
  16Standard-Model Lagrangian normalisation.
  17
  18The recognition-cost potential is
  19
  20    V_RS Λ v h := Λ^4 · J(exp (h / v))
  21
  22where `J(x) = ½(x + x⁻¹) − 1` is the canonical reciprocal cost functional
  23and `J(eᵉ) = cosh ε − 1` (Lean: `Cost.Jcost_exp_cosh`).
  24
  25Expanded around the vacuum `h = 0`, this becomes
  26
  27    V_RS Λ v h = (Λ⁴ / 2 v²) · h² + (Λ⁴ / 24 v⁴) · h⁴ + 𝒪(h⁶)
  28
  29Matching onto the Standard-Model parametrisation
  30
  31    V_SM h = ½ m_H² h² + (λ_SM / 4) · h⁴ + ⋯
  32
  33gives the SM-to-RS dictionary
  34
  35    m_H² = Λ⁴ / v²,        λ_SM = (1/6) · Λ⁴ / v⁴.
  36
  37The map closes the first two arrows of Anil Thapa's reviewer chain.
  38The remaining collider-normalisation problem reduces to fixing `Λ(v)`
  39from the recognition substrate, which is left explicit as a hypothesis
  40below.
  41
  42## Status
  43
  44* `THEOREM`: the Taylor-coefficient extraction is forced by the cosh
  45  expansion proved here from `Cost.Jcost_exp_cosh` plus a Mathlib
  46  truncation bound.
  47* `CONDITIONAL_THEOREM`: the SM-quartic identification depends on the
  48  normalisation hypothesis `Λ⁴ = m_H² · v²`, which is the open subproblem.
  49* `OPEN_NORMALIZATION`: deriving `Λ` from the φ-ladder yardstick.
  50-/
  51
  52namespace IndisputableMonolith
  53namespace StandardModel
  54namespace HiggsEFTBridge
  55
  56open Real
  57open Constants
  58open IndisputableMonolith.Cost
  59
  60noncomputable section
  61
  62/-! ## §1. The Recognition-Cost Potential -/
  63
  64/-- The RS Higgs effective potential at canonical mass dimension four.
  65
  66    `V_RS Λ v h = Λ⁴ · J(exp (h / v))`. -/
  67def V_RS (Λ v h : ℝ) : ℝ := Λ ^ 4 * Jcost (Real.exp (h / v))
  68
  69/-- `V_RS` reduces to `Λ⁴ · (cosh(h/v) − 1)`. -/
  70theorem V_RS_eq_cosh (Λ v h : ℝ) :
  71    V_RS Λ v h = Λ ^ 4 * (Real.cosh (h / v) - 1) := by
  72  unfold V_RS
  73  rw [Cost.Jcost_exp_cosh]
  74
  75/-- The vacuum is at `h = 0` with zero potential. -/
  76theorem V_RS_at_vacuum (Λ v : ℝ) : V_RS Λ v 0 = 0 := by
  77  rw [V_RS_eq_cosh]
  78  simp [Real.cosh_zero]
  79
  80/-- The RS potential is non-negative. -/
  81theorem V_RS_nonneg (Λ v : ℝ) (h : ℝ) : 0 ≤ V_RS Λ v h := by
  82  rw [V_RS_eq_cosh]
  83  have hΛ4 : 0 ≤ Λ ^ 4 := by positivity
  84  have hcosh : 1 ≤ Real.cosh (h / v) := Real.one_le_cosh _
  85  have : 0 ≤ Real.cosh (h / v) - 1 := by linarith
  86  exact mul_nonneg hΛ4 this
  87
  88/-! ## §2. Quartic-Order Taylor Expansion -/
  89
  90/-- The quartic Taylor approximation to the RS potential about the vacuum. -/
  91def V_RS_quartic (Λ v h : ℝ) : ℝ :=
  92  Λ ^ 4 * ((h / v) ^ 2 / 2 + (h / v) ^ 4 / 24)
  93
  94/-- Mathlib truncation lemma, restated for real `t` to depth 6.
  95
  96    `|exp t − (1 + t + t²/2 + t³/6 + t⁴/24 + t⁵/120)| ≤ exp |t| · |t|⁶`.
  97
  98    Proof: lift to ℂ and apply `Complex.norm_exp_sub_sum_le_norm_mul_exp`. -/
  99private theorem exp_sub_trunc6_le (t : ℝ) :
 100    |Real.exp t - (1 + t + t ^ 2 / 2 + t ^ 3 / 6 + t ^ 4 / 24 + t ^ 5 / 120)| ≤
 101      Real.exp |t| * |t| ^ 6 := by
 102  have h := Complex.norm_exp_sub_sum_le_norm_mul_exp (t : ℂ) 6
 103  have hexpr :
 104      Complex.exp (t : ℂ) - ∑ m ∈ Finset.range 6, (t : ℂ) ^ m / m.factorial =
 105        ((Real.exp t - (1 + t + t ^ 2 / 2 + t ^ 3 / 6 + t ^ 4 / 24 + t ^ 5 / 120) : ℝ) : ℂ) := by
 106    simp [Complex.ofReal_exp, Finset.sum_range_succ, Nat.factorial]
 107  rw [hexpr, Complex.norm_real, Real.norm_eq_abs] at h
 108  simpa [mul_comm, mul_left_comm, mul_assoc] using h
 109
 110/-- Quartic-error bound for `cosh ε - 1` on `|ε| ≤ 1/2`:
 111
 112    `|cosh ε - 1 - ε²/2 - ε⁴/24| ≤ exp |ε| · |ε|⁶`.
 113
 114    Proof: average the truncation bound for `exp t` and `exp (-t)`. -/
 115private theorem cosh_quartic_error (ε : ℝ) :
 116    |Real.cosh ε - 1 - ε ^ 2 / 2 - ε ^ 4 / 24| ≤ Real.exp |ε| * |ε| ^ 6 := by
 117  set P : ℝ → ℝ := fun t =>
 118    1 + t + t ^ 2 / 2 + t ^ 3 / 6 + t ^ 4 / 24 + t ^ 5 / 120
 119  have hpos : |Real.exp ε - P ε| ≤ Real.exp |ε| * |ε| ^ 6 := by
 120    simpa [P] using exp_sub_trunc6_le ε
 121  have hneg : |Real.exp (-ε) - P (-ε)| ≤ Real.exp |ε| * |ε| ^ 6 := by
 122    simpa [P, abs_neg] using exp_sub_trunc6_le (-ε)
 123  have hpoly : P ε + P (-ε) = 2 * (1 + ε ^ 2 / 2 + ε ^ 4 / 24) := by
 124    simp only [P]; ring
 125  have hrewrite :
 126      Real.cosh ε - 1 - ε ^ 2 / 2 - ε ^ 4 / 24 =
 127        ((Real.exp ε - P ε) + (Real.exp (-ε) - P (-ε))) / 2 := by
 128    rw [Real.cosh_eq]
 129    linarith [hpoly]
 130  rw [hrewrite, abs_div, abs_of_pos (by norm_num : (0 : ℝ) < 2)]
 131  calc
 132    |(Real.exp ε - P ε) + (Real.exp (-ε) - P (-ε))| / 2
 133        ≤ (|Real.exp ε - P ε| + |Real.exp (-ε) - P (-ε)|) / 2 :=
 134          div_le_div_of_nonneg_right (abs_add_le _ _) (by norm_num)
 135    _ ≤ (Real.exp |ε| * |ε| ^ 6 + Real.exp |ε| * |ε| ^ 6) / 2 :=
 136          div_le_div_of_nonneg_right (add_le_add hpos hneg) (by norm_num)
 137    _ = Real.exp |ε| * |ε| ^ 6 := by ring
 138
 139/-- Quartic Taylor identity for `J(exp ε)` at depth 4:
 140
 141    `|J(exp ε) - ε²/2 - ε⁴/24| ≤ exp |ε| · |ε|⁶`. -/
 142theorem jcost_quartic_error (ε : ℝ) :
 143    |Jcost (Real.exp ε) - ε ^ 2 / 2 - ε ^ 4 / 24| ≤ Real.exp |ε| * |ε| ^ 6 := by
 144  have h := cosh_quartic_error ε
 145  have hcosh : Jcost (Real.exp ε) = Real.cosh ε - 1 := Cost.Jcost_exp_cosh ε
 146  -- |Jcost(exp ε) - ε²/2 - ε⁴/24| = |cosh ε - 1 - ε²/2 - ε⁴/24|
 147  have hrewrite :
 148      Jcost (Real.exp ε) - ε ^ 2 / 2 - ε ^ 4 / 24
 149        = Real.cosh ε - 1 - ε ^ 2 / 2 - ε ^ 4 / 24 := by
 150    rw [hcosh]
 151  rw [hrewrite]
 152  exact h
 153
 154/-- The error in approximating `V_RS` by its quartic Taylor polynomial is
 155    bounded uniformly on `|h| ≤ v / 2`. -/
 156theorem V_RS_quartic_error (Λ v h : ℝ) (hv : 0 < v) (hbound : |h| ≤ v / 2) :
 157    |V_RS Λ v h - V_RS_quartic Λ v h|
 158      ≤ |Λ| ^ 4 * (Real.exp |h / v| * |h / v| ^ 6) := by
 159  have hε : |h / v| ≤ 1 / 2 := by
 160    rw [abs_div, abs_of_pos hv]
 161    rw [div_le_iff₀ hv]
 162    linarith
 163  have hcore := jcost_quartic_error (h / v)
 164  -- |V_RS − V_RS_quartic| = |Λ|^4 · |J(exp ε) − ε²/2 − ε⁴/24|
 165  unfold V_RS V_RS_quartic
 166  set ε := h / v
 167  have hL : Λ ^ 4 * Jcost (Real.exp ε) - Λ ^ 4 * (ε ^ 2 / 2 + ε ^ 4 / 24)
 168            = Λ ^ 4 * (Jcost (Real.exp ε) - ε ^ 2 / 2 - ε ^ 4 / 24) := by ring
 169  rw [hL, abs_mul]
 170  have hΛ : |Λ ^ 4| = |Λ| ^ 4 := by rw [abs_pow]
 171  rw [hΛ]
 172  have hΛ4 : 0 ≤ |Λ| ^ 4 := by positivity
 173  exact mul_le_mul_of_nonneg_left hcore hΛ4
 174
 175/-- The leading quadratic coefficient is forced: `Λ⁴ / (2 v²)`. -/
 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
 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
 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)
 251  /-- CONDITIONAL_THEOREM: under the normalisation hypothesis, the leading
 252      quadratic coefficient gives the SM Higgs mass term. -/
 253  mass_term_match    : ∀ Λ v m_H, 0 < v → NormalizationHypothesis Λ v m_H →
 254    quadratic_coefficient Λ v = m_H ^ 2 / 2
 255  /-- CONDITIONAL_THEOREM: under the normalisation hypothesis, the canonical
 256      SM quartic coupling is `λ_SM = (1/6) · m_H² / v²`. -/
 257  quartic_match      : ∀ Λ v m_H, 0 < v → NormalizationHypothesis Λ v m_H →
 258    4 * quartic_coefficient_canonical Λ v = m_H ^ 2 / (6 * v ^ 2)
 259
 260/-- The bridge certificate is theorem-backed (modulo the explicit
 261    normalisation hypotheses recorded in its conditional clauses). -/
 262def higgsEFTBridgeCert : HiggsEFTBridgeCert where
 263  vacuum_zero       := V_RS_at_vacuum
 264  nonneg            := V_RS_nonneg
 265  cosh_form         := V_RS_eq_cosh
 266  quartic_remainder := fun Λ v h hv hb => V_RS_quartic_error Λ v h hv hb
 267  mass_term_match   := fun Λ v m_H hv hΛ => mass_term_matches_SM Λ v m_H hv hΛ
 268  quartic_match     := fun Λ v m_H hv hΛ =>
 269    quartic_coupling_from_normalization Λ v m_H hv hΛ
 270
 271theorem higgsEFTBridgeCert_inhabited : Nonempty HiggsEFTBridgeCert :=
 272  ⟨higgsEFTBridgeCert⟩
 273
 274end
 275
 276end HiggsEFTBridge
 277end StandardModel
 278end IndisputableMonolith
 279