IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity

declarations in this module (29)

• lemma E_passive_exact L51
• lemma cube_faces_exact L56
• lemma W_exact L61
• lemma pi_gt_d6_local L66
• lemma pi_lt_d6_local L69
• lemma inv_4pi_lower L72
• lemma inv_4pi_upper L84
• lemma inv_4pi_bounds L95
• lemma step_e_mu_bounds L100
• lemma step_mu_tau_bounds L109
• lemma predicted_residue_mu_bounds L122
• lemma predicted_residue_tau_bounds L132
• theorem phi_pow_neg963_lower L151
• theorem phi_pow_neg962_upper L157
• theorem phi_pow_residue_mu_lower L162
• theorem phi_pow_residue_mu_upper L175
• lemma phi_pow_residue_mu_bounds L186
• theorem phi_pow_neg377_lower L196
• theorem phi_pow_neg375_upper L202
• theorem phi_pow_residue_tau_lower L207
• theorem phi_pow_residue_tau_upper L217
• lemma phi_pow_residue_tau_bounds L228
• theorem predicted_mass_mu_lower L239
• theorem predicted_mass_mu_upper L246
• theorem muon_mass_pred_bounds_proven L257
• theorem predicted_mass_tau_lower L268
• theorem predicted_mass_tau_upper L275
• theorem tau_mass_pred_bounds_proven L286
• theorem lepton_ladder_forced_from_T9 L307