theorem
proved
solar_correction_geometric
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.MixingDerivation on GitHub at line 223.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
220 linarith
221
222/-- Solar radiative correction coefficient (10) is forced by cube topology. -/
223theorem solar_correction_geometric :
224 solar_radiative_correction = PMNSCorrections.solar_correction := by
225 simpa using (PMNSCorrections.solar_matches).symm
226
227/-- **CERTIFICATE: Mixing Matrix Geometry**
228 Packages the proofs for CKM and PMNS mixing parameters. -/
229structure MixingCert where
230 vcb_ratio : V_cb_pred = edge_dual_ratio
231 vub_leakage : V_ub_pred = fine_structure_leakage
232 theta13_match : abs (sin2_theta13_pred - 0.022) < 0.002
233 theta12_match : abs (sin2_theta12_pred - 0.307) < 0.01
234 theta23_match : abs (sin2_theta23_pred - 0.546) < 0.01
235
236theorem mixing_verified : MixingCert where
237 vcb_ratio := vcb_derived
238 vub_leakage := vub_derived
239 theta13_match := pmns_theta13_match
240 theta12_match := pmns_theta12_match
241 theta23_match := pmns_theta23_match
242
243/-- **THEOREM: PMNS Mixing Angle Relation**
244 The predicted mixing angles satisfy the Born rule probability ratios
245 between the generations (with radiative corrections). -/
246theorem pmns_theta12_born_forced :
247 sin2_theta12_pred = solar_weight - solar_radiative_correction := by
248 unfold sin2_theta12_pred
249 rfl
250
251theorem pmns_theta23_born_forced :
252 sin2_theta23_pred = atmospheric_weight + atmospheric_radiative_correction := by
253 unfold sin2_theta23_pred