temperature_coefficient
The definition supplies the fixed value 0.01 for the temperature coefficient of NaI(Tl) detectors, encoding an approximate one-percent efficiency shift per degree Celsius. Experimental groups reanalyzing DAMA/LIBRA annual modulation data would cite it when testing whether seasonal temperature swings at Gran Sasso can account for the observed signal. It is introduced by direct assignment of the real constant together with a short physical annotation.
claimThe temperature coefficient for NaI(Tl) is the real number $0.01$, representing an approximate $1$ percent change in detection efficiency per degree Celsius.
background
The DAMA/LIBRA module examines whether the reported annual modulation arises from environmental systematics rather than dark-matter interactions. Recognition Science models dark matter as a substrate ledger carrier, which predicts null WIMP signals in all direct-detection experiments. The upstream temperature definition states that temperature equals the inverse Lagrange multiplier β and satisfies the thermodynamic relation dE/dS = T.
proof idea
The definition is a direct constant assignment of the real number 0.01. No lemmas or tactics are invoked; the value is supplied explicitly for use in downstream arithmetic checks.
why it matters in Recognition Science
The constant feeds the two downstream theorems that establish temperature_can_explain (showing a 10 percent efficiency swing from 10 °C variation) and dama_likely_systematic. These results support the EA-005 claim that DAMA modulation is environmental and that XENON/LUX/PandaX null results are consistent with the substrate model. The coefficient therefore closes one link in the chain from Recognition Science dark-matter predictions to concrete experimental systematics.
scope and limits
- Does not derive the numerical value from Recognition Science axioms or the J-cost functional.
- Does not incorporate radon or other background systematics.
- Applies only to NaI(Tl) and does not generalize to other detector materials.
- Does not claim that temperature is the sole explanation for the DAMA signal.
Lean usage
theorem temperature_can_explain : temperature_coefficient * annual_temp_variation > 0.05 := by unfold temperature_coefficient annual_temp_variation; norm_numformal statement (Lean)
101noncomputable def temperature_coefficient : ℝ := 0.01 -- ~1% per degree
proof body
Definition body.
102
103/-- Annual temperature variation at Gran Sasso.
104 Value: ~10°C seasonal variation -/