lithium_observed
plain-language theorem explainer
The observed lithium-7 to hydrogen abundance ratio is set to 1.6 times 10 to the minus 10. Researchers comparing Big Bang nucleosynthesis predictions to astronomical data would cite this value when addressing the lithium problem. The definition consists of a direct numerical assignment with no lemmas or reductions applied.
Claim. The observed lithium-7 to hydrogen ratio equals $1.6 × 10^{-10}$.
background
The Cosmology.Nucleosynthesis module derives light element abundances from RS principles during the first minutes after the Big Bang. Abundances of deuterium, helium-3, helium-4, and lithium-7 depend on the baryon-to-photon ratio eta together with nuclear reaction rates constrained by the eight-tick structure. The module documentation lists the observed lithium-7 abundance as approximately 1.6 times 10 to the minus 10 and flags it as the lithium problem.
proof idea
This is a definition that directly assigns the real number 1.6e-10. No lemmas are applied and no tactics are used; it functions as a constant assignment for later comparisons.
why it matters
The value anchors the lithium problem discussion in the BBN module and supplies the empirical benchmark for comparison with lithium_predicted. It connects to the RS mechanism in which eta is derived from phi and nuclear magic numbers follow from the eight-tick octave. The module documentation presents this constant as part of the target to resolve the noted discrepancy through RS-constrained parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.