primordialNucleusCount
plain-language theorem explainer
The theorem establishes that the finite type PrimordialNucleus has cardinality exactly five, enumerating proton, neutron, deuterium, helium-3, and helium-4. Cosmologists verifying Big Bang nucleosynthesis abundances against Recognition Science predictions cite this result to fix the configuration dimension for the light-element sector. The proof is a one-line decide tactic that evaluates the cardinality directly from the inductive definition equipped with Fintype.
Claim. The set of primordial nuclei has cardinality five: $|$proton, neutron, deuterium, ${}^3$He, ${}^4$He$| = 5$.
background
The module treats primordial nucleosynthesis in the RS A3 cosmology setting. Big Bang Nucleosynthesis produces H, D, He-4, He-3, and Li-7, yet the framework recognizes five canonical species whose count equals the configuration dimension D = 5. The inductive definition PrimordialNucleus lists proton, neutron, deuterium, He3, He4 and derives DecidableEq, Repr, BEq, Fintype, so the type is finite and its cardinality is computable by decision procedures. The upstream result is precisely this inductive definition, which supplies the Fintype instance used by the theorem.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the goal Fintype.card PrimordialNucleus = 5. The tactic succeeds because the inductive type has exactly five constructors and the derived Fintype instance allows exhaustive enumeration and cardinality computation at compile time.
why it matters
This theorem supplies the five_nuclei field of the BBN certificate bbnCert, which also records the helium-4 fraction results. It fills the enumeration step of the A3 cosmology block, fixing the number of primordial species to five before the mass-fraction calculation Y_p ≈ 1/4. The result is consistent with the RS claim that light-element abundances are controlled by the baryon-to-photon ratio η_B ≈ φ^{-44} and the eight-tick structure of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.