theorem
proved
tactic proof
pmns_theta12_match
show as:
view Lean formalization →
formal statement (Lean)
191theorem pmns_theta12_match :
192 abs (sin2_theta12_pred - 0.307) < 0.01 := by
proof body
Tactic-mode proof.
193 -- External verification: φ⁻² - 10*α ≈ 0.3819 - 0.073 = 0.3089
194 -- |0.3089 - 0.307| ≈ 0.002 < 0.01 ✓
195 unfold sin2_theta12_pred solar_weight solar_radiative_correction
196 -- Bound φ^(-2) and α, then bound the difference.
197 have hφ2_lo : (0.3818 : ℝ) < phi ^ (-2 : ℤ) := by
198 simpa [phi, Real.goldenRatio] using (IndisputableMonolith.Numerics.phi_neg2_gt)
199 have hφ2_hi : phi ^ (-2 : ℤ) < (0.382 : ℝ) := by
200 simpa [phi, Real.goldenRatio] using (IndisputableMonolith.Numerics.phi_neg2_lt)
201 have hα_lo := CKMGeometry.alpha_lower_bound
202 have hα_hi := CKMGeometry.alpha_upper_bound
203 -- Convert to a numeric envelope for φ^(-2) - 10α.
204 have h_lo : (0.3818 : ℝ) - 10 * (0.00731 : ℝ) < phi ^ (-2 : ℤ) - 10 * Constants.alpha := by
205 linarith
206 have h_hi : phi ^ (-2 : ℤ) - 10 * Constants.alpha < (0.382 : ℝ) - 10 * (0.00729 : ℝ) := by
207 linarith
208 -- Now show this interval sits within (0.297, 0.317), i.e. abs difference < 0.01.
209 rw [abs_lt]
210 constructor
211 · -- -0.01 < (pred - 0.307)
212 have : (0.297 : ℝ) < phi ^ (-2 : ℤ) - 10 * Constants.alpha := by
213 have hnum : (0.297 : ℝ) < (0.3818 : ℝ) - 10 * (0.00731 : ℝ) := by norm_num
214 exact lt_trans hnum h_lo
215 linarith
216 · -- (pred - 0.307) < 0.01
217 have : phi ^ (-2 : ℤ) - 10 * Constants.alpha < (0.317 : ℝ) := by
218 have hnum : (0.382 : ℝ) - 10 * (0.00729 : ℝ) < (0.317 : ℝ) := by norm_num
219 exact lt_trans h_hi hnum
220 linarith
221
222/-- Solar radiative correction coefficient (10) is forced by cube topology. -/