pmns_prob

formal source

 116/-- **THEOREM: PMNS Probabilities from Born Rule**
 117    The mixing probability P_ij is the normalized path weight for a transition
 118    between rungs. -/
 119noncomputable def pmns_prob (dτ : ℤ) (total_weight : ℝ) : ℝ :=
 120  pmns_weight dτ / total_weight
 121
 122/-- **CONJECTURE: PMNS angles from Rung Ratios**
 123    The neutrino mixing angles are forced by the rung differences.
 124    - θ₁₂: Solar angle, sin²θ₁₂ ≈ solar_weight - solar_radiative_correction.
 125    - θ₂₃: Atmospheric angle, sin²θ₂₃ ≈ atmospheric_weight + atmospheric_radiative_correction.
 126    - θ₁₃: Reactor angle, sin²θ₁₃ ≈ reactor_weight. -/
 127noncomputable def sin2_theta12_pred : ℝ := solar_weight - solar_radiative_correction
 128noncomputable def sin2_theta23_pred : ℝ := atmospheric_weight + atmospheric_radiative_correction
 129noncomputable def sin2_theta13_pred : ℝ := reactor_weight
 130
 131/-- **THEOREM: PMNS Atmospheric Angle Match**
 132    The atmospheric angle sin²θ₂₃ matches observation (0.546) within 1%. -/
 133theorem pmns_theta23_match :
 134    abs (sin2_theta23_pred - 0.546) < 0.01 := by
 135  unfold sin2_theta23_pred atmospheric_weight atmospheric_radiative_correction
 136  -- 0.5 + 6*alpha ≈ 0.5 + 0.0438 = 0.5438. PDG 2022: 0.546(21)
 137  -- Use alpha bounds
 138  have h_alpha_lo := CKMGeometry.alpha_lower_bound
 139  have h_alpha_hi := CKMGeometry.alpha_upper_bound
 140  rw [abs_lt]
 141  constructor <;> linarith
 142
 143/-- Atmospheric radiative correction coefficient (6) is forced by cube topology. -/
 144theorem atmospheric_correction_geometric :
 145    atmospheric_radiative_correction = PMNSCorrections.atmospheric_correction := by
 146  simpa using (PMNSCorrections.atmospheric_matches).symm
 147
 148/-- **THEOREM: PMNS Reactor Angle Match**
 149    The reactor angle sin²θ₁₃ matches observation (0.022) within reasonable range.