DMCandidate
The enumeration of dark matter candidates in the Recognition Science cosmology model lists five standard types. Cosmologists deriving the cold dark matter density parameter reference this list to confirm the candidate count. The construction is a direct inductive definition that automatically equips the type with finite cardinality and decidable equality.
claimDefine the finite set of dark matter candidates to consist of the WIMP, the axion, the sterile neutrino, the primordial black hole, and self-interacting dark matter.
background
In the Recognition Science framework applied to cosmology, the cold dark matter density parameter is derived from a fixed number of candidate types. The module posits exactly five canonical candidates corresponding to configuration dimension five and supports the observed value Ω_CDM ≈ 0.26 lying in the interval (0.25, 0.27). The inductive definition supplies the underlying type whose cardinality is later certified by a separate theorem.
proof idea
As a pure definition, the inductive type is introduced by enumerating the five constructors. The derived instances for decidable equality and finite type follow immediately from the finite enumeration without requiring explicit lemmas or tactics.
why it matters in Recognition Science
The definition feeds directly into the CDMDensityCert structure, which requires the cardinality to be five and places omegaCDM in the observational band. It realizes the A6/S3 depth of the cosmology module within Recognition Science, where the candidate count contributes to the density parameter. The framework links this to the overall forcing chain but leaves the explicit mass formulas to other components.
scope and limits
- Does not derive the value of the density parameter.
- Does not model interactions or masses of the candidates.
- Does not reference the J-function or phi-ladder from the core theory.
- Does not constrain the spatial dimension to three.
formal statement (Lean)
17inductive DMCandidate where
18 | wimp
19 | axion
20 | sterileNeutrino
21 | primordialBH
22 | selfInteracting
23 deriving DecidableEq, Repr, BEq, Fintype
24