`solar_correction_geometric`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.MixingDerivation
domain: Physics
line: 223 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.MixingDerivation on GitHub at line 223.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.