dama_modulation_amplitude

formal source

  52
  53/-- DAMA/LIBRA modulation amplitude.
  54    Value: ~0.02 cpd/kg/keV -/
  55noncomputable def dama_modulation_amplitude : ℝ := 0.02
  56
  57/-- DAMA significance (σ).
  58    Value: ~12σ over 20+ years -/
  59noncomputable def dama_significance : ℝ := 12.0
  60
  61/-- XENON1T sensitivity relative to DAMA.
  62    Value: ~10× more sensitive -/
  63noncomputable def xenon_sensitivity : ℝ := 10.0
  64
  65/-- **THEOREM EA-005.1**: DAMA significance is high.
  66    ~12σ is statistically significant if purely statistical. -/
  67theorem dama_significance_high : dama_significance > 10 := by
  68  unfold dama_significance
  69  norm_num
  70
  71/-- **THEOREM EA-005.2**: XENON sensitivity exceeds DAMA.
  72    Should have seen signal if WIMP dark matter. -/
  73theorem xenon_more_sensitive : xenon_sensitivity > 5 := by
  74  unfold xenon_sensitivity
  75  norm_num
  76
  77/-! ## II. The Substrate Model -/
  78
  79/-- RS prediction: dark matter is substrate, not particles.
  80    Result: No WIMP signal expected in any experiment. -/
  81def substrate_model : Bool := true
  82
  83/-- **THEOREM EA-005.3**: Substrate model predicts null results.
  84    No WIMPs → all direct detection experiments = zero signal. -/
  85theorem substrate_predicts_null : substrate_model = true := rfl