IndisputableMonolith.Verification.LeptonCoefficientPerturbation

   1import Mathlib
   2import IndisputableMonolith.Cost.JcostCore
   3import IndisputableMonolith.Constants.Alpha
   4import IndisputableMonolith.Physics.MassTopology
   5import IndisputableMonolith.Physics.ElectronMass.Necessity
   6import IndisputableMonolith.Constants.AlphaDerivation
   7
   8/-!
   9# Lepton Coefficient Perturbation Scaffold
  10
  11This module records a concrete perturbative step toward deriving the lepton
  12`α`-correction channels from first principles.
  13
  14We use the proved small-strain expansion of `Jcost` at `x = 1 + ε` and
  15specialize to `ε = α`, where `α` is already bounded in the framework.
  16
  17The outcome is an explicit channel decomposition with edge aggregation:
  18
  19* quadratic channel `α²` (leading),
  20* cubic channel scaling as edge-count times `α³`.
  21
  22This now provides the perturbative channel core used by the mass-layer O4
  23closure (`Masses.JCostPerturbation`): it removes ad-hoc handling of correction
  24orders and ties them to the existing `J`-cost calculus surface.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace Verification
  29namespace LeptonCoefficientPerturbation
  30
  31open Constants
  32open Physics.MassTopology
  33
  34noncomputable section
  35
  36/-- `α` is small enough for the `Jcost(1+ε)` expansion radius used in `JcostCore`. -/
  37lemma alpha_abs_le_half : |alpha| ≤ (1 : ℝ) / 2 := by
  38  have hα := Physics.ElectronMass.Necessity.alpha_bounds
  39  have hα_nonneg : 0 ≤ alpha := le_of_lt (lt_trans (by norm_num : (0 : ℝ) < 0.007297) hα.1)
  40  rw [abs_of_nonneg hα_nonneg]
  41  linarith
  42
  43/-- Specialize the proved `Jcost` small-strain expansion to `ε = α`. -/
  44theorem jcost_one_plus_alpha_expansion :
  45    ∃ c : ℝ, Cost.Jcost (1 + alpha) = alpha ^ 2 / 2 + c * alpha ^ 3 ∧ |c| ≤ 2 := by
  46  simpa using Cost.Jcost_one_plus_eps_quadratic alpha alpha_abs_le_half
  47
  48/-- Equivalent doubled form: quadratic coefficient normalized to `1`. -/
  49theorem two_jcost_one_plus_alpha_expansion :
  50    ∃ c : ℝ, 2 * Cost.Jcost (1 + alpha) = alpha ^ 2 + c * alpha ^ 3 ∧ |c| ≤ 4 := by
  51  rcases jcost_one_plus_alpha_expansion with ⟨c, hc, hcb⟩
  52  refine ⟨2 * c, ?_, ?_⟩
  53  · nlinarith [hc]
  54  · have habs : |2 * c| = 2 * |c| := by
  55      calc
  56        |2 * c| = |(2 : ℝ)| * |c| := by simp [abs_mul]
  57        _ = 2 * |c| := by norm_num
  58    have h2 : 2 * |c| ≤ 4 := by nlinarith [hcb]
  59    simpa [habs] using h2
  60
  61/-- Uniqueness of the cubic channel coefficient in the doubled `Jcost(1+α)`
  62representation: once
  63`2*Jcost(1+α) = α² + c*α³` is fixed, `c` is unique. -/
  64theorem two_jcost_cubic_coeff_unique
  65    {c1 c2 : ℝ}
  66    (h1 : 2 * Cost.Jcost (1 + alpha) = alpha ^ 2 + c1 * alpha ^ 3)
  67    (h2 : 2 * Cost.Jcost (1 + alpha) = alpha ^ 2 + c2 * alpha ^ 3) :
  68    c1 = c2 := by
  69  have hα := Physics.ElectronMass.Necessity.alpha_bounds
  70  have hα_pos : 0 < alpha := by linarith [hα.1]
  71  have hα_ne : alpha ≠ 0 := ne_of_gt hα_pos
  72  have hmul : c1 * alpha ^ 3 = c2 * alpha ^ 3 := by linarith [h1, h2]
  73  exact mul_right_cancel₀ (pow_ne_zero 3 hα_ne) hmul
  74
  75/-- Existence + uniqueness form of the doubled-channel perturbative coefficient. -/
  76theorem exists_unique_two_jcost_channel_coeff :
  77    ∃! c : ℝ, 2 * Cost.Jcost (1 + alpha) = alpha ^ 2 + c * alpha ^ 3 := by
  78  rcases two_jcost_one_plus_alpha_expansion with ⟨c, hc, _hcb⟩
  79  refine ⟨c, hc, ?_⟩
  80  intro c' hc'
  81  exact (two_jcost_cubic_coeff_unique (c1 := c) (c2 := c') hc hc').symm
  82
  83/-- The 3-cube edge count in real form. -/
  84lemma E_total_eq_twelve : (E_total : ℝ) = 12 := by
  85  norm_num [E_total, AlphaDerivation.cube_edges]
  86
  87/-- Edge-aggregated perturbation form: cubic channel remains bounded and scales with edge count. -/
  88theorem edge_aggregated_two_jcost_one_plus_alpha :
  89    ∃ C : ℝ,
  90      (E_total : ℝ) * (2 * Cost.Jcost (1 + alpha))
  91        = (E_total : ℝ) * alpha ^ 2 + C * alpha ^ 3 ∧
  92      |C| ≤ 4 * (E_total : ℝ) := by
  93  rcases two_jcost_one_plus_alpha_expansion with ⟨c, hc, hcb⟩
  94  refine ⟨(E_total : ℝ) * c, ?_, ?_⟩
  95  · nlinarith [hc]
  96  · have hE_nonneg : 0 ≤ (E_total : ℝ) := by positivity
  97    have habs : |(E_total : ℝ) * c| = (E_total : ℝ) * |c| := by
  98      rw [abs_mul, abs_of_nonneg hE_nonneg]
  99    have hbound : (E_total : ℝ) * |c| ≤ (E_total : ℝ) * 4 :=
 100      mul_le_mul_of_nonneg_left hcb hE_nonneg
 101    calc
 102      |(E_total : ℝ) * c| = (E_total : ℝ) * |c| := habs
 103      _ ≤ (E_total : ℝ) * 4 := hbound
 104      _ = 4 * (E_total : ℝ) := by ring
 105
 106/-- With current `α` bounds, the edge-cubic channel is strictly subleading to `α²`. -/
 107theorem edge_cubic_channel_subleading :
 108    (E_total : ℝ) * alpha ^ 3 < alpha ^ 2 := by
 109  have hα := Physics.ElectronMass.Necessity.alpha_bounds
 110  have hα_pos : 0 < alpha := lt_trans (by norm_num : (0 : ℝ) < 0.007297) hα.1
 111  have hα_lt_1_over_12 : alpha < (1 / 12 : ℝ) := by
 112    linarith [hα.2]
 113  have hEalpha_lt_one : (E_total : ℝ) * alpha < 1 := by
 114    have hE : (E_total : ℝ) = 12 := E_total_eq_twelve
 115    calc
 116      (E_total : ℝ) * alpha = 12 * alpha := by simp [hE]
 117      _ < 12 * (1 / 12 : ℝ) := by gcongr
 118      _ = 1 := by ring
 119  have hα2_pos : 0 < alpha ^ 2 := by positivity
 120  calc
 121    (E_total : ℝ) * alpha ^ 3 = ((E_total : ℝ) * alpha) * alpha ^ 2 := by ring
 122    _ < 1 * alpha ^ 2 := by exact mul_lt_mul_of_pos_right hEalpha_lt_one hα2_pos
 123    _ = alpha ^ 2 := by ring
 124
 125/-- Rephrase `MassTopology`'s cubic correction as the 12-edge channel. -/
 126theorem correction_order_3_eq_twelve_alpha_cube :
 127    correction_order_3 = 12 * alpha ^ 3 := by
 128  simp [correction_order_3, E_total_eq_twelve]
 129
 130/-- The radiative correction used in `refined_shift` has explicit channel decomposition. -/
 131theorem radiative_correction_channel_decomposition :
 132    radiative_correction = alpha ^ 2 + 12 * alpha ^ 3 := by
 133  unfold radiative_correction correction_order_2
 134  rw [correction_order_3_eq_twelve_alpha_cube]
 135
 136/-- O4 perturbative core certificate at the verification layer:
 137    the doubled `Jcost(1+α)` channel form, the explicit 12-edge cubic channel,
 138    and the resulting radiative decomposition used downstream in mass-layer forcing. -/
 139theorem o4_perturbative_core_certificate :
 140    (∃ c : ℝ, 2 * Cost.Jcost (1 + alpha) = alpha ^ 2 + c * alpha ^ 3 ∧ |c| ≤ 4) ∧
 141    correction_order_3 = 12 * alpha ^ 3 ∧
 142    radiative_correction = alpha ^ 2 + 12 * alpha ^ 3 := by
 143  exact ⟨two_jcost_one_plus_alpha_expansion,
 144    correction_order_3_eq_twelve_alpha_cube,
 145    radiative_correction_channel_decomposition⟩
 146
 147end
 148end LeptonCoefficientPerturbation
 149end Verification
 150end IndisputableMonolith
 151