module module

`IndisputableMonolith.Cosmology.Nucleosynthesis`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.PhiForcing module_import

declarations in this module (18)

def helium4_mass_fraction L48
def deuterium_ratio L51
def helium3_ratio L54
def lithium7_ratio L57
def eta L60
def bbnReactions L75
def neutron_proton_ratio L96
theorem helium_fraction_calculated L109
def abundanceVsEta L122
def lithium_predicted L144
def lithium_observed L145
theorem lithium_problem L147
theorem rs_lithium_insight L162
def neutrino_species_from_bbn L177
theorem three_neutrinos_confirmed L179
theorem eta_phi_connection L192
def summary L207
structure NucleosynthesisFalsifier L221