IndisputableMonolith.Physics.MixingDerivation

declarations in this module (25)

• theorem vus_derived L37
• theorem cabibbo_correction_geometric L43
• theorem vcb_derived L56
• theorem vub_derived L68
• theorem vcb_geometric_origin L78
• def pmns_weight L93
• theorem pmns_weight_eq_phi_pow L96
• def pmns_prob L119
• def sin2_theta12_pred L127
• def sin2_theta23_pred L128
• def sin2_theta13_pred L129
• theorem pmns_theta23_match L133
• theorem atmospheric_correction_geometric L144
• theorem pmns_theta13_match L151
• theorem pmns_theta12_match L191
• theorem solar_correction_geometric L223
• structure MixingCert L229
• theorem mixing_verified L236
• theorem pmns_theta12_born_forced L246
• theorem pmns_theta23_born_forced L251
• theorem pmns_theta13_born_forced L256
• def ckm_cp_phase L269
• def jarlskog_pred L277
• theorem jarlskog_match L284
• theorem jarlskog_pos L331