PrimordialNucleus
plain-language theorem explainer
PrimordialNucleus enumerates the five light nuclei produced during Big Bang nucleosynthesis in the Recognition Science setting. Cosmologists working with RS cosmology cite the enumeration to fix configDim D = 5 when computing the helium mass fraction and baryon-photon ratio. The declaration is a direct inductive type with five constructors that automatically derives decidable equality and Fintype structure.
Claim. The finite set of primordial nuclei is defined as the inductive type consisting of the five elements proton, neutron, deuterium, $^3$He and $^4$He.
background
Recognition Science models Big Bang nucleosynthesis through the baryon-to-photon ratio η_B ≈ φ^{-44} together with the neutron-to-proton ratio at freeze-out. The module states that five canonical primordial nuclei (proton, neutron, deuterium, He-3, He-4) realize configDim D = 5, with the He-4 mass fraction Y_p approximated as 1/4 in the leading RS calculation. The local theoretical setting is the A3 cosmology section, which links these nuclei directly to observed abundances without invoking external nuclear reaction networks.
proof idea
The declaration is a direct inductive definition that introduces five constructors and derives the required type-class instances (DecidableEq, Repr, BEq, Fintype) by structural recursion. No lemmas are applied; the finite cardinality follows immediately from the constructor list.
why it matters
This definition supplies the finite set whose cardinality is certified as five inside BBNCert, which also records the helium fraction equality heliumFraction = 1/4 and the observational interval (0.24, 0.26). It anchors the configDim D = 5 slot required by the RS forcing chain for light-element predictions. The parent structure BBNCert uses the enumeration to connect the phi-ladder constants to the observed helium abundance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.