IndisputableMonolith.StandardModel.NeutrinoMassHierarchy

declarations in this module (38)

• def deltam21_sq L15
• def deltam31_sq L16
• def sum_mass_bound L17
• def seesawMass L21
• def typicalDiracMass L22
• def typicalMajoranaMass L23
• theorem seesaw_gives_small_mass L25
• def phiPredictedMR L32
• lemma phi_pow13 L35
• theorem seesaw_scale_phi_connection L50
• def massRatio L78
• lemma phi_pow7 L80
• theorem mass_ratio_phi7 L89
• def m2_estimate L111
• def m3_estimate L112
• def m3_m2_ratio L113
• lemma phi_pow4 L115
• theorem mass_ratio_phi4 L121
• inductive MassOrdering L157
• def rsPrediction L162
• structure NuRungAssignments L179
• def canonicalNuRungs L191
• def nuYardstick L203
• def nuMassAtRung L205
• def m_nu1_pred L209
• def m_nu2_pred L211
• def m_nu3_pred L213
• theorem nu_rung_gap_ratio L216
• theorem nu_solar_rung_ratio L226
• lemma zpow_neg_lt_one L236
• theorem nu_sum_bound_consistent L246
• theorem nu1_abs_mass_upper L283
• theorem nu2_abs_mass_pos L290
• theorem nu2_abs_mass_upper L295
• theorem nu2_abs_mass_interval L302
• theorem nu3_abs_mass_positive L307
• structure NuAbsMassCert L312
• def nuAbsMassCert L321