BBNCert
plain-language theorem explainer
BBNCert packages three facts for the Recognition Science BBN model: the inductive type PrimordialNucleus has exactly five elements, the helium-4 mass fraction equals 1/4, and this value lies inside the observed interval (0.24, 0.26). Cosmologists checking phi-ladder predictions against nuclear abundances would cite the certificate when confirming the five-nucleus count and the leading-order Y_p approximation. The declaration is introduced as a plain structure whose fields are filled directly from the sibling cardinality fact, the constant 1/4,
Claim. Let $BBNCert$ be the structure whose fields assert that the set of primordial nuclei has cardinality 5, the helium-4 mass fraction equals $1/4$, and $0.24 < 1/4 < 0.26$.
background
The module treats Big Bang Nucleosynthesis as determined by the baryon-to-photon ratio $η_B ≈ φ^{-44}$ together with the neutron-to-proton freeze-out ratio. It introduces the inductive type PrimordialNucleus whose five constructors are proton, neutron, deuterium, He3 and He4; the Fintype instance on this type therefore yields cardinality 5. The helium-4 mass fraction is defined as the constant 1/4, which the module presents as the leading-order RS prediction that approximates the observed value near 0.25.
proof idea
BBNCert is a structure definition whose three fields are populated directly: the cardinality equality follows from the Fintype derivation on PrimordialNucleus, the fraction equality is the upstream constant definition heliumFraction, and the numerical inequality is stated as a direct proposition on the rational 1/4.
why it matters
The structure supplies the certificate type instantiated by the downstream bbnCert construction that certifies consistency between RS abundances and observation. It occupies the A3 Cosmology slot by confirming the five-nucleus count and the 1/4 helium fraction that the module derives from the phi-ladder. The module notes that 1/4 approximates the more precise 0.247 value, leaving open the question of higher-order phi-ladder corrections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.