IndisputableMonolith.Physics.PMNSCorrections

declarations in this module (24)

• def cube_vertices L63
• def cube_edges_count L66
• def cube_faces L69
• theorem cube3_vertices L77
• theorem cube3_edges L78
• theorem cube3_faces L79
• def atmospheric_coefficient L89
• theorem atmospheric_coefficient_eq_6 L91
• def atmospheric_correction L94
• theorem atmospheric_correction_eq L96
• def solar_coefficient L107
• theorem solar_coefficient_eq_10 L109
• def solar_correction L112
• theorem solar_correction_eq L114
• def cabibbo_coefficient L126
• theorem cabibbo_coefficient_eq_3_2 L128
• theorem cabibbo_coefficient_from_geometry L130
• def cabibbo_correction L136
• theorem cabibbo_correction_eq L138
• theorem atmospheric_matches L145
• theorem solar_matches L151
• theorem cabibbo_matches L157
• structure CorrectionDerivationCert L169
• theorem correction_derivation_verified L177