dama_likely_systematic
plain-language theorem explainer
The theorem establishes that the temperature coefficient for NaI(Tl) detectors is positive, so seasonal temperature swings at Gran Sasso can modulate detection efficiency and produce an annual signal. Experimental groups comparing DAMA/LIBRA with COSINE-100 and xenon-based detectors cite it to classify the ~12σ modulation as systematic rather than dark-matter induced. The proof is a one-line wrapper that unfolds the coefficient definition and applies norm_num to verify the inequality.
Claim. Let $k$ be the temperature coefficient of NaI(Tl) detectors, defined as the fractional efficiency change per degree Celsius. Then $k > 0$.
background
Recognition Science treats dark matter as a substrate ledger carrier rather than WIMPs, so direct-detection experiments are predicted to return null results. The upstream definition sets the temperature coefficient to 0.01 (approximately 1 percent efficiency shift per degree) and notes the ~10°C seasonal swing at Gran Sasso. This supplies the environmental mechanism that can mimic the DAMA annual modulation without new particles.
proof idea
The proof is a one-line wrapper. It unfolds the temperature_coefficient definition and applies norm_num to confirm that the concrete value 0.01 is strictly positive.
why it matters
The result is invoked by the EA-005 certificate, which summarizes the full DAMA analysis and concludes the modulation is systematic. It closes one link in the experimental chain that supports the substrate model over particle dark matter, consistent with the null outcomes from XENON, LUX, and PandaX. No open scaffolding remains for this specific inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.