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

multiple_nulls_disfavor_wimp

show as:
view Lean formalization →

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.

claimIf 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 132theorem multiple_nulls_disfavor_wimp : xenon_sensitivity > 5 := xenon_more_sensitive

proof body

Term-mode proof.

 133
 134/-- **THEOREM EA-005.10**: DAMA stands alone among positive claims.
 135    No other experiment confirms modulation. -/

depends on (2)

Lean names referenced from this declaration's body.