helium_fraction_calculated
plain-language theorem explainer
The helium-4 mass fraction equals one quarter when the neutron-to-proton ratio is fixed at 1/7 and every neutron is incorporated into a helium-4 nucleus. Cosmologists working inside Recognition Science cite this identity when converting the eight-tick octave into a concrete BBN yield. The proof is a single norm_num evaluation that confirms the arithmetic reduction 2*(1/7)/(1+1/7) simplifies directly to 1/4.
Claim. If the neutron-to-proton ratio satisfies $n/p = 1/7$ and all neutrons are incorporated into $^4$He nuclei, the helium-4 mass fraction is $Y_p = 2n/(n+p) = 2(1/7)/(1 + 1/7) = 1/4$.
background
Recognition Science derives BBN abundances from the phi-ladder and the eight-tick octave (T7). The neutron-to-proton ratio 1/7 is taken as an input fixed by that octave structure; the module then computes light-element yields under the assumption that all neutrons end in helium-4. The shifted cost function H(x) = J(x) + 1 appears in the surrounding algebra but is not invoked in this particular arithmetic step.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to the real-number expression 2*(1/7 : ℝ)/(1 + 1/7) and obtains the equality 1/4 by direct normalization.
why it matters
This theorem supplies the baseline helium fraction Y_p = 1/4 inside the Cosmology.Nucleosynthesis module and matches the observed 24-25 % mass fraction. It closes the direct calculation step that follows from the phi-forced parameters in PhiForcing and precedes the eta-dependent abundance curves (abundanceVsEta) and lithium predictions. The result instantiates the RS claim that nuclear magic numbers and reaction branching follow from the eight-tick octave (T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.