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## ATTACKER BREADCRUMB (read before claiming this matches the SM at tree level)
  52
  53The "λ_SM = m_H²/(6v²)" coefficient extracted in §3 is **NOT the standard
  54SM Higgs quartic** (which is m_H²/(2v²) ≈ 0.129 at v = 246 GeV, not
  55m_H²/(6v²) ≈ 0.043). It is the value that would match the cosh's quartic
  56Taylor coefficient.
  57
  58The cosh form `V_RS = Λ⁴(cosh(h/v)−1)` is **even in h**, so:
  59  * the trilinear `h³` coefficient is identically zero (`κ_λ_3 = 0`).
  60  * the quartic `h⁴` coefficient is `m_H²/(24v²) = (1/3)·(m_H²/(8v²))`,
  61    one-third of the SM Mexican-hat value (`κ_λ_4 = 1/3`).
  62  * the sextic `h⁶` coefficient is `m_H²/(720v⁴)`, nonzero (BSM).
  63
  64These are pre-registered BSM signatures, falsifiable at HL-LHC di-Higgs
  65(probes h³) and FCC-hh tri-Higgs (probes h⁴). See
  66`StandardModel.HiggsCoshBSMPredictions` for the explicit Lean theorems
  67and the master falsifier `HiggsCoshBSMFalsifier`.
  68
  69The exact magnitude of the BSM deviation depends on the substrate
  70kinetic-term shape: under the canonical (linear) identification
  71`h = v · ε` used in this module, the predictions are as above. Other
  72kinetic-term shapes give different `κ_λ_3`, `κ_λ_4` values; deriving
  73the canonical kinetic term from RS primitives is the OPEN frontier.
  74-/
  75
  76namespace IndisputableMonolith
  77namespace StandardModel
  78namespace HiggsEFTBridge
  79
  80open Real
  81open Constants
  82open IndisputableMonolith.Cost
  83
  84noncomputable section
  85
  86/-! ## §1. The Recognition-Cost Potential -/
  87
  88/-- The RS Higgs effective potential at canonical mass dimension four.
  89
  90    `V_RS Λ v h = Λ⁴ · J(exp (h / v))`. -/
  91def V_RS (Λ v h : ℝ) : ℝ := Λ ^ 4 * Jcost (Real.exp (h / v))
  92
  93/-- `V_RS` reduces to `Λ⁴ · (cosh(h/v) − 1)`. -/
  94theorem V_RS_eq_cosh (Λ v h : ℝ) :
  95    V_RS Λ v h = Λ ^ 4 * (Real.cosh (h / v) - 1) := by
  96  unfold V_RS
  97  rw [Cost.Jcost_exp_cosh]
  98
  99/-- The vacuum is at `h = 0` with zero potential. -/
 100theorem V_RS_at_vacuum (Λ v : ℝ) : V_RS Λ v 0 = 0 := by
 101  rw [V_RS_eq_cosh]
 102  simp [Real.cosh_zero]
 103
 104/-- The RS potential is non-negative. -/
 105theorem V_RS_nonneg (Λ v : ℝ) (h : ℝ) : 0 ≤ V_RS Λ v h := by
 106  rw [V_RS_eq_cosh]
 107  have hΛ4 : 0 ≤ Λ ^ 4 := by positivity
 108  have hcosh : 1 ≤ Real.cosh (h / v) := Real.one_le_cosh _
 109  have : 0 ≤ Real.cosh (h / v) - 1 := by linarith
 110  exact mul_nonneg hΛ4 this
 111
 112/-! ## §2. Quartic-Order Taylor Expansion -/
 113
 114/-- The quartic Taylor approximation to the RS potential about the vacuum. -/
 115def V_RS_quartic (Λ v h : ℝ) : ℝ :=
 116  Λ ^ 4 * ((h / v) ^ 2 / 2 + (h / v) ^ 4 / 24)
 117
 118/-- Mathlib truncation lemma, restated for real `t` to depth 6.
 119
 120    `|exp t − (1 + t + t²/2 + t³/6 + t⁴/24 + t⁵/120)| ≤ exp |t| · |t|⁶`.
 121
 122    Proof: lift to ℂ and apply `Complex.norm_exp_sub_sum_le_norm_mul_exp`. -/
 123private theorem exp_sub_trunc6_le (t : ℝ) :
 124    |Real.exp t - (1 + t + t ^ 2 / 2 + t ^ 3 / 6 + t ^ 4 / 24 + t ^ 5 / 120)| ≤
 125      Real.exp |t| * |t| ^ 6 := by
 126  have h := Complex.norm_exp_sub_sum_le_norm_mul_exp (t : ℂ) 6
 127  have hexpr :
 128      Complex.exp (t : ℂ) - ∑ m ∈ Finset.range 6, (t : ℂ) ^ m / m.factorial =
 129        ((Real.exp t - (1 + t + t ^ 2 / 2 + t ^ 3 / 6 + t ^ 4 / 24 + t ^ 5 / 120) : ℝ) : ℂ) := by
 130    simp [Complex.ofReal_exp, Finset.sum_range_succ, Nat.factorial]
 131  rw [hexpr, Complex.norm_real, Real.norm_eq_abs] at h
 132  simpa [mul_comm, mul_left_comm, mul_assoc] using h
 133
 134/-- Quartic-error bound for `cosh ε - 1` on `|ε| ≤ 1/2`:
 135
 136    `|cosh ε - 1 - ε²/2 - ε⁴/24| ≤ exp |ε| · |ε|⁶`.
 137
 138    Proof: average the truncation bound for `exp t` and `exp (-t)`. -/
 139private theorem cosh_quartic_error (ε : ℝ) :
 140    |Real.cosh ε - 1 - ε ^ 2 / 2 - ε ^ 4 / 24| ≤ Real.exp |ε| * |ε| ^ 6 := by
 141  set P : ℝ → ℝ := fun t =>
 142    1 + t + t ^ 2 / 2 + t ^ 3 / 6 + t ^ 4 / 24 + t ^ 5 / 120
 143  have hpos : |Real.exp ε - P ε| ≤ Real.exp |ε| * |ε| ^ 6 := by
 144    simpa [P] using exp_sub_trunc6_le ε
 145  have hneg : |Real.exp (-ε) - P (-ε)| ≤ Real.exp |ε| * |ε| ^ 6 := by
 146    simpa [P, abs_neg] using exp_sub_trunc6_le (-ε)
 147  have hpoly : P ε + P (-ε) = 2 * (1 + ε ^ 2 / 2 + ε ^ 4 / 24) := by
 148    simp only [P]; ring
 149  have hrewrite :
 150      Real.cosh ε - 1 - ε ^ 2 / 2 - ε ^ 4 / 24 =
 151        ((Real.exp ε - P ε) + (Real.exp (-ε) - P (-ε))) / 2 := by
 152    rw [Real.cosh_eq]
 153    linarith [hpoly]
 154  rw [hrewrite, abs_div, abs_of_pos (by norm_num : (0 : ℝ) < 2)]
 155  calc
 156    |(Real.exp ε - P ε) + (Real.exp (-ε) - P (-ε))| / 2
 157        ≤ (|Real.exp ε - P ε| + |Real.exp (-ε) - P (-ε)|) / 2 :=
 158          div_le_div_of_nonneg_right (abs_add_le _ _) (by norm_num)
 159    _ ≤ (Real.exp |ε| * |ε| ^ 6 + Real.exp |ε| * |ε| ^ 6) / 2 :=
 160          div_le_div_of_nonneg_right (add_le_add hpos hneg) (by norm_num)
 161    _ = Real.exp |ε| * |ε| ^ 6 := by ring
 162
 163/-- Quartic Taylor identity for `J(exp ε)` at depth 4:
 164
 165    `|J(exp ε) - ε²/2 - ε⁴/24| ≤ exp |ε| · |ε|⁶`. -/
 166theorem jcost_quartic_error (ε : ℝ) :
 167    |Jcost (Real.exp ε) - ε ^ 2 / 2 - ε ^ 4 / 24| ≤ Real.exp |ε| * |ε| ^ 6 := by
 168  have h := cosh_quartic_error ε
 169  have hcosh : Jcost (Real.exp ε) = Real.cosh ε - 1 := Cost.Jcost_exp_cosh ε
 170  -- |Jcost(exp ε) - ε²/2 - ε⁴/24| = |cosh ε - 1 - ε²/2 - ε⁴/24|
 171  have hrewrite :
 172      Jcost (Real.exp ε) - ε ^ 2 / 2 - ε ^ 4 / 24
 173        = Real.cosh ε - 1 - ε ^ 2 / 2 - ε ^ 4 / 24 := by
 174    rw [hcosh]
 175  rw [hrewrite]
 176  exact h
 177
 178/-- The error in approximating `V_RS` by its quartic Taylor polynomial is
 179    bounded uniformly on `|h| ≤ v / 2`. -/
 180theorem V_RS_quartic_error (Λ v h : ℝ) (hv : 0 < v) (hbound : |h| ≤ v / 2) :
 181    |V_RS Λ v h - V_RS_quartic Λ v h|
 182      ≤ |Λ| ^ 4 * (Real.exp |h / v| * |h / v| ^ 6) := by
 183  have hε : |h / v| ≤ 1 / 2 := by
 184    rw [abs_div, abs_of_pos hv]
 185    rw [div_le_iff₀ hv]
 186    linarith
 187  have hcore := jcost_quartic_error (h / v)
 188  -- |V_RS − V_RS_quartic| = |Λ|^4 · |J(exp ε) − ε²/2 − ε⁴/24|
 189  unfold V_RS V_RS_quartic
 190  set ε := h / v
 191  have hL : Λ ^ 4 * Jcost (Real.exp ε) - Λ ^ 4 * (ε ^ 2 / 2 + ε ^ 4 / 24)
 192            = Λ ^ 4 * (Jcost (Real.exp ε) - ε ^ 2 / 2 - ε ^ 4 / 24) := by ring
 193  rw [hL, abs_mul]
 194  have hΛ : |Λ ^ 4| = |Λ| ^ 4 := by rw [abs_pow]
 195  rw [hΛ]
 196  have hΛ4 : 0 ≤ |Λ| ^ 4 := by positivity
 197  exact mul_le_mul_of_nonneg_left hcore hΛ4
 198
 199/-- The leading quadratic coefficient is forced: `Λ⁴ / (2 v²)`. -/
 200def quadratic_coefficient (Λ v : ℝ) : ℝ := Λ ^ 4 / (2 * v ^ 2)
 201
 202/-- The leading quartic coefficient is forced: `Λ⁴ / (24 v⁴)`. -/
 203def quartic_coefficient_canonical (Λ v : ℝ) : ℝ := Λ ^ 4 / (24 * v ^ 4)
 204
 205/-- Algebraic identity: the quartic Taylor potential equals the canonical
 206    quadratic-plus-quartic Lagrangian potential up to renaming. -/
 207theorem V_RS_quartic_canonical (Λ v : ℝ) (hv : v ≠ 0) (h : ℝ) :
 208    V_RS_quartic Λ v h
 209      = quadratic_coefficient Λ v * h ^ 2
 210        + quartic_coefficient_canonical Λ v * h ^ 4 := by
 211  unfold V_RS_quartic quadratic_coefficient quartic_coefficient_canonical
 212  have hv2 : v ^ 2 ≠ 0 := pow_ne_zero 2 hv
 213  have hv4 : v ^ 4 ≠ 0 := pow_ne_zero 4 hv
 214  field_simp
 215
 216/-! ## §3. Standard-Model Dictionary -/
 217
 218/-- The Standard-Model normalisation hypothesis: the canonically normalised
 219    Higgs mass squared equals `Λ⁴ / v²`.
 220
 221    This is the *defining* normalisation map between the recognition-cost
 222    scale `Λ` and the SM electroweak scale `v`.  Closing this hypothesis
 223    from the φ-ladder yardstick is the open collider-normalisation problem
 224    flagged in the companion paper. -/
 225def NormalizationHypothesis (Λ v m_H : ℝ) : Prop :=
 226  Λ ^ 4 = m_H ^ 2 * v ^ 2
 227
 228/-- Under the normalisation hypothesis, the SM kinetic-normalised Higgs mass
 229    appears as the coefficient of `½ h²` in the RS quartic Taylor potential. -/
 230theorem mass_term_matches_SM
 231    (Λ v m_H : ℝ) (hv : 0 < v) (hΛ : NormalizationHypothesis Λ v m_H) :
 232    quadratic_coefficient Λ v = m_H ^ 2 / 2 := by
 233  unfold quadratic_coefficient
 234  unfold NormalizationHypothesis at hΛ
 235  have hv2 : v ^ 2 ≠ 0 := pow_ne_zero 2 (ne_of_gt hv)
 236  rw [hΛ]
 237  field_simp
 238
 239/-- Under the normalisation hypothesis, the canonical SM quartic coupling is
 240    `λ_SM = (1/6) · m_H² / v²`.
 241
 242    In the convention `V_SM = ½ m_H² h² + (λ_SM / 4) h⁴`, matching the RS
 243    quartic coefficient `Λ⁴ / (24 v⁴)` to `λ_SM / 4` gives this relation. -/
 244theorem quartic_coupling_from_normalization
 245    (Λ v m_H : ℝ) (hv : 0 < v) (hΛ : NormalizationHypothesis Λ v m_H) :
 246    4 * quartic_coefficient_canonical Λ v = m_H ^ 2 / (6 * v ^ 2) := by
 247  unfold quartic_coefficient_canonical
 248  unfold NormalizationHypothesis at hΛ
 249  have hv2 : v ^ 2 ≠ 0 := pow_ne_zero 2 (ne_of_gt hv)
 250  have hv4 : v ^ 4 ≠ 0 := pow_ne_zero 4 (ne_of_gt hv)
 251  have hv4_eq : (v : ℝ) ^ 4 = v ^ 2 * v ^ 2 := by ring
 252  rw [hΛ, hv4_eq]
 253  field_simp
 254  ring
 255
 256/-! ## §4. Master Bridge Certificate -/
 257
 258/-- Master certificate for the cost-geometry → scalar-EFT map.
 259
 260    Tags: each clause is `THEOREM` except where marked `CONDITIONAL_THEOREM`;
 261    those clauses depend on `NormalizationHypothesis Λ v m_H`. -/
 262structure HiggsEFTBridgeCert where
 263  /-- THEOREM: the RS potential vanishes at the vacuum. -/
 264  vacuum_zero        : ∀ Λ v, V_RS Λ v 0 = 0
 265  /-- THEOREM: the RS potential is non-negative everywhere. -/
 266  nonneg             : ∀ Λ v h, 0 ≤ V_RS Λ v h
 267  /-- THEOREM: the RS potential equals `Λ⁴(cosh − 1)`. -/
 268  cosh_form          : ∀ Λ v h, V_RS Λ v h = Λ ^ 4 * (Real.cosh (h / v) - 1)
 269  /-- THEOREM: the RS potential matches its quartic Taylor approximation up
 270      to a sextic-order remainder bounded uniformly on `|h| ≤ v / 2`. -/
 271  quartic_remainder  :
 272    ∀ Λ v h, 0 < v → |h| ≤ v / 2 →
 273      |V_RS Λ v h - V_RS_quartic Λ v h|
 274        ≤ |Λ| ^ 4 * (Real.exp |h / v| * |h / v| ^ 6)
 275  /-- CONDITIONAL_THEOREM: under the normalisation hypothesis, the leading
 276      quadratic coefficient gives the SM Higgs mass term. -/
 277  mass_term_match    : ∀ Λ v m_H, 0 < v → NormalizationHypothesis Λ v m_H →
 278    quadratic_coefficient Λ v = m_H ^ 2 / 2
 279  /-- CONDITIONAL_THEOREM: under the normalisation hypothesis, the canonical
 280      SM quartic coupling is `λ_SM = (1/6) · m_H² / v²`. -/
 281  quartic_match      : ∀ Λ v m_H, 0 < v → NormalizationHypothesis Λ v m_H →
 282    4 * quartic_coefficient_canonical Λ v = m_H ^ 2 / (6 * v ^ 2)
 283
 284/-- The bridge certificate is theorem-backed (modulo the explicit
 285    normalisation hypotheses recorded in its conditional clauses). -/
 286def higgsEFTBridgeCert : HiggsEFTBridgeCert where
 287  vacuum_zero       := V_RS_at_vacuum
 288  nonneg            := V_RS_nonneg
 289  cosh_form         := V_RS_eq_cosh
 290  quartic_remainder := fun Λ v h hv hb => V_RS_quartic_error Λ v h hv hb
 291  mass_term_match   := fun Λ v m_H hv hΛ => mass_term_matches_SM Λ v m_H hv hΛ
 292  quartic_match     := fun Λ v m_H hv hΛ =>
 293    quartic_coupling_from_normalization Λ v m_H hv hΛ
 294
 295theorem higgsEFTBridgeCert_inhabited : Nonempty HiggsEFTBridgeCert :=
 296  ⟨higgsEFTBridgeCert⟩
 297
 298end
 299
 300end HiggsEFTBridge
 301end StandardModel
 302end IndisputableMonolith
 303