dmIsNot
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.