IndisputableMonolith.Cosmology.BaryonAsymmetryExact

declarations in this module (23)

• def eta_B_rung L70
• def saturation_exponent L73
• def flip_count_gen0 L77
• def torsion_gap_01 L81
• theorem rung_44_is_product L89
• theorem rung_matches_alpha_seed_nat L99
• theorem eta_B_rung_eq L104
• theorem phi_neg44_times_phi45_eq_phi L112
• theorem phi_neg44_times_phi45_eq_phi' L118
• theorem rung_sum L123
• theorem rung_sum_named L126
• def eta_B_phi_scale L132
• theorem eta_B_phi_scale_pos L135
• theorem eta_B_phi_scale_lt_one L141
• def phi45_scale L150
• theorem phi45_scale_gt_one L153
• theorem eta_B_phi45_balance L174
• theorem eta_B_eq_phi_over_phi45_scale L180
• theorem full_derivation_chain L199
• def eta_B_observed_central L228
• def discrepancy_percent L233
• structure BaryonAsymmetryExactCert L244
• theorem baryon_asymmetry_exact_cert L271