dmIsNot
dmIsNot enumerates four classes of dark matter candidates excluded by observation in the Recognition Science ledger-shadow model. Cosmologists using the COS-010 framework cite it when contrasting the phantom sector against baryons, black holes, neutrinos, and modified gravity. The definition is a direct enumeration of empirical constraints drawn from nucleosynthesis and structure-formation data.
claimThe excluded dark matter candidates are the list consisting of MACHOs (ruled out for most mass range), primordial black holes (limited), hot dark matter (neutrinos too fast for structure), and modified Newtonian dynamics alone (does not fit clusters).
background
In the COS-010 module dark matter is introduced as non-luminous ledger configurations arising from the odd-phase orbits of the eight-tick parity cycle. The definition dmIsNot records the observational exclusions that follow from this picture: baryons are limited by big-bang nucleosynthesis, black holes by microlensing, neutrinos by their inability to seed structure, and modified gravity by cluster dynamics. Upstream results supply the supporting structures: NucleosynthesisTiers.of gives the discrete φ-tiers for nuclear densities and photon fluxes, RSNativeUnits.Mass supplies the real-valued mass type, and LargeScaleStructureFromRS.scale supplies the φ-powered length scales used to quantify structure formation.
proof idea
The definition is a direct assignment of a four-element string list; no lemmas or tactics are applied beyond the literal construction of the excluded-candidate enumeration.
why it matters in Recognition Science
The definition sharpens the ledger-shadow interpretation of the phantom sector by stating what dark matter cannot be, thereby preparing the ground for the suppression mechanism described in the module. It sits inside the eight-tick octave and the D=3 spatial structure forced by the UnifiedForcingChain, and it is consistent with the J(φ)-suppressed signal at 1.79 GeV mentioned in the module documentation. No downstream theorems yet depend on it.
scope and limits
- Does not derive the exclusion list from the Recognition Composition Law or the forcing chain.
- Does not supply quantitative mass or cross-section bounds.
- Does not assert that any particular candidate is impossible in all parameter regimes.
- Does not replace the positive ledger-shadow model with a new mechanism.
formal statement (Lean)
94def dmIsNot : List String := [
proof body
Definition body.
95 "MACHOs (ruled out for most mass range)",
96 "Primordial black holes (limited)",
97 "Hot dark matter (neutrinos - too fast)",
98 "MOND alone (doesn't fit clusters)"
99]
100
101/-! ## Standard Candidates -/
102
103/-- WIMPs: Weakly Interacting Massive Particles
104 - Mass: ~10-1000 GeV
105 - Interaction: Weak-scale
106 - Thermal relic: Ω_dm from freeze-out
107 - Status: NOT found despite decades of searches -/