cosine_confirms_tension
plain-language theorem explainer
COSINE-100 data establishes tension with DAMA/LIBRA modulation claims using identical NaI(Tl) targets. Dark matter experimentalists would reference this when evaluating consistency across direct detection searches. The statement is established by a direct trivial reduction in the formal system.
Claim. COSINE-100 confirms tension with the DAMA/LIBRA annual modulation signal despite using the same NaI(Tl) target.
background
Recognition Science treats dark matter as a substrate ledger carrier rather than as particles. The upstream WIMP definition specifies a structure with mass around 10-1000 GeV, weak-scale cross section, and thermal relic abundance from freeze-out, noting that such particles have not been found despite decades of searches.
proof idea
The proof is a term-mode application of the trivial tactic.
why it matters
This result feeds into the EA-005 certificate summarizing the DAMA analysis. It reinforces the Recognition Science substrate model, which predicts no WIMP signals in direct detection experiments, consistent with the null outcomes and the tension highlighted here. The module documentation positions it as part of the key theorems supporting the systematic interpretation of the DAMA signal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.