omegaCDM_band
plain-language theorem explainer
The theorem establishes that the RS-derived cold dark matter density parameter satisfies 0.25 < omegaCDM < 0.27. Cosmologists working inside the Recognition Science framework cite this interval when anchoring the five canonical dark-matter candidates to the observed density. The proof is a one-line wrapper that unfolds the constant definition and discharges the numerical inequalities via norm_num.
Claim. $0.25 < 0.26 < 0.27$ where the middle value is the constant definition of the cold dark matter density parameter.
background
The module treats the cold dark matter density parameter at A6/S3 depth inside Recognition Science cosmology. It enumerates five canonical candidates (WIMP, axion, sterile neutrino, primordial black hole, self-interacting DM) that correspond to configDim D = 5. The upstream definition supplies the constant value 0.26 that this theorem then bounds.
proof idea
The proof is a one-line wrapper. It unfolds the definition of omegaCDM to expose the literal 0.26, then applies refine to split the conjunction and norm_num to verify both strict inequalities.
why it matters
The result is consumed by cdmDensityCert, which packages the candidate count together with this density band to produce a certified object. It supplies the numerical anchor (0.25, 0.27) for Ω_CDM inside the RS cosmology module while the broader framework derives other constants from the forcing chain and Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.