CDMDensityCert
plain-language theorem explainer
A certificate structure asserts that exactly five dark matter candidates exist and that the cold dark matter density parameter satisfies 0.25 < Ω_CDM < 0.27. Cosmologists working in the Recognition Science framework cite this to fix the Ω_CDM value at 0.26 from configDim D = 5. The structure assembles the Fintype cardinality of the five-candidate enumeration directly with the explicit numerical band on the density constant.
Claim. A structure certifying that the cardinality of the set of dark matter candidates equals five and that the cold dark matter density parameter satisfies $0.25 < Ω_{CDM} < 0.27$.
background
The module derives the cold dark matter density parameter from Recognition Science at A6/S3 depth, with the local setting that five canonical candidates match configDim D = 5. The inductive enumeration lists WIMP, axion, sterile neutrino, primordial black hole, and self-interacting dark matter. The constant for the density parameter is fixed at the real number 0.26, and the band (0.25, 0.27) is supplied by the upstream result on that constant.
proof idea
The structure is introduced by direct field declarations with no separate proof body. It packages the Fintype.card equality for the candidate enumeration together with the inequality band on the density parameter.
why it matters
This structure supplies the certified inputs consumed by the downstream construction of the density certificate. It encodes the five-candidate requirement from configDim D = 5 in the T0-T8 forcing chain and the observed Ω_CDM band near 0.26. The module states zero sorrys or axioms, closing the scaffolding for this cosmological input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.