IndisputableMonolith.Verification.NeutrinoBaselineChoiceSet

   1import Mathlib
   2import IndisputableMonolith.Physics.NeutrinoSector
   3
   4/-!
   5# Neutrino Baseline Choice-Set Enumeration (O5 Progress)
   6
   7This module adds a finite-search closure step for the neutrino absolute baseline
   8question:
   9
  10- Parameterize the lightest neutrino rung by a quarter-rung numerator `r1_num`.
  11- Enforce the structural gap profile (`+2`, then `+7/2`) in numerator form.
  12- Impose a deep-atmospheric window for `r3` and the canonical `-1/4` phase class.
  13
  14Under these constraints, the admissible baseline set collapses to a singleton
  15`r1 = -239/4`.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Verification
  20namespace NeutrinoBaselineChoiceSet
  21
  22open Physics.NeutrinoSector
  23
  24/-- Candidate encoded by the quarter-rung numerator for `r1 = r1_num / 4`. -/
  25structure BaselineCandidate where
  26  r1_num : ℤ
  27  deriving Repr, DecidableEq
  28
  29/-- Numerator of `r2`, using the structural `r2 - r1 = 2` gap (`= 8/4`). -/
  30def r2_num (c : BaselineCandidate) : ℤ := c.r1_num + 8
  31
  32/-- Numerator of `r3`, using `r3 - r2 = 7/2` (`= 14/4`). -/
  33def r3_num (c : BaselineCandidate) : ℤ := c.r1_num + 22
  34
  35/-- Convert a quarter-rung numerator to a rational rung value. -/
  36def quarterRung (n : ℤ) : ℚ := (n : ℚ) / 4
  37
  38def r1 (c : BaselineCandidate) : ℚ := quarterRung c.r1_num
  39def r2 (c : BaselineCandidate) : ℚ := quarterRung (r2_num c)
  40def r3 (c : BaselineCandidate) : ℚ := quarterRung (r3_num c)
  41
  42/-- Canonical baseline candidate from the current neutrino construction. -/
  43def canonicalCandidate : BaselineCandidate := { r1_num := -239 }
  44
  45/-- Finite search window for deep-ladder baselines (contains the canonical value). -/
  46def candidatePool : List BaselineCandidate :=
  47  (List.range 121).map (fun n => { r1_num := (n : ℤ) - 300 })
  48
  49/-- Atmospheric rung must lie in the deep window `(-55, -54)`, i.e. `(-220, -216)/4`. -/
  50def deepAtmosphericWindow (c : BaselineCandidate) : Bool :=
  51  decide ((-220 : ℤ) < r3_num c ∧ r3_num c < (-216 : ℤ))
  52
  53/-- Canonical 8-tick phase class: atmospheric rung is at `integer - 1/4`. -/
  54def quarterPhaseClass (c : BaselineCandidate) : Bool :=
  55  decide (((r3_num c + 1) % 4) = (0 : ℤ))
  56
  57/-- Structural gap profile in doubled/quarter coordinates. -/
  58def structuralGapProfile (c : BaselineCandidate) : Bool :=
  59  decide (r2_num c - c.r1_num = 8 ∧ r3_num c - r2_num c = 14)
  60
  61/-- Combined admissibility filter for the baseline search. -/
  62def admissible (c : BaselineCandidate) : Bool :=
  63  deepAtmosphericWindow c && quarterPhaseClass c && structuralGapProfile c
  64
  65def validCandidates : List BaselineCandidate :=
  66  candidatePool.filter admissible
  67
  68/-- "Deepest edge-only sublattice" condition for atmospheric numerators:
  69in the deep window and in the canonical `-1/4` phase class. -/
  70def deepestEdgeOnlyAtmospheric (n : ℤ) : Prop :=
  71  ((-220 : ℤ) < n ∧ n < (-216 : ℤ)) ∧ (((n + 1) % 4) = (0 : ℤ))
  72
  73theorem candidate_pool_count : candidatePool.length = 121 := by
  74  native_decide
  75
  76theorem structural_gap_profile_holds (c : BaselineCandidate) :
  77    structuralGapProfile c = true := by
  78  simp [structuralGapProfile, r2_num, r3_num]
  79
  80/-- Structural atmospheric numerator from deepest edge level (`rung_nu3 = -54`)
  81and quarter-phase offset (`-1/4`): `4*(-54) - 1 = -217`. -/
  82theorem deepest_edge_atmospheric_num_eq :
  83    (4 * rung_nu3 - 1 : ℤ) = -217 := by
  84  norm_num [rung_nu3]
  85
  86/-- Deep-window filter is forced once the atmospheric numerator is fixed by
  87edge confinement to `4*rung_nu3 - 1`. -/
  88theorem deep_window_forced_from_edge_confinement (c : BaselineCandidate)
  89    (hdeep : r3_num c = (4 * rung_nu3 - 1 : ℤ)) :
  90    deepAtmosphericWindow c = true := by
  91  have hr3 : r3_num c = -217 := by
  92    simpa [deepest_edge_atmospheric_num_eq] using hdeep
  93  simp [deepAtmosphericWindow, hr3]
  94
  95/-- Quarter-phase (`-1/4`) class is forced by the same deepest-edge atmospheric
  96numerator, via 8-tick modular arithmetic. -/
  97theorem quarter_phase_forced_from_eight_tick_offset (c : BaselineCandidate)
  98    (hdeep : r3_num c = (4 * rung_nu3 - 1 : ℤ)) :
  99    quarterPhaseClass c = true := by
 100  have hr3 : r3_num c = -217 := by
 101    simpa [deepest_edge_atmospheric_num_eq] using hdeep
 102  simp [quarterPhaseClass, hr3]
 103
 104/-- The deep-window and quarter-phase filters are jointly forced by the
 105edge-confinement atmospheric numerator. -/
 106theorem filter_pair_forced_from_edge_confinement (c : BaselineCandidate)
 107    (hdeep : r3_num c = (4 * rung_nu3 - 1 : ℤ)) :
 108    deepAtmosphericWindow c = true ∧ quarterPhaseClass c = true := by
 109  exact ⟨deep_window_forced_from_edge_confinement c hdeep,
 110    quarter_phase_forced_from_eight_tick_offset c hdeep⟩
 111
 112/-- Within the deep window, the `-1/4` phase class picks a unique atmospheric numerator. -/
 113theorem deepest_edge_only_forces_atmospheric_num (n : ℤ)
 114    (h : deepestEdgeOnlyAtmospheric n) :
 115    n = -217 := by
 116  rcases h with ⟨hwin, hphase⟩
 117  have hdiv : (4 : ℤ) ∣ (n + 1) := (Int.dvd_iff_emod_eq_zero).2 hphase
 118  rcases hdiv with ⟨k, hk⟩
 119  omega
 120
 121/-- The deep-atmospheric window plus quarter-phase class force `r3_num = -217`. -/
 122theorem deep_window_phase_forces_r3_num (c : BaselineCandidate)
 123    (hwin : deepAtmosphericWindow c = true)
 124    (hphase : quarterPhaseClass c = true) :
 125    r3_num c = -217 := by
 126  have hwin' : (-220 : ℤ) < r3_num c ∧ r3_num c < (-216 : ℤ) := by
 127    exact decide_eq_true_eq.mp (by simpa [deepAtmosphericWindow] using hwin)
 128  have hphase' : ((r3_num c + 1) % 4) = (0 : ℤ) := by
 129    exact decide_eq_true_eq.mp (by simpa [quarterPhaseClass] using hphase)
 130  exact deepest_edge_only_forces_atmospheric_num (r3_num c) ⟨hwin', hphase'⟩
 131
 132/-- Under the same filters, the atmospheric rung value is uniquely `-217/4`. -/
 133theorem deep_window_phase_forces_r3_value (c : BaselineCandidate)
 134    (hwin : deepAtmosphericWindow c = true)
 135    (hphase : quarterPhaseClass c = true) :
 136    r3 c = (-217 : ℚ) / 4 := by
 137  have hr3 : r3_num c = -217 := deep_window_phase_forces_r3_num c hwin hphase
 138  simp [r3, quarterRung, hr3]
 139
 140/-- With fixed spacing (`r3_num = r1_num + 22`), the same filters force `r1_num = -239`. -/
 141theorem deep_window_phase_forces_r1_num (c : BaselineCandidate)
 142    (hwin : deepAtmosphericWindow c = true)
 143    (hphase : quarterPhaseClass c = true) :
 144    c.r1_num = -239 := by
 145  have hr3 : r3_num c = -217 := deep_window_phase_forces_r3_num c hwin hphase
 146  have hr3' : c.r1_num + 22 = (-217 : ℤ) := by simpa [r3_num] using hr3
 147  omega
 148
 149/-- Corresponding forced baseline rung value. -/
 150theorem deep_window_phase_forces_r1_value (c : BaselineCandidate)
 151    (hwin : deepAtmosphericWindow c = true)
 152    (hphase : quarterPhaseClass c = true) :
 153    r1 c = (-239 : ℚ) / 4 := by
 154  have hr1 : c.r1_num = -239 := deep_window_phase_forces_r1_num c hwin hphase
 155  simp [r1, quarterRung, hr1]
 156
 157/-- Deep-window forcing aligns exactly with the canonical atmospheric rung `res_nu3`. -/
 158theorem deep_window_phase_forces_res_nu3 (c : BaselineCandidate)
 159    (hwin : deepAtmosphericWindow c = true)
 160    (hphase : quarterPhaseClass c = true) :
 161    r3 c = res_nu3 := by
 162  calc
 163    r3 c = (-217 : ℚ) / 4 := deep_window_phase_forces_r3_value c hwin hphase
 164    _ = res_nu3 := by simpa using res_nu3_simp.symm
 165
 166/-- With built-in spacing, the same forcing aligns with the canonical baseline `res_nu1`. -/
 167theorem deep_window_phase_forces_res_nu1 (c : BaselineCandidate)
 168    (hwin : deepAtmosphericWindow c = true)
 169    (hphase : quarterPhaseClass c = true) :
 170    r1 c = res_nu1 := by
 171  calc
 172    r1 c = (-239 : ℚ) / 4 := deep_window_phase_forces_r1_value c hwin hphase
 173    _ = res_nu1 := by simpa using res_nu1_simp.symm
 174
 175/-- Full baseline forcing from edge-confinement atmospheric level:
 176filters are forced, then `r3`/`r1` collapse to canonical `res_nu3`/`res_nu1`. -/
 177theorem edge_confinement_forces_canonical_baseline (c : BaselineCandidate)
 178    (hdeep : r3_num c = (4 * rung_nu3 - 1 : ℤ)) :
 179    r3 c = res_nu3 ∧ r1 c = res_nu1 := by
 180  have hpair : deepAtmosphericWindow c = true ∧ quarterPhaseClass c = true :=
 181    filter_pair_forced_from_edge_confinement c hdeep
 182  exact ⟨deep_window_phase_forces_res_nu3 c hpair.1 hpair.2,
 183    deep_window_phase_forces_res_nu1 c hpair.1 hpair.2⟩
 184
 185/-- Absolute baseline numerator forced from deep-ladder atmospheric confinement
 186plus fixed structural spacing `r3_num = r1_num + 22`. -/
 187theorem absolute_baseline_num_forced_from_deep_ladder (c : BaselineCandidate)
 188    (hdeep : r3_num c = (4 * rung_nu3 - 1 : ℤ)) :
 189    c.r1_num = (4 * rung_nu3 - 1 : ℤ) - 22 := by
 190  have hr3 : c.r1_num + 22 = (4 * rung_nu3 - 1 : ℤ) := by
 191    simpa [r3_num] using hdeep
 192  omega
 193
 194/-- Numeric form of the same forced baseline numerator at `D=3`: `r1_num = -239`. -/
 195theorem absolute_baseline_num_forced_eq_neg239 (c : BaselineCandidate)
 196    (hdeep : r3_num c = (4 * rung_nu3 - 1 : ℤ)) :
 197    c.r1_num = -239 := by
 198  calc
 199    c.r1_num = (4 * rung_nu3 - 1 : ℤ) - 22 :=
 200      absolute_baseline_num_forced_from_deep_ladder c hdeep
 201    _ = -239 := by norm_num [rung_nu3]
 202
 203/-- O5' iff surface: deep-ladder atmospheric confinement is equivalent to the
 204canonical baseline candidate (single-field structure). -/
 205theorem deep_ladder_constraint_iff_canonical_candidate (c : BaselineCandidate) :
 206    (r3_num c = (4 * rung_nu3 - 1 : ℤ)) ↔ c = canonicalCandidate := by
 207  constructor
 208  · intro hdeep
 209    have hr1 : c.r1_num = -239 := absolute_baseline_num_forced_eq_neg239 c hdeep
 210    cases c
 211    simp [canonicalCandidate] at hr1 ⊢
 212    simpa using hr1
 213  · intro hc
 214    subst hc
 215    simp [canonicalCandidate, r3_num, rung_nu3]
 216
 217/-- Baseline candidate forced directly by deep-ladder atmospheric geometry:
 218`r3_num = 4 * rung_nu3 - 1` and fixed spacing `r3_num = r1_num + 22`. -/
 219def deepLadderForcedCandidate : BaselineCandidate where
 220  r1_num := (4 * rung_nu3 - 1 : ℤ) - 22
 221
 222/-- The deep-ladder forced candidate is exactly the canonical one. -/
 223theorem deep_ladder_forced_candidate_eq_canonical :
 224    deepLadderForcedCandidate = canonicalCandidate := by
 225  simp [deepLadderForcedCandidate, canonicalCandidate, rung_nu3]
 226
 227/-- The deep-ladder forced candidate reproduces canonical `res_nu3`/`res_nu1`
 228without any extra filter assumptions. -/
 229theorem deep_ladder_geometry_forces_canonical_baseline :
 230    r3 deepLadderForcedCandidate = res_nu3 ∧
 231    r1 deepLadderForcedCandidate = res_nu1 := by
 232  have hdeep : r3_num deepLadderForcedCandidate = (4 * rung_nu3 - 1 : ℤ) := by
 233    simp [r3_num, deepLadderForcedCandidate]
 234  simpa using edge_confinement_forces_canonical_baseline deepLadderForcedCandidate hdeep
 235
 236theorem valid_candidate_count : validCandidates.length = 1 := by
 237  native_decide
 238
 239theorem valid_candidates_singleton :
 240    validCandidates = [canonicalCandidate] := by
 241  native_decide
 242
 243theorem canonical_is_valid :
 244    canonicalCandidate ∈ validCandidates := by
 245  rw [valid_candidates_singleton]
 246  simp
 247
 248theorem unique_valid_candidate (c : BaselineCandidate) (hc : c ∈ validCandidates) :
 249    c = canonicalCandidate := by
 250  rw [valid_candidates_singleton] at hc
 251  simpa using hc
 252
 253/-- The singleton baseline agrees with the neutrino module baseline rung. -/
 254theorem canonical_r1_matches_res_nu1 :
 255    r1 canonicalCandidate = res_nu1 := by
 256  simpa [r1, quarterRung, canonicalCandidate] using res_nu1_simp.symm
 257
 258/-- The induced atmospheric rung from the singleton baseline matches `res_nu3`. -/
 259theorem canonical_r3_matches_res_nu3 :
 260    r3 canonicalCandidate = res_nu3 := by
 261  have h : r3 canonicalCandidate = (-217 : ℚ) / 4 := by
 262    norm_num [r3, quarterRung, r3_num, canonicalCandidate]
 263  calc
 264    r3 canonicalCandidate = (-217 : ℚ) / 4 := h
 265    _ = res_nu3 := by simpa using res_nu3_simp.symm
 266
 267/-- Enumerated-choice closure summary for O5 under the current filter set. -/
 268theorem baseline_choice_set_collapsed :
 269    validCandidates = [canonicalCandidate] := valid_candidates_singleton
 270
 271/-- Any admissible baseline reproduces the current `res_nu1` value. -/
 272theorem admissible_baselines_match_res_nu1 (c : BaselineCandidate) (hc : c ∈ validCandidates) :
 273    r1 c = res_nu1 := by
 274  have huniq : c = canonicalCandidate := unique_valid_candidate c hc
 275  simpa [huniq] using canonical_r1_matches_res_nu1
 276
 277end NeutrinoBaselineChoiceSet
 278end Verification
 279end IndisputableMonolith
 280