pith. machine review for the scientific record. sign in
theorem proved tactic proof

correction_derivation_verified

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 177theorem correction_derivation_verified : CorrectionDerivationCert where
 178  atmospheric_from_faces := rfl

proof body

Tactic-mode proof.

 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

depends on (5)

Lean names referenced from this declaration's body.