IndisputableMonolith.Verification.LeptonCoefficientPerturbation

declarations in this module (11)

• lemma alpha_abs_le_half L37
• theorem jcost_one_plus_alpha_expansion L44
• theorem two_jcost_one_plus_alpha_expansion L49
• theorem two_jcost_cubic_coeff_unique L64
• theorem exists_unique_two_jcost_channel_coeff L76
• lemma E_total_eq_twelve L84
• theorem edge_aggregated_two_jcost_one_plus_alpha L88
• theorem edge_cubic_channel_subleading L107
• theorem correction_order_3_eq_twelve_alpha_cube L126
• theorem radiative_correction_channel_decomposition L131
• theorem o4_perturbative_core_certificate L139