IndisputableMonolith.Physics.RGTransport

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.RSBridge.Anchor
   4
   5/-!
   6# Renormalization Group Transport for Mass Residues
   7
   8This module formalizes the **RG transport** that defines the empirical mass residue `f^exp`.
   9
  10## Background
  11
  12In the Standard Model, fermion masses run with the renormalization scale μ according to:
  13
  14  `d(ln m)/d(ln μ) = -γ_m(μ)`
  15
  16where `γ_m(μ)` is the mass anomalous dimension, depending on couplings `α_s(μ), α(μ), ...`.
  17
  18The **integrated residue** from scale `μ₀` to `μ₁` is:
  19
  20  `f(μ₀, μ₁) = (1/λ) ∫_{ln μ₀}^{ln μ₁} γ_m(μ') d(ln μ')`
  21
  22where `λ = ln φ` is the normalization constant used in the mass formula.
  23
  24## Relation to Mass Formula
  25
  26The structural mass `m_struct` is defined at the anchor `μ⋆`. The physical mass relates via:
  27
  28  `m(μ⋆) = m_phys · φ^{f(μ⋆, m_phys)}`
  29
  30If `m(μ⋆) = m_struct`, then:
  31
  32  `m_phys = m_struct · φ^{-f}`
  33
  34## What This Module Provides
  35
  361. **AnomalousDimension**: A structure representing the mass anomalous dimension γ_m(μ).
  372. **RGTransport**: The integral formula that defines the residue.
  383. **Connection theorems**: Relating the transport to the mass ratio.
  39
  40## What This Module Does NOT Provide
  41
  42The actual QCD 4L / QED 2L kernels. Those would require extensive Standard Model machinery.
  43This module provides the *mathematical framework* that such kernels would plug into.
  44
  45## See Also
  46
  47- `IndisputableMonolith/Physics/AnchorPolicy.lean`: The axiom `f_residue` is intended to be
  48  the result of this transport at the anchor scale.
  49- `IndisputableMonolith/Physics/AnchorPolicyCertified.lean`: If you want to avoid global axioms
  50  and instead depend on externally certified residue intervals.
  51- `IndisputableMonolith/Physics/RunningCouplings.lean`: Threshold scales and crossover structure.
  52- `IndisputableMonolith/Physics/ElectronMass/Necessity.lean`: Proven bounds on electron mass
  53  and residues using interval arithmetic.
  54-/
  55
  56namespace IndisputableMonolith
  57namespace Physics
  58namespace RGTransport
  59
  60open IndisputableMonolith.Constants
  61open IndisputableMonolith.RSBridge
  62open MeasureTheory
  63
  64noncomputable section
  65
  66/-! ## Anomalous Dimension Structure -/
  67
  68/-- Running coupling at scale μ. This is an abstract interface; the actual SM couplings
  69    (α_s, α, α_2) would be specializations. -/
  70structure RunningCoupling where
  71  /-- The coupling value at scale μ (in GeV). -/
  72  at_scale : ℝ → ℝ
  73  /-- The coupling is positive in the perturbative regime. -/
  74  positive_in_pert : ∀ μ, μ > 1 → at_scale μ > 0
  75  /-- Asymptotic freedom: coupling decreases at high scale (for QCD). -/
  76  asymp_free : ∀ μ₁ μ₂, μ₁ < μ₂ → μ₂ > 100 → at_scale μ₂ < at_scale μ₁
  77
  78/-- The mass anomalous dimension γ_m(μ).
  79    In general, this is a function of the scale and the fermion species.
  80    It encodes how the running mass changes with μ. -/
  81structure AnomalousDimension where
  82  /-- The anomalous dimension value for fermion f at scale μ. -/
  83  gamma : Fermion → ℝ → ℝ
  84  /-- The anomalous dimension is smooth (differentiable). -/
  85  smooth : ∀ f, Differentiable ℝ (gamma f)
  86  /-- Perturbative bound: |γ| is bounded in the perturbative regime. -/
  87  pert_bounded : ∃ B > 0, ∀ f μ, μ > 1 → |gamma f μ| < B
  88
  89/-! ## RG Transport Integral -/
  90
  91/-- The λ-normalization constant: `λ = ln(φ)`. -/
  92def lambda : ℝ := Real.log phi
  93
  94/-- λ is positive. -/
  95theorem lambda_pos : lambda > 0 := by
  96  have h : 1 < phi := one_lt_phi
  97  exact Real.log_pos h
  98
  99/-! ## Canonical one-loop beta/gamma kernels (Level-B groundwork) -/
 100
 101/-- One-loop QCD beta coefficient in the convention `beta0 = 11 - 2*nf/3`. -/
 102def beta0QCD (nf : ℕ) : ℚ := (11 : ℚ) - (2 : ℚ) * nf / 3
 103
 104/-- Real-valued view of `beta0QCD`. -/
 105def beta0QCDReal (nf : ℕ) : ℝ := (beta0QCD nf : ℝ)
 106
 107/-- One-loop QCD running for `alpha_s`:
 108`d alpha_s / d ln mu = -(beta0/(2*pi)) * alpha_s^2`. -/
 109noncomputable def betaQCD1L (nf : ℕ) (alphaS : ℝ) : ℝ :=
 110  -((beta0QCDReal nf) / (2 * Real.pi)) * alphaS ^ 2
 111
 112/-- One-loop QED running with an effective charge-weight factor.
 113This keeps the kernel explicit while allowing policy-level charge sums. -/
 114noncomputable def betaQED1L (chargeWeight : ℝ) (alpha : ℝ) : ℝ :=
 115  (chargeWeight / (3 * Real.pi)) * alpha ^ 2
 116
 117/-- Minimal one-loop mass anomalous-dimension scaffold for QCD.
 118The exact scheme-dependent higher-loop expression is left to Level-B extensions. -/
 119noncomputable def gammaMassQCD1L (alphaS : ℝ) : ℝ :=
 120  (2 / Real.pi) * alphaS
 121
 122/-- Minimal one-loop mass anomalous-dimension scaffold for QED. -/
 123noncomputable def gammaMassQED1L (chargeSq : ℝ) (alpha : ℝ) : ℝ :=
 124  (3 * chargeSq / (4 * Real.pi)) * alpha
 125
 126theorem beta0QCD_nf0 : beta0QCD 0 = 11 := by
 127  norm_num [beta0QCD]
 128
 129theorem beta0QCD_asymp_free (nf : ℕ) (hnf : nf ≤ 16) : 0 < beta0QCD nf := by
 130  unfold beta0QCD
 131  have hnfQ : (nf : ℚ) ≤ 16 := by
 132    exact_mod_cast hnf
 133  have h_le : (2 : ℚ) * nf / 3 ≤ (2 : ℚ) * 16 / 3 := by
 134    exact div_le_div_of_nonneg_right (by nlinarith [hnfQ]) (by norm_num)
 135  have h_lt : (2 : ℚ) * 16 / 3 < 11 := by norm_num
 136  have h_frac_lt : (2 : ℚ) * nf / 3 < 11 := lt_of_le_of_lt h_le h_lt
 137  linarith
 138
 139theorem betaQCD1L_vanishes_at_zero (nf : ℕ) :
 140    betaQCD1L nf 0 = 0 := by
 141  simp [betaQCD1L]
 142
 143theorem gammaMassQCD1L_zero : gammaMassQCD1L 0 = 0 := by
 144  simp [gammaMassQCD1L]
 145
 146/-! ## RK4 integrator scaffold with enclosure bounds -/
 147
 148/-- RK4 increment from stage values `(k1,k2,k3,k4)`. -/
 149def rk4Increment (h k1 k2 k3 k4 : ℝ) : ℝ :=
 150  (h / 6) * (k1 + 2 * k2 + 2 * k3 + k4)
 151
 152/-- One RK4 step for `x' = f(x)` with step size `h`. -/
 153def rk4Step (f : ℝ → ℝ) (x h : ℝ) : ℝ :=
 154  let k1 := f x
 155  let k2 := f (x + (h / 2) * k1)
 156  let k3 := f (x + (h / 2) * k2)
 157  let k4 := f (x + h * k3)
 158  x + rk4Increment h k1 k2 k3 k4
 159
 160theorem rk4Step_eq_self_of_zero (f : ℝ → ℝ)
 161    (hzero : ∀ y, f y = 0) (x h : ℝ) :
 162    rk4Step f x h = x := by
 163  simp [rk4Step, rk4Increment, hzero]
 164
 165/-- Algebraic enclosure: if each RK4 stage is bounded by `M`, then one-step
 166deviation is bounded by `|h|*M`. -/
 167theorem abs_rk4Increment_le (M h k1 k2 k3 k4 : ℝ)
 168    (hk1 : |k1| ≤ M) (hk2 : |k2| ≤ M)
 169    (hk3 : |k3| ≤ M) (hk4 : |k4| ≤ M) :
 170    |rk4Increment h k1 k2 k3 k4| ≤ |h| * M := by
 171  have hsum1 : |k1 + 2 * k2 + 2 * k3 + k4| ≤ |k1| + |2 * k2 + 2 * k3 + k4| := by
 172    simpa [Real.norm_eq_abs, add_assoc] using
 173      (norm_add_le k1 (2 * k2 + 2 * k3 + k4))
 174  have hsum2 : |2 * k2 + 2 * k3 + k4| ≤ |2 * k2| + |2 * k3 + k4| := by
 175    simpa [Real.norm_eq_abs, add_assoc] using
 176      (norm_add_le (2 * k2) (2 * k3 + k4))
 177  have hsum3 : |2 * k3 + k4| ≤ |2 * k3| + |k4| := by
 178    simpa [Real.norm_eq_abs] using (norm_add_le (2 * k3) k4)
 179  have h2k2 : |2 * k2| = 2 * |k2| := by
 180    norm_num [abs_mul]
 181  have h2k3 : |2 * k3| = 2 * |k3| := by
 182    norm_num [abs_mul]
 183  have hsum :
 184      |k1 + 2 * k2 + 2 * k3 + k4| ≤ |k1| + 2 * |k2| + 2 * |k3| + |k4| := by
 185    nlinarith [hsum1, hsum2, hsum3, h2k2, h2k3]
 186  have hsumM : |k1 + 2 * k2 + 2 * k3 + k4| ≤ 6 * M := by
 187    nlinarith [hsum, hk1, hk2, hk3, hk4]
 188  calc
 189    |rk4Increment h k1 k2 k3 k4|
 190        = |h / 6| * |k1 + 2 * k2 + 2 * k3 + k4| := by
 191            simp [rk4Increment, abs_mul]
 192    _ = (|h| / 6) * |k1 + 2 * k2 + 2 * k3 + k4| := by
 193          simp [abs_div]
 194    _ ≤ (|h| / 6) * (6 * M) := by
 195          gcongr
 196    _ = |h| * M := by ring
 197
 198/-- RK4 one-step enclosure bound for function evaluations at the four RK stages. -/
 199theorem rk4Step_deviation_le (f : ℝ → ℝ) (x h M : ℝ)
 200    (hk1 : |f x| ≤ M)
 201    (hk2 : |f (x + (h / 2) * f x)| ≤ M)
 202    (hk3 : |f (x + (h / 2) * f (x + (h / 2) * f x))| ≤ M)
 203    (hk4 : |f (x + h * f (x + (h / 2) * f (x + (h / 2) * f x)))| ≤ M) :
 204    |rk4Step f x h - x| ≤ |h| * M := by
 205  unfold rk4Step
 206  set k1 : ℝ := f x
 207  set k2 : ℝ := f (x + (h / 2) * k1)
 208  set k3 : ℝ := f (x + (h / 2) * k2)
 209  set k4 : ℝ := f (x + h * k3)
 210  have hk1' : |k1| ≤ M := by simpa [k1] using hk1
 211  have hk2' : |k2| ≤ M := by simpa [k1, k2] using hk2
 212  have hk3' : |k3| ≤ M := by simpa [k1, k2, k3] using hk3
 213  have hk4' : |k4| ≤ M := by simpa [k1, k2, k3, k4] using hk4
 214  have hinc :
 215      |rk4Increment h k1 k2 k3 k4| ≤ |h| * M :=
 216    abs_rk4Increment_le M h k1 k2 k3 k4 hk1' hk2' hk3' hk4'
 217  have hstep : |(x + rk4Increment h k1 k2 k3 k4) - x| = |rk4Increment h k1 k2 k3 k4| := by
 218    ring_nf
 219  simpa [hstep]
 220
 221/-- The integrated residue from ln-scale `lnμ₀` to `lnμ₁`.
 222
 223    `f(μ₀, μ₁) = (1/λ) ∫_{lnμ₀}^{lnμ₁} γ(exp(t)) dt`
 224
 225    This is the abstract definition; the actual computation requires the SM kernels.
 226    We parameterize by an `AnomalousDimension` structure. -/
 227def integratedResidue (γ : AnomalousDimension) (f : Fermion) (lnμ₀ lnμ₁ : ℝ) : ℝ :=
 228  (1 / lambda) * ∫ t in Set.Icc lnμ₀ lnμ₁, γ.gamma f (Real.exp t)
 229
 230/-! ## Connection to Mass Formula -/
 231
 232/-- The running mass at scale μ, given the mass at scale μ₀ and an anomalous dimension.
 233
 234    `m(μ) = m(μ₀) · exp(-∫_{ln μ₀}^{ln μ} γ(μ') d(ln μ'))`
 235
 236    This is the solution to `d(ln m)/d(ln μ) = -γ_m(μ)`. -/
 237def runningMass (γ : AnomalousDimension) (f : Fermion) (m_μ₀ : ℝ) (lnμ₀ lnμ : ℝ) : ℝ :=
 238  m_μ₀ * Real.exp (-(∫ t in Set.Icc lnμ₀ lnμ, γ.gamma f (Real.exp t)))
 239
 240/-- The mass ratio between two scales.
 241
 242    `m(μ₁)/m(μ₀) = exp(-∫_{ln μ₀}^{ln μ₁} γ d(ln μ))` -/
 243theorem mass_ratio_formula (γ : AnomalousDimension) (f : Fermion) (m_μ₀ : ℝ)
 244    (lnμ₀ lnμ₁ : ℝ) (hm : m_μ₀ ≠ 0) :
 245    runningMass γ f m_μ₀ lnμ₀ lnμ₁ / m_μ₀ =
 246      Real.exp (-(∫ t in Set.Icc lnμ₀ lnμ₁, γ.gamma f (Real.exp t))) := by
 247  simp only [runningMass]
 248  field_simp
 249
 250/-! ## Anchor Relation -/
 251
 252/-- The anchor scale from the papers: μ⋆ = 182.201 GeV. -/
 253def muStar : ℝ := 182.201
 254
 255theorem muStar_pos : muStar > 0 := by norm_num [muStar]
 256
 257/-- ln(μ⋆) for use in integral bounds. -/
 258def lnMuStar : ℝ := Real.log muStar
 259
 260/-- The residue at the anchor, relative to a reference ln-scale.
 261
 262    `f_i(μ⋆, μ_ref) := (1/λ) ∫_{ln μ⋆}^{lnμ_ref} γ_i(exp(t)) dt`
 263
 264    This is what the axiom `f_residue` in `AnchorPolicy.lean` is intended to represent. -/
 265def residueAtAnchor (γ : AnomalousDimension) (f : Fermion) (lnμ_ref : ℝ) : ℝ :=
 266  integratedResidue γ f lnMuStar lnμ_ref
 267
 268/-- The claim of Single Anchor Phenomenology: at the anchor scale μ⋆, the residue
 269    equals the closed-form display F(Z).
 270
 271    `residueAtAnchor γ f (ln m_phys) ≈ gap(ZOf f)`
 272
 273    This is what `display_identity_at_anchor` in `AnchorPolicy.lean` asserts. -/
 274def anchorClaimHolds (γ : AnomalousDimension) (tolerance : ℝ) : Prop :=
 275  ∀ (f : Fermion) (lnμ_ref : ℝ),
 276    |residueAtAnchor γ f lnμ_ref - gap (ZOf f)| < tolerance
 277
 278/-! ## Stationarity at the Anchor -/
 279
 280/-- The derivative of the residue with respect to the upper integration limit.
 281    This equals (1/λ) · γ(exp(lnμ)) = (1/λ) · γ(μ) by the fundamental theorem of calculus.
 282
 283    Stationarity of the residue at μ⋆ means this vanishes, i.e., γ(μ⋆) = 0. -/
 284def residueDerivative (γ : AnomalousDimension) (f : Fermion) (lnμ : ℝ) : ℝ :=
 285  (1 / lambda) * γ.gamma f (Real.exp lnμ)
 286
 287theorem stationarity_iff_gamma_zero (γ : AnomalousDimension) (f : Fermion) :
 288    residueDerivative γ f lnMuStar = 0 ↔ γ.gamma f muStar = 0 := by
 289  simp only [residueDerivative, lnMuStar]
 290  rw [Real.exp_log muStar_pos]
 291  have hlambda : lambda ≠ 0 := ne_of_gt lambda_pos
 292  constructor
 293  · intro h
 294    have hmul : (1 / lambda) * γ.gamma f muStar = 0 := h
 295    have h1 : (1 / lambda) ≠ 0 := one_div_ne_zero hlambda
 296    exact (mul_eq_zero.mp hmul).resolve_left h1
 297  · intro h
 298    simp [h]
 299
 300/-! ## Relation to φ-Power Form -/
 301
 302/-- The mass ratio in φ-power form.
 303
 304    If `m(μ₁)/m(μ₀) = exp(-λ · f)`, then `m(μ₁)/m(μ₀) = φ^{-f}`.
 305
 306    Note: `-lambda * f_residue` parses as `(-lambda) * f_residue` by precedence. -/
 307theorem mass_ratio_phi_power (f_residue : ℝ) :
 308    Real.exp (-lambda * f_residue) = phi ^ (-f_residue) := by
 309  have hphi_pos : 0 < phi := lt_trans (by norm_num : (0 : ℝ) < 1) one_lt_phi
 310  simp only [lambda]
 311  -- `-Real.log phi * f_residue` equals `Real.log phi * (-f_residue)`
 312  have h1 : -Real.log phi * f_residue = Real.log phi * (-f_residue) := by ring
 313  rw [h1]
 314  -- Now goal is: Real.exp (Real.log phi * -f_residue) = phi ^ (-f_residue)
 315  have h2 : Real.log phi * -f_residue = -f_residue * Real.log phi := by ring
 316  rw [h2, ← Real.log_rpow hphi_pos, Real.exp_log (Real.rpow_pos_of_pos hphi_pos _)]
 317
 318/-! ## Summary -/
 319
 320/-
 321This module provides the mathematical framework for understanding the RG transport
 322that defines the empirical residue f^exp:
 323
 3241. **AnomalousDimension** captures the structure of γ_m(μ).
 3252. **integratedResidue** is the integral formula (1/λ)∫γ dt.
 3263. **residueAtAnchor** specializes to the anchor scale μ⋆.
 3274. **anchorClaimHolds** states the phenomenological claim that this equals gap(Z).
 3285. **stationarity_iff_gamma_zero** shows the stationarity condition.
 329
 330The actual SM kernels are NOT implemented here. This is the interface that such
 331an implementation would satisfy.
 332-/
 333
 334end
 335
 336end RGTransport
 337end Physics
 338end IndisputableMonolith
 339