heliumFraction_in_observed
plain-language theorem explainer
The declaration confirms that the helium-4 mass fraction computed in the Recognition Science model of primordial nucleosynthesis lies strictly between 0.24 and 0.26. Cosmologists working inside the RS framework cite the result to verify consistency between the leading-order abundance and the observed BBN band. The proof is a one-line wrapper that unfolds the definition of heliumFraction and applies numerical normalization to the resulting inequalities.
Claim. The helium-4 mass fraction satisfies $0.24 < Y_p < 0.26$, where $Y_p = 1/4$.
background
The module models Big Bang nucleosynthesis inside Recognition Science, deriving light-element abundances from the baryon-photon ratio η_B ≈ φ^{-44} and the neutron-to-proton ratio at freeze-out. Five canonical primordial nuclei (p, n, D, He-3, He-4) are identified with configDim D = 5, and the helium-4 mass fraction is fixed at Y_p ≈ 0.25 in the leading approximation. The upstream definition heliumFraction supplies the exact rational value 1/4 used by the present theorem.
proof idea
The proof is a one-line wrapper. It unfolds heliumFraction to obtain the literal value 1/4, splits the conjunction with constructor, and discharges both inequalities with norm_num.
why it matters
The theorem populates the he4_in_observed field of the downstream BBN certificate bbnCert. It thereby closes the observational check on the RS prediction that Y_p ≈ 0.25 matches the measured band, supporting the claim that abundances follow from the phi-ladder without extra parameters. The module notes that 1/4 approximates the corrected value 1/(4 × 1.012) ≈ 0.247 while remaining inside the wider interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.