nu_phase_offset

formal source

 135/-! ### Canonical fractional rungs (quarter resolution) -/
 136
 137/-- Neutrino phase offset: \(-2/8\) of an octave = \(-1/4\) rung. -/
 138def nu_phase_offset : Rung := (-(2 : ℚ)) / 8
 139
 140/-- Neutrino spacing for the solar-to-atmospheric gap: \((8-1)/2 = 7/2\) rungs. -/
 141def nu_spacing : Rung := ((8 : ℚ) - 1) / 2
 142
 143lemma nu_phase_offset_eq : nu_phase_offset = (-1 : ℚ) / 4 := by
 144  unfold nu_phase_offset
 145  norm_num
 146
 147lemma nu_spacing_eq : nu_spacing = (7 : ℚ) / 2 := by
 148  unfold nu_spacing
 149  norm_num
 150
 151/-- Upgraded atmospheric rung: integer base (-54) plus the fixed quarter offset (-1/4). -/
 152def res_nu3 : Rung := ofInt rung_nu3 + nu_phase_offset
 153
 154/-- Upgraded solar rung: enforce \(r_3-r_2 = 7/2\) (→ φ⁷ in squared-mass ratio). -/
 155def res_nu2 : Rung := res_nu3 - nu_spacing
 156
 157/-- Canonical lightest rung spacing: one quarter of the 8‑tick cycle (8/4 = 2 rungs). -/
 158def nu1_spacing : Rung := (8 : ℚ) / 4
 159
 160lemma nu1_spacing_eq : nu1_spacing = (2 : ℚ) := by
 161  unfold nu1_spacing
 162  norm_num
 163
 164/-- Upgraded lightest rung: place ν1 two rungs below ν2 (parameter-free 8‑tick quarter). -/
 165def res_nu1 : Rung := res_nu2 - nu1_spacing
 166
 167lemma res_nu3_simp : res_nu3 = (-217 : ℚ) / 4 := by
 168  unfold res_nu3