IndisputableMonolith.Masses.NeutrinoYardstick

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Neutrino Yardstick Derivation
   6
   7The neutrino sector yardstick is the last unfixed mass parameter.
   8This module derives constraints on the neutrino yardstick from the
   9existing mass law structure and cosmological bounds.
  10
  11## Neutrino Sector Properties
  12
  13- ZOf = 0 (neutral, chiral) — unique among fermion sectors
  14- Gap function: gap(0) = 0 (no gap correction)
  15- Rungs: ν₁ = 0, ν₂ = 11, ν₃ = 19 (from RSBridge.Anchor)
  16- Baseline: neutrino_baseline_int = -54
  17
  18## Constraint: Cosmological Mass Sum Bound
  19
  20Planck+DESI: Σmᵢ < 0.12 eV (95% CL).
  21The yardstick Y_ν must satisfy:
  22  Y_ν × (φ^(0-8) + φ^(11-8) + φ^(19-8)) < 0.12 eV
  23
  24## Status: THEOREM (constraints) + HYPOTHESIS (unique determination)
  25-/
  26
  27namespace IndisputableMonolith.Masses.NeutrinoYardstick
  28
  29open Constants
  30
  31/-- The three neutrino rung assignments. -/
  32def nu_rungs : Fin 3 → ℤ := ![0, 11, 19]
  33
  34/-- Mass formula: m_i = Y × φ^(rung_i - 8). -/
  35noncomputable def nuMass (Y : ℝ) (i : Fin 3) : ℝ :=
  36  Y * phi ^ (nu_rungs i - 8)
  37
  38/-- Sum of neutrino masses as function of yardstick. -/
  39noncomputable def nuMassSum (Y : ℝ) : ℝ :=
  40  nuMass Y 0 + nuMass Y 1 + nuMass Y 2
  41
  42/-- The mass sum factor: φ^(-8) + φ^3 + φ^11. -/
  43noncomputable def sumFactor : ℝ :=
  44  phi ^ (-8 : ℤ) + phi ^ (3 : ℤ) + phi ^ (11 : ℤ)
  45
  46theorem sum_factor_pos : sumFactor > 0 := by
  47  unfold sumFactor
  48  have h1 : phi ^ (-8 : ℤ) > 0 := zpow_pos phi_pos _
  49  have h2 : phi ^ (3 : ℤ) > 0 := zpow_pos phi_pos _
  50  have h3 : phi ^ (11 : ℤ) > 0 := zpow_pos phi_pos _
  51  linarith
  52
  53/-- The mass sum is linear in the yardstick. -/
  54theorem nuMassSum_eq_Y_times_factor (Y : ℝ) :
  55    nuMassSum Y = Y * sumFactor := by
  56  unfold nuMassSum nuMass sumFactor nu_rungs
  57  simp [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
  58  ring
  59
  60/-- Cosmological bound constrains the yardstick.
  61    Σmᵢ < 0.12 eV ⟹ Y < 0.12 / sumFactor. -/
  62theorem yardstick_upper_bound (Y : ℝ) (hY : Y > 0)
  63    (h_cosmo : nuMassSum Y < 0.12) :
  64    Y < 0.12 / sumFactor := by
  65  rw [nuMassSum_eq_Y_times_factor] at h_cosmo
  66  exact (div_lt_iff sum_factor_pos).mpr h_cosmo |>.2 |> fun h => by linarith [h]
  67
  68/-- Normal mass ordering: ν₃ > ν₂ > ν₁ for positive yardstick. -/
  69theorem normal_ordering (Y : ℝ) (hY : Y > 0) :
  70    nuMass Y 0 < nuMass Y 1 ∧ nuMass Y 1 < nuMass Y 2 := by
  71  unfold nuMass nu_rungs
  72  simp [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
  73  constructor
  74  · apply mul_lt_mul_of_pos_left _ hY
  75    apply zpow_lt_zpow_right phi_gt_one; omega
  76  · apply mul_lt_mul_of_pos_left _ hY
  77    apply zpow_lt_zpow_right phi_gt_one; omega
  78
  79/-- Mass-squared ratio is determined by rung differences. -/
  80theorem mass_ratio_from_rungs (Y : ℝ) (hY : Y > 0) :
  81    nuMass Y 2 / nuMass Y 1 = phi ^ (8 : ℤ) := by
  82  unfold nuMass nu_rungs
  83  simp [Matrix.cons_val_one, Matrix.head_cons]
  84  rw [mul_div_mul_left _ _ (ne_of_gt hY)]
  85  rw [← zpow_sub₀ (ne_of_gt phi_pos)]
  86  norm_num
  87
  88end IndisputableMonolith.Masses.NeutrinoYardstick
  89