IndisputableMonolith.Physics.NeutrinoSector

declarations in this module (53)

• def dm2_21_exp L57
• def dm2_32_exp L58
• def m2_approx L61
• def m3_approx L62
• def rung_nu3 L66
• def rung_nu2 L67
• structure MassDisplayCalibration L70
• def legacy_mass_display_calibration L75
• def mass_display_calibration_of_external L81
• def MeV_to_eV L91
• def predicted_mass_eV_with L94
• def predicted_mass_eV L99
• lemma predicted_mass_eV_legacy L102
• def nu_phase_offset L138
• def nu_spacing L141
• lemma nu_phase_offset_eq L143
• lemma nu_spacing_eq L147
• def res_nu3 L152
• def res_nu2 L155
• def nu1_spacing L158
• lemma nu1_spacing_eq L160
• def res_nu1 L165
• lemma res_nu3_simp L167
• lemma res_nu2_simp L173
• lemma res_nu1_simp L179
• theorem rung_gap_21_is_two L185
• def predicted_mass_eV_frac_with L190
• def predicted_mass_eV_frac L195
• lemma predicted_mass_eV_frac_legacy L198
• theorem rung_gap_is_seven_halves L205
• lemma nu3_frac_pred_bounds L224
• lemma nu2_frac_pred_bounds L256
• lemma nu1_frac_pred_bounds L284
• def dm2 L392
• def dm2_21_frac_pred L394
• def dm2_31_frac_pred L397
• def dm2_21_frac_pred_with L401
• def dm2_31_frac_pred_with L405
• lemma dm2_21_frac_pred_with_legacy L408
• lemma dm2_31_frac_pred_with_legacy L412
• lemma dm2_21_frac_pred_in_nufit_1sigma L417
• lemma dm2_21_frac_pred_with_legacy_in_nufit_1sigma L486
• lemma dm2_31_frac_pred_in_nufit_2sigma L492
• lemma dm2_31_frac_pred_with_legacy_in_nufit_2sigma L556
• theorem squared_mass_ratio_structural_phi7 L572
• lemma nu3_pred_bounds L623
• lemma m3_approx_bounds L651
• theorem nu3_match L674
• lemma nu2_pred_bounds L689
• lemma m2_approx_bounds L717
• theorem nu2_match L738
• structure NeutrinoMassCert L748
• theorem neutrino_mass_verified L752