DarkMatterFalsifier
plain-language theorem explainer
The DarkMatterFalsifier structure encodes three explicit conditions under which the ledger-shadow account of dark matter would fail. A cosmologist checking rotation curves or CMB ratios against the Recognition Science φ-ladder would cite it to bound the model against MOND or photon-coupled alternatives. The definition is a direct record that packages the three falsifiers and the required contradiction into a single Prop.
Claim. A structure consists of propositions $P_1$ (dark matter does not exist), $P_2$ (the dark-matter to baryon ratio differs from $φ^3 + 1$), $P_3$ (dark matter couples strongly to photons), together with the implication $P_1 ∨ P_3 → ⊥$.
background
The Cosmology.DarkMatter module treats dark matter as non-luminous ledger configurations in the σ=0, Z≠0 phantom sector at the temporal scale of the 8-tick parity cycle. It imports Constants, Cost, and PhiForcing to supply the φ-ladder ratios and J-cost suppression. The module documentation states that the derivation is falsified if dark matter does not exist, if the ratio deviates from φ³+1, or if dark matter couples strongly to photons.
proof idea
This is a structure definition with an empty proof body. It assembles the three named propositions and the implication clause into a single record type with no further reduction or lemma application.
why it matters
The definition closes the COS-010 ledger-shadow claim by listing the precise observational tests that would refute it. It sits inside the eight-tick octave and φ-ladder framework of the forcing chain. No downstream theorems reference it, leaving open whether a concrete counterexample such as a confirmed MOND regime can be formalized inside the same structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.