dmEvidence
dmEvidence enumerates five standard observational signatures of dark matter as a fixed list of strings. Cosmologists and Recognition Science authors would cite it when summarizing the phantom sector at temporal resolution in the COS-010 paper. The definition is a direct enumeration with no computation or lemmas applied.
claimThe empirical evidence for dark matter consists of the list: galaxy rotation curves remaining flat rather than Keplerian, galaxy cluster masses exceeding visible matter by a factor of approximately ten, gravitational lensing maps of unseen mass distributions, CMB acoustic peaks constraining total matter content, and the requirement for density seeds to enable structure formation.
background
The Cosmology.DarkMatter module treats dark matter as non-luminous ledger configurations in the σ=0, Z≠0 phantom sector at temporal resolution, specifically odd-phase orbits of the 8-tick parity cycle. This constitutes one of five projections of the same object, with unification handled in Cosmology.PhantomSectorStratification. The module records Ω_dm ≈ 0.27, Ω_b ≈ 0.05 and ratio ≈5.4, arising naturally from 8-tick phase structure where ledger entries couple gravitationally but not to photons.
proof idea
The definition is a direct enumeration of the five strings listed in the doc-comment. No lemmas from the upstream results (CrystalStructure, OptionAEmpiricalProgram.is, EdgeLengthFromPsi.is, UniversalForcingSelfReference.for, MechanismDesignFromSigma.is, MockThetaPhantom.is) are invoked; the body simply constructs the List String.
why it matters in Recognition Science
This definition supplies the observational anchor for the COS-010 claim that dark matter equals ledger shadows from 8-tick phase structure. It supports the Recognition Science derivation of cosmology from the unified forcing chain (T0-T8), including D=3 dimensions and phi-forced self-similarity, and is consistent with the suppression mechanism stated for the rs_explains_null_detection theorem. No downstream uses are recorded.
scope and limits
- Does not derive mass values or phi-ladder rungs for any dark matter candidate.
- Does not compute Ω_dm or Ω_b in RS-native units (c=1, ħ=φ^{-5}).
- Does not prove the phase-mismatch suppression for null detections.
- Does not classify specific candidates beyond the listed observations.
formal statement (Lean)
79def dmEvidence : List String := [
proof body
Definition body.
80 "Galaxy rotation curves (flat, not Keplerian)",
81 "Galaxy cluster mass (10× visible)",
82 "Gravitational lensing (mass maps)",
83 "CMB acoustic peaks (matter content)",
84 "Structure formation (need seeds)"
85]
86
87/-! ## What Dark Matter Is NOT -/
88
89/-- Dark matter is NOT:
90 - Ordinary matter (baryons) - BBN limits
91 - Black holes (mostly) - microlensing limits
92 - Neutrinos (mostly) - too hot for structure
93 - Modified gravity (alone) - cluster data -/