IndisputableMonolith.StandardModel.RelativisticDOF

declarations in this module (46)

• def adjoint_dim L110
• theorem su3_adjoint L112
• theorem su2_adjoint L113
• def gluon_dof L116
• theorem gluon_dof_eq L118
• def weak_boson_dof_symmetric L124
• theorem weak_boson_dof_symmetric_eq L126
• def higgs_dof L129
• def bosonic_dof L132
• theorem bosonic_dof_eq L134
• def quark_flavors_per_gen L139
• def n_colors L142
• theorem n_colors_eq L144
• def chiralities L147
• def particle_antiparticle L150
• def quark_dof_per_gen L154
• theorem quark_dof_per_gen_eq L157
• def charged_lepton_dof_per_gen L161
• theorem charged_lepton_dof_per_gen_eq L163
• def neutrino_dof_per_gen L168
• theorem neutrino_dof_per_gen_eq L170
• def fermion_dof_per_gen L173
• theorem fermion_dof_per_gen_eq L176
• def n_generations L179
• theorem n_generations_eq L181
• def fermionic_dof L184
• theorem fermionic_dof_eq L186
• def fermi_dirac_weight L201
• theorem fermi_dirac_weight_pos L203
• def g_star_derived L224
• theorem g_star_derived_eq L227
• theorem g_star_derived_pos L232
• theorem g_star_matches_cosmology L237
• theorem bosonic_traces_to_Q3 L245
• theorem fermionic_traces_to_Q3 L252
• def neutrino_dof_per_gen_dirac L273
• theorem neutrino_dof_per_gen_dirac_eq L275
• def fermion_dof_per_gen_dirac L279
• theorem fermion_dof_per_gen_dirac_eq L282
• def fermionic_dof_dirac L286
• theorem fermionic_dof_dirac_eq L288
• def g_star_dirac L293
• theorem g_star_dirac_eq L297
• theorem g_star_branch_gap L304
• structure GStarCert L312
• def gStarCert L322