dmCandidate_count
plain-language theorem explainer
The declaration asserts that the Recognition Science cosmology module enumerates exactly five dark matter candidates. Researchers deriving the cold dark matter density parameter Ω_CDM from the RS framework would reference this count to fix the multiplicity in the density calculation. The proof reduces to a single decision tactic that verifies the cardinality of the inductive enumeration.
Claim. The finite set of dark matter candidates has cardinality 5, where the candidates are the WIMP, axion, sterile neutrino, primordial black hole, and self-interacting dark matter.
background
In the Recognition Science cosmology module, the cold dark matter density parameter Ω_CDM is derived from a fixed set of five canonical candidates. The inductive type DMCandidate enumerates these as wimp, axion, sterileNeutrino, primordialBH, and selfInteracting, each deriving Fintype to enable cardinality computation. This setup supports the claim that Ω_CDM lies in the band (0.25, 0.27) with the central value approximately 0.26.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the equality Fintype.card DMCandidate = 5. The tactic succeeds because the inductive type has exactly five constructors and derives the necessary decidable instances.
why it matters
This count is used directly in the definition of cdmDensityCert to populate the five_candidates field, which in turn supports the certification of the CDM density parameter. It fills the A6/S3 depth in the RS cosmology by fixing the multiplicity of dark matter candidates at five, consistent with the framework's enumeration of configDim D = 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.