IndisputableMonolith.Physics.LeptonGenerations.Necessity

declarations in this module (110)

• theorem lepton_rungs_forced L59
• theorem lepton_residues_distinct L71
• def is_stable_lepton_ladder L89
• theorem lepton_rungs_unique L101
• structure LeptonTorsionCert L130
• theorem lepton_torsion_verified L138
• theorem torsion_minimality_forced L152
• lemma E_passive_exact L165
• lemma cube_faces_exact L170
• lemma W_exact L175
• lemma pi_gt_d6_local L180
• lemma pi_lt_d6_local L183
• lemma inv_4pi_lower L186
• lemma inv_4pi_upper L198
• lemma inv_4pi_bounds L209
• lemma step_e_mu_bounds L214
• lemma step_mu_tau_bounds L223
• lemma gap_minus_shift_bounds_proven L236
• lemma predicted_residue_mu_bounds L244
• lemma predicted_residue_tau_bounds L257
• def phi_pow_neg963_lower_hypothesis L276
• def phi_pow_neg962_upper_hypothesis L280
• lemma exp_four_upper L285
• lemma exp_four_lower L296
• def exp_taylor_10_at_081416924 L309
• def exp_error_10_at_081416924 L313
• lemma exp_081416924_upper_q L317
• lemma exp_081416924_upper L321
• def exp_taylor_10_at_080454125 L343
• def exp_error_10_at_080454125 L347
• lemma exp_080454125_lower_q L351
• lemma exp_080454125_lower L355
• def exp_taylor_10_at_063407156 L380
• def exp_error_10_at_063407156 L384
• lemma exp_063407156_upper_q L388
• lemma exp_063407156_upper L392
• def exp_taylor_10_at_062924882 L414
• def exp_error_10_at_062924882 L418
• lemma exp_062924882_lower_q L422
• lemma exp_062924882_lower L426
• lemma exp_181416924_upper L451
• lemma exp_180454125_lower L464
• lemma exp_463407156_upper L477
• lemma exp_462924882_lower L490
• theorem phi_pow_neg963_lower_proved L503
• theorem phi_pow_neg962_upper_proved L529
• theorem phi_pow_residue_mu_lower L555
• theorem phi_pow_residue_mu_upper L570
• lemma phi_pow_residue_mu_bounds L583
• def phi_pow_neg377_lower_hypothesis L594
• def phi_pow_neg375_upper_hypothesis L598
• theorem phi_pow_neg377_lower_proved L601
• theorem phi_pow_neg375_upper_proved L627
• theorem phi_pow_residue_tau_lower L653
• theorem phi_pow_residue_tau_upper L665
• lemma phi_pow_residue_tau_bounds L678
• theorem predicted_mass_mu_lower L690
• theorem predicted_mass_mu_upper L698
• theorem muon_mass_pred_bounds_proven L710
• theorem predicted_mass_mu_lower_tight L716
• theorem predicted_mass_mu_upper_tight L725
• theorem muon_mass_pred_bounds_tight L735
• theorem predicted_mass_tau_lower L746
• theorem predicted_mass_tau_upper L754
• theorem tau_mass_pred_bounds_proven L766
• theorem predicted_mass_tau_lower_tight L772
• theorem predicted_mass_tau_upper_tight L781
• theorem tau_mass_pred_bounds_tight L791
• theorem lepton_ladder_forced_from_T9 L812
• lemma inv_4pi_lower_v2 L863
• lemma inv_4pi_upper_v2 L871
• lemma step_e_mu_bounds_v2 L879
• lemma step_mu_tau_bounds_v2 L886
• lemma predicted_residue_mu_bounds_v2 L891
• lemma predicted_residue_tau_bounds_v2 L898
• def exp_taylor_v2_1 L915
• def exp_error_v2_1 L918
• lemma exp_v2_1_q L921
• lemma exp_06327_upper L922
• def exp_taylor_v2_2 L944

… and 30 more