substrate_predicts_null
plain-language theorem explainer
The substrate model asserts that dark matter functions as a ledger carrier rather than WIMPs, so every direct detection experiment registers zero signal. Experimental groups reconciling the DAMA/LIBRA annual modulation with null results from XENON, LUX and PandaX would cite this statement. The proof is a one-line reflexivity reduction on the constant definition of the substrate model.
Claim. In the Recognition Science framework the substrate model holds, i.e., dark matter is realized as a ledger carrier rather than weakly interacting massive particles, which entails null results for all direct detection experiments.
background
The module EA-005 analyzes the DAMA/LIBRA annual modulation against null results from more sensitive detectors. Within this setting dark matter is identified with the substrate (ledger carrier) rather than particles. The upstream definition substrate_model is the constant Bool value true, which encodes the RS prediction that no WIMP signal appears in any experiment. The sibling definition model from CPM2D supplies the underlying Hypothesis bundle but is not invoked in the present reduction.
proof idea
The proof is a term-mode one-liner that applies reflexivity directly to the constant definition substrate_model := true.
why it matters
This theorem supplies the base fact for no_wimp_expected and for the ea005_certificate summary. It fills the EA-005.3 slot in the module's key theorems list, confirming that the substrate model is consistent with the observed null results from XENON/LUX/PandaX. The result anchors the RS claim that dark matter is substrate, not particles, and closes the experimental tension loop described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.