IndisputableMonolith.StandardModel.HiggsYukawaBridge

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Masses.Anchor
   4import IndisputableMonolith.Masses.MassLaw
   5
   6/-!
   7# Higgs–Yukawa Bridge
   8
   9This module exposes the standard-model Yukawa coupling for a fermion as a
  10ratio of an RS-derived mass to the electroweak scale `v`, in the canonical
  11form
  12
  13    y_f = √2 · m_f / v.
  14
  15The mass `m_f` is supplied by `Masses.MassLaw.predict_mass`.  The result is
  16that *no Yukawa is fit independently*: every Yukawa is a function of the
  17fermion's rung on the φ-ladder and of the electroweak scale `v`, with the
  18SM extraction convention `y_f = √2 m_f / v` translated into the same
  19ladder structure.
  20
  21The φ-rung scaling property is preserved: increasing the fermion's rung by
  22one multiplies its Yukawa coupling by `φ`.  Generation jumps are therefore
  23`φ^(Δr)` where `Δr` is the integer rung difference, *not* `φ^1` between
  24adjacent SM generations.
  25
  26## Status
  27
  28* `THEOREM`: Yukawa positivity, φ-rung scaling, ratio of Yukawas equals
  29  ratio of masses.
  30* `CONDITIONAL`: identification of the SM Yukawa value `y_f^{SM}` with the
  31  RS Yukawa requires the same `v` as in the SM extraction (this is the
  32  same normalisation hypothesis as `HiggsEFTBridge.NormalizationHypothesis`,
  33  but expressed for fermions).
  34* `OPEN`: deriving the rung map for each SM species from cube combinatorics
  35  is a separate project, tracked under the `OPEN_RUNG_MAP` tag.
  36-/
  37
  38namespace IndisputableMonolith
  39namespace StandardModel
  40namespace HiggsYukawaBridge
  41
  42open Real
  43open Constants
  44open Masses
  45open Masses.MassLaw
  46
  47noncomputable section
  48
  49/-! ## §1. Yukawa Coupling -/
  50
  51/-- Standard-Model Yukawa extraction convention:
  52
  53    `y_f = √2 · m_f / v`
  54
  55    where `m_f = predict_mass sector rung Z` is the φ-ladder mass. -/
  56def yukawa_SM (sector : Anchor.Sector) (rung Z : ℤ) (v : ℝ) : ℝ :=
  57  Real.sqrt 2 * predict_mass sector rung Z / v
  58
  59/-- Yukawa couplings are positive for `v > 0`. -/
  60theorem yukawa_SM_pos
  61    (sector : Anchor.Sector) (rung Z : ℤ) (v : ℝ) (hv : 0 < v) :
  62    0 < yukawa_SM sector rung Z v := by
  63  unfold yukawa_SM
  64  have hsqrt2 : 0 < Real.sqrt 2 := Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 2)
  65  have hm : 0 < predict_mass sector rung Z := predict_mass_pos sector rung Z
  66  have hnum : 0 < Real.sqrt 2 * predict_mass sector rung Z := mul_pos hsqrt2 hm
  67  exact div_pos hnum hv
  68
  69/-- φ-rung scaling: increasing rung by 1 multiplies the Yukawa by `φ`. -/
  70theorem yukawa_SM_phi_scaling
  71    (sector : Anchor.Sector) (rung Z : ℤ) (v : ℝ) (hv : 0 < v) :
  72    yukawa_SM sector (rung + 1) Z v = phi * yukawa_SM sector rung Z v := by
  73  unfold yukawa_SM
  74  have hscale : predict_mass sector (rung + 1) Z = phi * predict_mass sector rung Z :=
  75    mass_rung_scaling sector rung Z
  76  have hv_ne : v ≠ 0 := ne_of_gt hv
  77  rw [hscale]
  78  field_simp
  79
  80/-- The Yukawa ratio between adjacent rungs is exactly `φ`. -/
  81theorem yukawa_SM_ratio_adjacent
  82    (sector : Anchor.Sector) (rung Z : ℤ) (v : ℝ) (hv : 0 < v) :
  83    yukawa_SM sector (rung + 1) Z v / yukawa_SM sector rung Z v = phi := by
  84  have h := yukawa_SM_phi_scaling sector rung Z v hv
  85  have hpos : 0 < yukawa_SM sector rung Z v := yukawa_SM_pos sector rung Z v hv
  86  have hne : yukawa_SM sector rung Z v ≠ 0 := ne_of_gt hpos
  87  rw [h]
  88  field_simp
  89
  90/-- The ratio of two Yukawas (same sector, same charge) equals the ratio
  91    of their masses; the `v`-dependence cancels. -/
  92theorem yukawa_SM_ratio_independent_of_v
  93    (sector : Anchor.Sector) (rung1 rung2 Z : ℤ) (v : ℝ) (hv : 0 < v) :
  94    yukawa_SM sector rung1 Z v / yukawa_SM sector rung2 Z v
  95      = predict_mass sector rung1 Z / predict_mass sector rung2 Z := by
  96  unfold yukawa_SM
  97  have hsqrt2_pos : 0 < Real.sqrt 2 := Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 2)
  98  have hsqrt2_ne : Real.sqrt 2 ≠ 0 := ne_of_gt hsqrt2_pos
  99  have hv_ne : v ≠ 0 := ne_of_gt hv
 100  have hm2_pos : 0 < predict_mass sector rung2 Z := predict_mass_pos sector rung2 Z
 101  have hm2_ne : predict_mass sector rung2 Z ≠ 0 := ne_of_gt hm2_pos
 102  field_simp
 103
 104/-! ## §2. Cross-Sector Generation Gap -/
 105
 106/-- The Yukawa scaling under an integer rung difference `Δr ≥ 0`:
 107
 108    y_f(rung + n) = φ^n · y_f(rung). -/
 109theorem yukawa_SM_phi_pow_scaling
 110    (sector : Anchor.Sector) (rung Z : ℤ) (n : ℕ) (v : ℝ) (hv : 0 < v) :
 111    yukawa_SM sector (rung + (n : ℤ)) Z v
 112      = phi ^ n * yukawa_SM sector rung Z v := by
 113  induction n with
 114  | zero =>
 115      simp [yukawa_SM]
 116  | succ k ih =>
 117      have h_one_step :
 118          yukawa_SM sector (rung + ((k : ℤ) + 1)) Z v
 119            = phi * yukawa_SM sector (rung + (k : ℤ)) Z v := by
 120        have := yukawa_SM_phi_scaling sector (rung + (k : ℤ)) Z v hv
 121        simpa [add_assoc] using this
 122      have hcast : (rung + (((k + 1 : ℕ) : ℤ))) = (rung + ((k : ℤ) + 1)) := by
 123        push_cast
 124        ring
 125      rw [hcast, h_one_step, ih]
 126      ring
 127
 128/-! ## §3. SM-Normalisation Hypothesis -/
 129
 130/-- The SM-normalisation hypothesis for fermion species: `v` is the same
 131    electroweak scale as the one used in the SM Yukawa extraction.
 132
 133    This is the fermion-sector counterpart of
 134    `HiggsEFTBridge.NormalizationHypothesis`.  It states that the Yukawa
 135    coupling extracted from `m_f` and `v` via `y_f = √2 m_f / v` is the
 136    same as the Yukawa appearing in the SM Lagrangian. -/
 137def YukawaNormalizationHypothesis
 138    (sector : Anchor.Sector) (rung Z : ℤ) (v y_SM : ℝ) : Prop :=
 139  yukawa_SM sector rung Z v = y_SM
 140
 141/-- Under the normalisation hypothesis, the SM-extracted Yukawa is positive. -/
 142theorem yukawa_SM_pos_of_hypothesis
 143    (sector : Anchor.Sector) (rung Z : ℤ) (v y_SM : ℝ) (hv : 0 < v)
 144    (hY : YukawaNormalizationHypothesis sector rung Z v y_SM) :
 145    0 < y_SM := by
 146  unfold YukawaNormalizationHypothesis at hY
 147  have h := yukawa_SM_pos sector rung Z v hv
 148  rw [← hY]; exact h
 149
 150/-! ## §4. Master Bridge Certificate -/
 151
 152/-- Master certificate for the Higgs–Yukawa bridge. -/
 153structure HiggsYukawaBridgeCert where
 154  /-- THEOREM: every Yukawa is positive for `v > 0`. -/
 155  yukawa_pos      : ∀ s r Z v, 0 < v → 0 < yukawa_SM s r Z v
 156  /-- THEOREM: adjacent-rung scaling by `φ`. -/
 157  yukawa_phi_step : ∀ s r Z v, 0 < v →
 158    yukawa_SM s (r + 1) Z v = phi * yukawa_SM s r Z v
 159  /-- THEOREM: integer-rung scaling by `φ^n`. -/
 160  yukawa_phi_pow  : ∀ s r Z (n : ℕ) v, 0 < v →
 161    yukawa_SM s (r + (n : ℤ)) Z v = phi ^ n * yukawa_SM s r Z v
 162  /-- THEOREM: ratio of Yukawas equals ratio of masses. -/
 163  yukawa_ratio_v_independent :
 164    ∀ s r1 r2 Z v, 0 < v →
 165      yukawa_SM s r1 Z v / yukawa_SM s r2 Z v
 166        = predict_mass s r1 Z / predict_mass s r2 Z
 167
 168def higgsYukawaBridgeCert : HiggsYukawaBridgeCert where
 169  yukawa_pos      := yukawa_SM_pos
 170  yukawa_phi_step := yukawa_SM_phi_scaling
 171  yukawa_phi_pow  := yukawa_SM_phi_pow_scaling
 172  yukawa_ratio_v_independent := yukawa_SM_ratio_independent_of_v
 173
 174theorem higgsYukawaBridgeCert_inhabited : Nonempty HiggsYukawaBridgeCert :=
 175  ⟨higgsYukawaBridgeCert⟩
 176
 177end
 178
 179end HiggsYukawaBridge
 180end StandardModel
 181end IndisputableMonolith
 182