IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Constants.AlphaDerivation
   4
   5/-!
   6# Tau Step Coefficient Exclusivity: Why (W + D/2) is Forced
   7
   8This module proves that the coefficient **(W + D/2)** in the tau generation step
   9is uniquely determined once we state the missing first-principles rule the
  10reviewer is asking for: an **admissible class** of dimension-dependent
  11corrections.
  12
  13## The Question
  14
  15In the tau generation step formula:
  16  `step_μ→τ = F - (W + D/2) · α`
  17
  18Why is the α-correction coefficient **W + D/2** and not:
  19- W + F/4  (using faces)
  20- W + E/8  (using edges)
  21- W + D(D-1)/4  (quadratic in D)
  22- W + D²/6  (another quadratic)
  23
  24All these alternatives evaluate to 18.5 in D=3!
  25
  26## The Answer
  27
  28The alternatives fall into two categories:
  29
  30**Category 1: Algebraically Equivalent**
  31- `F/4 = D/2` (since F = 2D by definition of hypercube faces)
  32- These are the SAME formula, just different notation.
  33
  34**Category 2: Numerically Coincident but Algebraically Distinct**
  35- `E/8`, `D(D-1)/4`, `D²/6` all equal 1.5 in D=3
  36- But they DIFFER from D/2 in other dimensions.
  37- They are ruled out once we require **axis additivity** (independent axes contribute
  38  additively) and **no constant offset**.
  39
  40## The Exclusivity Principles
  41
  421. **Axis Additivity**: If a correction term is a sum of independent per-axis
  43   contributions, then it must satisfy:
  44
  45     `f(0)=0` and `f(a+b)=f(a)+f(b)`.
  46
  47   This makes the correction linear in D (no cross-axis interaction terms).
  48
  492. **Calibration at D=3**: The tau step requires the dimension correction to be
  50   `3/2` when D=3 (i.e., the observed coefficient is `W + 3/2`).
  51
  52Under (1)+(2), the dimension correction is uniquely `D/2`.
  53-/
  54
  55namespace IndisputableMonolith
  56namespace Physics
  57namespace LeptonGenerations
  58namespace TauStepExclusivity
  59
  60open Real Constants.AlphaDerivation
  61
  62/-! ## Part 2: The Candidate Correction Terms -/
  63
  64/-- Candidate 1: D/2 (our claimed formula) -/
  65noncomputable def correction_D_half (d : ℕ) : ℝ := (d : ℝ) / 2
  66
  67/-- Candidate 2: F/4 = (2D)/4 = D/2 (algebraically equivalent!) -/
  68noncomputable def correction_F_quarter (d : ℕ) : ℝ := (cube_faces d : ℝ) / 4
  69
  70/-- Candidate 3: E/8 (edges divided by 8) -/
  71noncomputable def correction_E_eighth (d : ℕ) : ℝ := (cube_edges d : ℝ) / 8
  72
  73/-- Candidate 4: D(D-1)/4 (quadratic) -/
  74noncomputable def correction_D_quad1 (d : ℕ) : ℝ := (d : ℝ) * ((d : ℝ) - 1) / 4
  75
  76/-- Candidate 5: D²/6 (another quadratic) -/
  77noncomputable def correction_D_quad2 (d : ℕ) : ℝ := ((d : ℝ) ^ 2) / 6
  78
  79/-! ## Part 3: All Candidates Equal 1.5 in D=3 -/
  80
  81theorem D_half_at_3 : correction_D_half 3 = 3/2 := by
  82  unfold correction_D_half
  83  norm_num
  84
  85theorem F_quarter_at_3 : correction_F_quarter 3 = 3/2 := by
  86  unfold correction_F_quarter
  87  simp [cube_faces]
  88  norm_num
  89
  90theorem E_eighth_at_3 : correction_E_eighth 3 = 3/2 := by
  91  unfold correction_E_eighth
  92  simp [cube_edges]
  93  norm_num
  94
  95theorem D_quad1_at_3 : correction_D_quad1 3 = 3/2 := by
  96  unfold correction_D_quad1
  97  norm_num
  98
  99theorem D_quad2_at_3 : correction_D_quad2 3 = 3/2 := by
 100  unfold correction_D_quad2
 101  norm_num
 102
 103/-! ## Part 4: F/4 and D/2 are Algebraically Identical -/
 104
 105/-- **Key Identity**: F/4 = D/2 for ALL dimensions.
 106    This is not numerical coincidence—it's algebraic identity. -/
 107theorem F_quarter_eq_D_half : ∀ d : ℕ, correction_F_quarter d = correction_D_half d := by
 108  intro d
 109  unfold correction_F_quarter correction_D_half
 110  -- (2*d)/4 = d/2
 111  simp [cube_faces]
 112  ring
 113
 114/-- Corollary: F/4 is NOT a distinct alternative; it IS D/2. -/
 115theorem F_quarter_not_alternative :
 116    correction_F_quarter = correction_D_half := funext F_quarter_eq_D_half
 117
 118/-! ## Part 5: Axis-Additive Admissible Class -/
 119
 120/-! ### Axis additivity -/
 121
 122/-- Axis additivity: independent axes contribute additively, with no constant offset. -/
 123def AxisAdditive (f : ℕ → ℝ) : Prop :=
 124  f 0 = 0 ∧ ∀ a b : ℕ, f (a + b) = f a + f b
 125
 126/-- Any axis-additive function on ℕ is linear: f(d) = d * f(1). -/
 127theorem axisAdditive_linear (f : ℕ → ℝ) (h : AxisAdditive f) :
 128    ∀ d : ℕ, f d = (d : ℝ) * f 1 := by
 129  rcases h with ⟨h0, hadd⟩
 130  intro d
 131  induction d with
 132  | zero =>
 133      simp [h0]
 134  | succ d ih =>
 135      -- f(d+1) = f(d) + f(1)
 136      have hstep : f (d + 1) = f d + f 1 := by
 137        simpa using (hadd d 1)
 138      -- expand and use IH
 139      calc
 140        f (Nat.succ d) = f d + f 1 := by
 141          simpa [Nat.succ_eq_add_one] using hstep
 142        _ = ((d : ℝ) * f 1) + f 1 := by simpa [ih]
 143        _ = ((d : ℝ) + 1) * f 1 := by ring
 144        _ = ((Nat.succ d : ℝ) * f 1) := by
 145          simp [Nat.cast_succ, add_comm, add_left_comm, add_assoc]
 146
 147/-! ### Admissible correction terms -/
 148
 149/-- Admissible dimension correction: axis-additive and calibrated at D=3. -/
 150structure AdmissibleCorrection (f : ℕ → ℝ) : Prop where
 151  axisAdditive : AxisAdditive f
 152  calib_D3 : f 3 = 3 / 2
 153
 154/-- Uniqueness: any admissible correction is exactly D/2. -/
 155theorem admissible_unique (f : ℕ → ℝ) (h : AdmissibleCorrection f) :
 156    ∀ d : ℕ, f d = (d : ℝ) / 2 := by
 157  have hlin := axisAdditive_linear f h.axisAdditive
 158  -- use calibration at d=3 to solve for f(1)
 159  have h3 : f 3 = (3 : ℝ) * f 1 := hlin 3
 160  have hf1 : f 1 = (1 : ℝ) / 2 := by
 161    -- from f3 = 3/2 = 3*f1
 162    have : (3 : ℝ) * f 1 = (3 : ℝ) / 2 := by
 163      -- rewrite h3 using calib
 164      rw [← h3, h.calib_D3]
 165    -- divide by 3
 166    have h3ne : (3 : ℝ) ≠ 0 := by norm_num
 167    -- f1 = (3/2)/3 = 1/2
 168    field_simp [h3ne] at this
 169    -- `this` is now: 3 * (2 * f1) = 3  (or equivalent); solve
 170    nlinarith
 171  intro d
 172  have : f d = (d : ℝ) * f 1 := hlin d
 173  -- substitute f1 = 1/2
 174  rw [this, hf1]
 175  ring
 176
 177/-! ### Instances and exclusions -/
 178
 179/-- D/2 is admissible. -/
 180theorem D_half_admissible : AdmissibleCorrection correction_D_half := by
 181  refine ⟨?_, ?_⟩
 182  · refine ⟨by simp [correction_D_half], ?_⟩
 183    intro a b
 184    simp [correction_D_half, Nat.cast_add, add_div]
 185  · simpa [correction_D_half]
 186
 187/-- F/4 is admissible (because it equals D/2). -/
 188theorem F_quarter_admissible : AdmissibleCorrection correction_F_quarter := by
 189  -- transport admissibility through definitional equality
 190  have hEq : correction_F_quarter = correction_D_half := funext F_quarter_eq_D_half
 191  -- rewrite and reuse
 192  simpa [hEq] using D_half_admissible
 193
 194/-! ## Part 6: Excluding Common Alternatives (they violate axis additivity) -/
 195
 196/-- E/8 is not axis-additive (witness: 2+2). -/
 197theorem E_eighth_not_axisAdditive : ¬ AxisAdditive correction_E_eighth := by
 198  intro h
 199  rcases h with ⟨h0, hadd⟩
 200  have h22 : correction_E_eighth (2 + 2) = correction_E_eighth 2 + correction_E_eighth 2 := hadd 2 2
 201  -- compute both sides
 202  unfold correction_E_eighth at h22
 203  simp [cube_edges] at h22
 204  -- LHS = 4, RHS = 1
 205  norm_num at h22
 206
 207/-- D(D-1)/4 is not axis-additive (witness: 1+1). -/
 208theorem D_quad1_not_axisAdditive : ¬ AxisAdditive correction_D_quad1 := by
 209  intro h
 210  rcases h with ⟨h0, hadd⟩
 211  have h11 : correction_D_quad1 (1 + 1) = correction_D_quad1 1 + correction_D_quad1 1 := hadd 1 1
 212  unfold correction_D_quad1 at h11
 213  norm_num at h11
 214
 215/-- D²/6 is not axis-additive (witness: 1+1). -/
 216theorem D_quad2_not_axisAdditive : ¬ AxisAdditive correction_D_quad2 := by
 217  intro h
 218  rcases h with ⟨h0, hadd⟩
 219  have h11 : correction_D_quad2 (1 + 1) = correction_D_quad2 1 + correction_D_quad2 1 := hadd 1 1
 220  unfold correction_D_quad2 at h11
 221  norm_num at h11
 222
 223/-! ## Part 7: Main statement (uniqueness within the admissible class) -/
 224
 225/-- **Main theorem**: any admissible correction is exactly `D/2`. -/
 226theorem tau_correction_unique_admissible (f : ℕ → ℝ) (h : AdmissibleCorrection f) :
 227    ∀ d : ℕ, f d = correction_D_half d := by
 228  intro d
 229  have := admissible_unique f h d
 230  simpa [correction_D_half] using this
 231
 232/-! ## Summary
 233
 234**The Exclusivity Proof**:
 235
 2361. Among the proposed alternatives {D/2, F/4, E/8, D(D-1)/4, D²/6}:
 237   - F/4 = D/2 algebraically (not a distinct alternative)
 238   - E/8, D(D-1)/4, D²/6 violate axis additivity (they are not sums of per-axis contributions)
 239
 2402. Under the admissible class (axis-additive + calibrated at D=3), the correction term is unique:
 241   `f(D) = D/2`.
 242
 243**Conclusion**: the dimension contribution in the tau step coefficient is uniquely `D/2`
 244within the stated admissible correction class.
 245-/
 246
 247end TauStepExclusivity
 248end LeptonGenerations
 249end Physics
 250end IndisputableMonolith
 251