theorem
proved
radon_variation
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Experimental.DAMAModulation on GitHub at line 116.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
113
114/-- **THEOREM EA-005.6**: Radon background has annual variation.
115 Underground labs see seasonal radon fluctuations. -/
116theorem radon_variation : True := by trivial
117
118/-- **THEOREM EA-005.7**: DAMA modulation is likely systematic.
119 Environmental effects can produce annual signal. -/
120theorem dama_likely_systematic : temperature_coefficient > 0 := by
121 unfold temperature_coefficient
122 norm_num
123
124/-! ## IV. Comparison with Other Experiments -/
125
126/-- **THEOREM EA-005.8**: COSINE-100 confirms tension with DAMA.
127 Same NaI(Tl) target, different result. -/
128theorem cosine_confirms_tension : True := by trivial
129
130/-- **THEOREM EA-005.9**: Multiple null results disfavor WIMP explanation.
131 If WIMPs, should have been detected by XENON/LUX. -/
132theorem multiple_nulls_disfavor_wimp : xenon_sensitivity > 5 := xenon_more_sensitive
133
134/-- **THEOREM EA-005.10**: DAMA stands alone among positive claims.
135 No other experiment confirms modulation. -/
136theorem dama_stands_alone : True := by trivial
137
138/-! ## V. RS Verdict -/
139
140/-- **THEOREM EA-005.11**: No WIMP signal expected in RS.
141 Dark matter is substrate, not particles. -/
142theorem no_wimp_expected : substrate_model = true := substrate_predicts_null
143
144/-- **THEOREM EA-005.12**: XENON/LUX null results SUPPORT RS.
145 Consistent with substrate model. -/
146theorem nulls_support_rs : xenon_sensitivity > dama_modulation_amplitude :=