annual_temp_variation
plain-language theorem explainer
The declaration supplies the numerical value of seasonal temperature swing at the Gran Sasso laboratory as ten degrees Celsius. Experimental physicists analyzing DAMA/LIBRA data would cite this constant when testing whether detector efficiency variations can account for the observed modulation. The definition is a direct real-number assignment with no computation or lemmas required.
Claim. Let $T$ denote the annual temperature variation at Gran Sasso. Then $T = 10^circ mathrm{C}$.
background
The DAMA/LIBRA module models dark matter as a substrate (ledger carrier) rather than WIMPs, predicting null results in direct detection while attributing apparent modulation to systematics such as temperature. Upstream results include the S-matrix amplitude definition giving transition elements between states and the double-slit amplitude as the sum of complex path phases, supplying the general quantum framework though not invoked here. The module doc states that DAMA modulation is likely environmental and that XENON/LUX/PandaX null results support the substrate model.
proof idea
The definition is a direct numerical assignment of the constant 10.0. No lemmas from the upstream amplitude or for structures are applied; the value is hardcoded from the experimental context of seasonal swings at Gran Sasso.
why it matters
This constant is used by the downstream theorem temperature_can_explain to show that a 10°C swing times a 1%/°C coefficient produces a 10% efficiency variation sufficient for the signal. It supports the Recognition Science claim that DAMA results are consistent with the substrate model rather than particle dark matter, aligning with the forcing chain prediction of no WIMP signals and the eight-tick octave structure. It provides a concrete mechanism closing part of the experimental tension between DAMA and null-result experiments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.