multiple_nulls_disfavor_wimp
plain-language theorem explainer
Multiple null results from XENON and LUX disfavor a WIMP particle interpretation of the DAMA modulation signal. Dark matter experimentalists comparing direct detection claims would cite this to quantify the tension between positive and null outcomes. The proof is a one-line reference to the established sensitivity comparison theorem.
Claim. If the relative sensitivity of XENON1T to DAMA exceeds 5, then multiple null results disfavor a WIMP explanation for the observed annual modulation.
background
The DAMA/LIBRA module frames dark matter as a substrate (ledger carrier) rather than particles, predicting null signals in direct detection. The definition xenon_sensitivity assigns the numerical value 10.0 to the relative sensitivity of XENON1T versus DAMA. The upstream theorem xenon_more_sensitive states that XENON sensitivity exceeds DAMA and should have seen a signal if WIMPs were present, with its proof unfolding the definition and applying numerical normalization.
proof idea
The proof is a one-line wrapper that directly invokes the xenon_more_sensitive theorem.
why it matters
This result supports the EA-005 analysis in the module, where null outcomes from XENON/LUX/PandaX confirm the substrate model over WIMPs. It feeds the claim that DAMA modulation is likely systematic and aligns with Recognition Science predictions of zero WIMP signal. The theorem closes part of the experimental tension without addressing other dark matter candidates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.