helium3_ratio
plain-language theorem explainer
The declaration assigns the helium-3 to hydrogen ratio the fixed value 1.0 times 10 to the minus 5. Cosmologists working on Big Bang nucleosynthesis within Recognition Science would reference this constant when comparing model outputs to observed light-element abundances. It is introduced as a direct numerical definition with no lemmas or reductions.
Claim. The helium-3 to hydrogen ratio is defined as $1.0 × 10^{-5}$.
background
The Cosmology.Nucleosynthesis module derives light-element abundances under Recognition Science for the first few minutes after the Big Bang. It incorporates the baryon-to-photon ratio eta derived from phi, nuclear reaction rates tied to the eight-tick structure, and observed values including helium-3 to hydrogen near 10^{-5}. The module documentation states that abundances for deuterium, helium-3, helium-4, and lithium-7 follow from RS-constrained parameters.
proof idea
The definition is a direct constant assignment of 1.0e-5 with no lemmas applied and no tactic steps.
why it matters
This supplies the helium-3 input for abundance calculations such as abundanceVsEta in the same module. It supports the COS-012 target of reproducing observed BBN yields from phi-forced eta and the eight-tick octave. The module flags the lithium problem as an open discrepancy not addressed by this constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.