omegaCDM
plain-language theorem explainer
The declaration fixes the cold dark matter density parameter at 0.26. Cosmologists working inside the Recognition Science framework cite this value when matching the five-candidate count (configDim D = 5) to observed densities. It is introduced by direct numerical assignment with no computation or lemmas.
Claim. The cold dark matter density parameter is defined by the assignment $0.26$.
background
The module treats five canonical dark-matter candidates (WIMP, axion, sterile neutrino, primordial black hole, self-interacting DM) as the objects counted by configDim D = 5. It places the cold dark matter density parameter inside the interval (0.25, 0.27) while remaining inside RS-native units where c = 1 and the phi-ladder supplies the mass scale. The module doc states that Lean status is zero sorry and zero axiom.
proof idea
This is a direct definition that assigns the constant 0.26 to the real number omegaCDM. No lemmas or tactics are invoked; the body is a single literal.
why it matters
The definition supplies the numerical anchor required by the downstream CDMDensityCert structure (five candidates and the band condition) and by the theorem omegaCDM_band that verifies the open interval. It therefore closes the cosmology section to the RS claim that exactly five candidates arise when configDim equals 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.