cdmDensityCert
plain-language theorem explainer
This definition constructs the cold dark matter density certificate by supplying the two fields of the CDMDensityCert structure from upstream results. Cosmologists working in the Recognition Science framework cite it to record that exactly five dark matter candidate types are recognized and that the density parameter lies in the interval (0.25, 0.27). The construction is a direct record literal that references an enumeration theorem and a numerical bound theorem.
Claim. The cold dark matter density certificate is the structure asserting that the cardinality of the dark matter candidate type equals 5 and that the density parameter satisfies $0.25 < Ω_{CDM} < 0.27$.
background
The module treats the cold dark matter density parameter Ω_CDM within Recognition Science cosmology at A6/S3 depth. It recognizes five canonical dark matter candidates (WIMP, axion, sterile neutrino, primordial black hole, self-interacting DM) and states that Ω_CDM lies near 0.26 inside the band (0.25, 0.27). The supporting structure CDMDensityCert requires exactly these two properties: the candidate count and the numerical band on omegaCDM.
proof idea
The definition constructs the CDMDensityCert record by assigning the five_candidates field directly to the theorem dmCandidate_count and the omega_band field directly to the theorem omegaCDM_band.
why it matters
This definition supplies the terminal certificate for Ω_CDM in the RS cosmology module, confirming consistency with the observed value near 0.26. It completes the A6/S3 depth section by recording the five-candidate count and the density band. No downstream results depend on it yet, leaving open its use in larger derivations such as the total matter density parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.