excess_rate
plain-language theorem explainer
The definition assigns the constant value 20 to the excess event rate in events per ton per year for the XENON1T low-energy excess. Experimental physicists comparing dark matter search data to background models would cite this value when testing tritium hypotheses. It is a direct numerical assignment with no computation or lemmas applied.
Claim. The excess event rate is defined as $20$ events per ton per year.
background
The module EA-006 analyzes the XENON1T/nT low-energy excess of 2-3 keV electron recoils with observed rate ~10-30 events above background. Possible origins include tritium at natural concentrations, solar axions via Primakoff processes, or neutrino magnetic moments above $10^{-11} mu_B$. Upstream WIMP is defined as a structure with mass 10-1000 GeV, weak-scale cross section, and thermal relic status, noted as undetected despite extensive searches.
proof idea
Direct numerical definition assigning 20.0 with no lemmas or tactics.
why it matters
This definition is used by the downstream tritium_rate_matches theorem, which establishes |tritium_rate - excess_rate| < 10. It supports the module's RS verdict that tritium background is most likely with P ~70 percent and no new physics required. The value quantifies the fit within the 2-3 sigma significance range for the excess.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.