xenon_more_sensitive
plain-language theorem explainer
XENON1T sensitivity exceeds DAMA/LIBRA by a factor greater than five, so a WIMP signal should have appeared if dark matter consisted of weakly interacting massive particles. Dark matter experimentalists reconciling the DAMA annual modulation with null results from other detectors would cite this to quantify the tension. The proof is a one-line wrapper that unfolds the sensitivity definition and normalizes the numerical comparison.
Claim. The sensitivity of the XENON1T experiment exceeds that of DAMA/LIBRA by a factor greater than 5.
background
In the Recognition Science treatment of the DAMA/LIBRA annual modulation, dark matter is identified with the substrate rather than with particles. The WIMP structure encodes weakly interacting massive particles of mass 10-1000 GeV whose thermal relic density arises from freeze-out at the weak scale. The XENON sensitivity definition supplies the concrete numerical ratio of 10.0 between XENON1T and DAMA detection thresholds.
proof idea
The proof is a one-line wrapper. It unfolds the XENON sensitivity definition, which evaluates to 10, then applies norm_num to establish the inequality 10 > 5.
why it matters
The result supplies the quantitative step for the EA-005 certificate and is invoked directly by the theorem that multiple null results disfavor the WIMP explanation. It reinforces the substrate model in which dark matter is the ledger carrier, predicting zero WIMP signals and attributing the DAMA modulation to detector systematics. The declaration closes one link in the chain from the Law of Existence model to the experimental prediction of null direct-detection outcomes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.