omegaCDM
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive 0.26 from the J-cost equation or the phi-ladder.
- Does not relate the value to baryon or dark-energy densities.
- Does not prove that exactly five candidates exist.
- Does not specify the RS units in which the number is expressed.
formal statement (Lean)
27noncomputable def omegaCDM : ℝ := 0.26
proof body
Definition body.
28