sin2_theta23_pred

formal source

 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.
 150    NOTE: Proof requires bounds on φ⁻⁸ which are in Numerics.Interval.PhiBounds. -/
 151theorem pmns_theta13_match :
 152    abs (sin2_theta13_pred - 0.022) < 0.002 := by
 153  -- External verification: φ⁻⁸ ≈ 0.02129, |0.02129 - 0.022| ≈ 0.0007 < 0.002 ✓
 154  unfold sin2_theta13_pred reactor_weight
 155  -- Bound φ^(-8) via reciprocal bounds on φ^8 from PhiBounds.
 156  have h8_gt : (46.97 : ℝ) < phi ^ (8 : ℕ) := by
 157    simpa [phi, Real.goldenRatio] using (IndisputableMonolith.Numerics.phi_pow8_gt)
 158  have h8_lt : phi ^ (8 : ℕ) < (46.99 : ℝ) := by