structure
definition
NucleosynthesisFalsifier
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.Nucleosynthesis on GitHub at line 221.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
218 1. η not φ-related
219 2. ⁴He abundance very different from 25%
220 3. BBN predictions don't match (except Li) -/
221structure NucleosynthesisFalsifier where
222 eta_not_phi : Prop
223 helium_wrong : Prop
224 bbn_fails : Prop
225 falsified : helium_wrong ∧ bbn_fails → False
226
227end Nucleosynthesis
228end Cosmology
229end IndisputableMonolith