pith. machine review for the scientific record. sign in
def

substrate_model

definition
show as:
view math explainer →
module
IndisputableMonolith.Experimental.DAMAModulation
domain
Experimental
line
81 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Experimental.DAMAModulation on GitHub at line 81.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  86
  87/-- **THEOREM EA-005.4**: XENON/LUX null results support substrate.
  88    Consistent with RS dark matter model. -/
  89theorem null_supports_substrate : xenon_sensitivity > dama_modulation_amplitude := by
  90  unfold xenon_sensitivity dama_modulation_amplitude
  91  norm_num
  92
  93/-! ## III. DAMA Systematic Explanation -/
  94
  95/-- DAMA modulation is likely systematic.
  96    Candidates: temperature, radon, detector efficiency -/
  97def dama_systematic : Bool := true
  98
  99/-- Temperature coefficient for NaI(Tl).
 100    Annual temp variation → efficiency modulation -/
 101noncomputable def temperature_coefficient : ℝ := 0.01  -- ~1% per degree
 102
 103/-- Annual temperature variation at Gran Sasso.
 104    Value: ~10°C seasonal variation -/
 105noncomputable def annual_temp_variation : ℝ := 10.0  -- degrees C
 106
 107/-- **THEOREM EA-005.5**: Temperature can explain modulation amplitude.
 108    10°C × 1%/°C = 10% efficiency variation, sufficient for signal. -/
 109theorem temperature_can_explain :
 110    temperature_coefficient * annual_temp_variation > 0.05 := by
 111  unfold temperature_coefficient annual_temp_variation