`correction_derivation_verified`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.PMNSCorrections
domain: Physics
line: 177 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.PMNSCorrections on GitHub at line 177.

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

 174                       solar_coefficient = 10 ∧
 175                       cabibbo_coefficient = 3/2
 176
 177theorem correction_derivation_verified : CorrectionDerivationCert where
 178  atmospheric_from_faces := rfl
 179  solar_from_edges_minus_2 := rfl
 180  cabibbo_from_faces_over_4 := cabibbo_coefficient_from_geometry
 181  coefficients_match := by
 182    constructor
 183    · exact atmospheric_coefficient_eq_6
 184    constructor
 185    · exact solar_coefficient_eq_10
 186    · exact cabibbo_coefficient_eq_3_2
 187
 188end PMNSCorrections
 189end Physics
 190end IndisputableMonolith

papers checked against this theorem

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