bbnCert
plain-language theorem explainer
Recognition Science cosmology supplies a certificate that Big Bang nucleosynthesis produces exactly five primordial nuclei with helium-4 mass fraction exactly one quarter inside the observed interval 0.24 to 0.26. Cosmologists tracing light-element yields to the phi-derived baryon-photon ratio would cite this to confirm the first-approximation match with data. The definition is a direct record construction that inserts three upstream results into the structure fields.
Claim. Let BBNCert be the structure whose fields require that the set of primordial nuclei has cardinality 5, the helium-4 mass fraction equals exactly 1/4, and 0.24 < helium-4 mass fraction < 0.26. The certificate term is the explicit witness obtained by substituting the enumerated nuclei count, the reflexivity equality for the fraction, and the numerical bounds theorem.
background
The module treats Big Bang nucleosynthesis as the production of H, D, He-3, He-4 and Li-7 under RS rules, with abundances fixed by the baryon-photon ratio eta_B approximately phi to the minus 44 and the neutron-proton ratio at freeze-out. Five canonical nuclei are identified with configDim D equals 5. The helium-4 mass fraction is stated as 1/4 in the first approximation, noted to lie near the observed 0.247-0.252 band after small corrections.
proof idea
The definition is a one-line record construction. It assigns the nuclei cardinality field from the decidable enumeration theorem, the fraction field from the reflexivity theorem heliumFraction_eq, and the observation interval field from the numerical normalization theorem heliumFraction_in_observed.
why it matters
The certificate closes the BBN section of the RS cosmology module by exhibiting a concrete witness to the predicted light-element abundances. It supports the broader claim that RS recovers the observed helium fraction from the phi ladder without extra parameters, consistent with the eight-tick octave and D equals 3 spatial dimensions in the forcing chain. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.