IndisputableMonolith.StandardModel.CKMFromCube

declarations in this module (22)

• def torsionGap L81
• theorem gap_12 L83
• theorem gap_13 L84
• theorem gap_23 L85
• theorem torsionGap_hierarchy L89
• def suppressionExponent L102
• theorem suppression_12 L106
• theorem suppression_23 L107
• theorem suppression_13 L108
• def flipWeight L118
• theorem flipWeight_sum L122
• theorem flipWeight_values L131
• def unnormalizedAmplSq L154
• def wolfenstein_lambda_structural L183
• theorem lambda_structural_bounds L187
• def wolfenstein_A_structural L208
• theorem A_structural_value L212
• theorem ckm_hierarchy_qualitative L223
• theorem ckm_dimension L229
• theorem ratio_Vus_Vcb_structural L236
• structure CKMStructureCert L243
• def ckmStructureCert L254