pith. machine review for the scientific record. sign in
theorem proved term proof high

temperature_can_explain

show as:
view Lean formalization →

The theorem establishes that the product of the NaI(Tl) temperature coefficient (0.01 per °C) and annual temperature variation at Gran Sasso (10 °C) exceeds 0.05, indicating seasonal changes can induce at least 5% detector efficiency modulation. Experimental physicists evaluating DAMA/LIBRA annual modulation data would cite this when testing whether environmental systematics suffice to explain the observed amplitude without invoking dark matter particles. The proof is a one-line wrapper that unfolds the two constant definitions and reduces the

claimLet $c = 0.01$ be the temperature coefficient of NaI(Tl) scintillators and $ΔT = 10$ the annual temperature variation in °C at Gran Sasso. Then $c · ΔT > 0.05$.

background

In the DAMA/LIBRA module the analysis treats observed annual modulation as a candidate systematic rather than a dark-matter signal. The temperature coefficient is the constant 0.01 representing roughly 1% efficiency change per degree Celsius for NaI(Tl). The annual temperature variation is the constant 10.0 representing the seasonal swing recorded at the Gran Sasso laboratory. These two definitions are the only hypotheses required by the theorem. The surrounding module frames the result inside the Recognition Science substrate model for dark matter, which predicts null WIMP signals at all direct-detection experiments and attributes DAMA modulation to detector or environmental effects.

proof idea

The proof unfolds the definitions of temperature_coefficient and annual_temp_variation, then applies norm_num to verify the numerical inequality 0.01 × 10 > 0.05.

why it matters in Recognition Science

The result supplies the EA-005.5 step that feeds the ea005_certificate, which certifies the DAMA modulation as likely systematic. It thereby supports the Recognition Science claim that dark matter is substrate (no WIMPs) and that all direct-detection experiments should return null results. The theorem closes one concrete environmental channel in the EA-005 chain while leaving radon and other systematics for separate treatment.

scope and limits

formal statement (Lean)

 109theorem temperature_can_explain :
 110    temperature_coefficient * annual_temp_variation > 0.05 := by

proof body

Term-mode proof.

 111  unfold temperature_coefficient annual_temp_variation
 112  norm_num
 113
 114/-- **THEOREM EA-005.6**: Radon background has annual variation.
 115    Underground labs see seasonal radon fluctuations. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.