IndisputableMonolith.Cosmology.MatterAntimatter

declarations in this module (25)

• def eta_observed L46
• def eta_B L49
• theorem eta_is_small L52
• def matterAntimatterRatio L58
• inductive SakharovCondition L66
• def allConditionsNeeded L73
• theorem sakharov_necessary L81
• def cpTransformTick L94
• theorem cp_not_symmetry L99
• def epsilon_CP L107
• def dilutionFactor L111
• theorem eta_from_epsilon L114
• theorem eta_from_phi L126
• def eta_phi_prediction L142
• lemma phi_sq L147
• lemma phi_pow_fib_succ L160
• lemma phi_pow_44_gt_1pt5e9 L185
• lemma phi_pow_44_lt_1pt6e9 L202
• theorem phi_power_matches_eta L227
• def baryogenesisMechanisms L259
• theorem rs_baryogenesis L272
• def predictions L283
• def eta_exponent L294
• structure EtaFalsifier L303
• def experimentalStatus L310