heliumFraction
plain-language theorem explainer
Helium-4 mass fraction set exactly to 1/4 as the leading approximation in Recognition Science Big Bang nucleosynthesis. Cosmologists using the RS baryon-photon ratio and neutron-proton freeze-out would cite this constant when checking consistency with observed abundances near 0.25. The entry is a direct constant assignment with no lemmas or computation.
Claim. The helium-4 mass fraction $Y_p$ equals $1/4$.
background
The module treats Big Bang nucleosynthesis as producing five canonical nuclei (protons, neutrons, deuterium, helium-3, helium-4) whose abundances follow from the RS baryon-photon ratio η_B ≈ φ^{-44} and the neutron-to-proton ratio at freeze-out. The helium-4 mass fraction is fixed at 1/4 in the first approximation, with the note that the observed value ≈0.247 lies close after a small correction factor. No upstream lemmas are required; the definition supplies a base constant for the local cosmology setting.
proof idea
Direct definition that assigns the rational constant 1/4 with no tactics or lemmas applied.
why it matters
Supplies the helium-4 fraction required by the BBNCert structure to certify five nuclei and place the value inside the observed interval (0.24, 0.26). It realizes the module's statement that Y_p ≈ 0.25 exactly in the initial RS approximation, linking the phi-ladder scaling to nuclear yields without further derivation. The placement closes the first-approximation step before any phi-ladder refinement of the fraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.