temperature_coefficient
plain-language theorem explainer
The temperature coefficient for NaI(Tl) detectors is defined as the constant 0.01, representing an approximate one percent efficiency change per degree Celsius. DAMA/LIBRA analysts would cite this value when modeling the observed annual modulation as an environmental systematic. The definition is a direct numerical assignment with no lemmas or computation.
Claim. The temperature coefficient for NaI(Tl) is the constant $0.01$, corresponding to an approximate $1$ percent change in detection efficiency per degree Celsius.
background
The module analyzes the DAMA/LIBRA annual modulation signal under the Recognition Science substrate model for dark matter, where the modulation is treated as a detector systematic rather than a WIMP signal. Temperature enters via the upstream definition in BoltzmannDistribution: temperature(beta) equals $1$/beta and is the derivative of average energy with respect to entropy, which can be related to J-cost derivatives. The coefficient links seasonal temperature swings at Gran Sasso to efficiency variations that could mimic the reported DAMA amplitude.
proof idea
Direct definition that assigns the numerical value $0.01$ with no lemmas applied.
why it matters
This constant is unfolded inside the proofs of dama_likely_systematic and temperature_can_explain, which conclude that a $10$ degree Celsius variation times the coefficient exceeds a $5$ percent efficiency swing and can therefore account for the DAMA signal. It supports the module's claim that the modulation is systematic, consistent with the RS prediction of null WIMP results in XENON-class detectors and the substrate interpretation of dark matter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.