dmCandidate_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute the numerical value of Ω_CDM.
- Does not establish the observational band (0.25, 0.27).
- Does not derive the five candidates from the forcing chain T0-T8.
- Does not address stability or detection prospects for each candidate.
Lean usage
example : cdmDensityCert.five_candidates = 5 := dmCandidate_countformal statement (Lean)
25theorem dmCandidate_count : Fintype.card DMCandidate = 5 := by decide
proof body
26