heliumFraction_eq
plain-language theorem explainer
The helium-4 mass fraction in the Recognition Science model of primordial nucleosynthesis is fixed at exactly one quarter. Cosmologists working inside the RS framework cite this equality when assembling the certified light-element abundances for comparison with the observed range near 0.25. The proof is a single reflexivity step that follows immediately from the definition of the heliumFraction quantity.
Claim. The helium-4 mass fraction satisfies $Y_p = 1/4$.
background
In the Recognition Science treatment of primordial nucleosynthesis the helium-4 mass fraction is introduced as the rational constant one quarter in the leading approximation. The module states that this recovers the observed value near 0.25, which equals 1/(2φ²) times a small correction, while the Lean implementation adopts the exact value 1/4. The upstream definition supplies heliumFraction : ℚ := 1/4 and is the sole dependency of the present theorem.
proof idea
The proof is a term-mode reflexivity step. It applies rfl, which succeeds because the left-hand side is definitionally identical to the right-hand side by the body of the heliumFraction definition.
why it matters
This equality supplies the helium-4 fraction field inside the bbnCert structure that certifies the full set of primordial abundances. It occupies the first-approximation slot in the cosmology module, where the observed Y_p ≈ 0.25 is recovered exactly before higher-order phi-ladder corrections appear. The parent bbnCert assembles it with the five-nucleus count and the observed-range check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.