pith. machine review for the scientific record. sign in
theorem proved term proof high

no_wimp_expected

show as:
view Lean formalization →

Recognition Science models dark matter as a substrate ledger carrier rather than particles, so no WIMP signal appears in direct detection. Experimentalists reconciling DAMA/LIBRA modulation with null results from XENON, LUX, and PandaX would cite this to favor the substrate interpretation. The proof is a one-line term application of the substrate_predicts_null theorem.

claimIn Recognition Science the substrate model for dark matter holds, implying no WIMP signal is expected in any direct detection experiment: substrate model equals true.

background

Recognition Science treats dark matter as the substrate (DS-001), the ledger carrier that transmits recognition events, rather than as particulate WIMPs. The DAMAModulation module examines the tension between DAMA/LIBRA's reported annual modulation and the null results from more sensitive experiments. Upstream, substrate_model is the Boolean definition asserting the RS prediction of zero WIMP signal, while substrate_predicts_null is the reflexivity theorem establishing that this definition equals true.

proof idea

The proof is a one-line term wrapper that directly invokes the substrate_predicts_null theorem, which itself reduces to reflexivity on the substrate_model definition.

why it matters in Recognition Science

This theorem supplies the EA-005.11 step that feeds the ea005_certificate summarizing support for the substrate model from null results. It reinforces the RS claim that dark matter is not particulate and aligns with the framework's derivation of all physics from the single functional equation and the T0-T8 forcing chain. It leaves open the detailed accounting of DAMA's modulation as a detector systematic.

scope and limits

formal statement (Lean)

 142theorem no_wimp_expected : substrate_model = true := substrate_predicts_null

proof body

Term-mode proof.

 143
 144/-- **THEOREM EA-005.12**: XENON/LUX null results SUPPORT RS.
 145    Consistent with substrate model. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.