tritium_most_likely
plain-language theorem explainer
The theorem asserts that the predicted tritium event rate in xenon exceeds zero, establishing tritium as the dominant explanation for the XENON1T low-energy excess with roughly 70 percent likelihood among alternatives. Experimental physicists analyzing dark matter detector backgrounds would cite this result when evaluating natural radioactivity versus new physics. The proof is a term-mode reduction that unfolds the rate definition and applies numerical normalization to confirm positivity.
Claim. The predicted tritium-induced event rate $r$ in the XENON1T detector satisfies $r > 0$, where $r$ is the noncomputable constant 25.0 events per ton per year.
background
The XENON1T/nT module analyzes the low-energy electron recoil excess at 2-3 keV, with observed rates of 10-30 events above background and significance 2-3 sigma. Tritium background is modeled via a rate definition set to 25.0 events per ton per year, arising from natural tritium at the $10^{-20}$ concentration level in xenon that reproduces the observed spectrum. Upstream results include the tritium rate definition itself and the axion structure from cosmology, which supplies mass and decay constant parameters for alternative hypotheses.
proof idea
The proof is a one-line term wrapper that unfolds the tritium rate definition and applies norm_num to evaluate the constant 25.0 as positive.
why it matters
This result feeds the parent theorem that no beyond-standard-model physics is required, since tritium background explains the excess naturally. It occupies the EA-006.5 position in the module's chain, aligning with Recognition Science emphasis on minimal assumptions over solar axion or neutrino magnetic moment alternatives. The downstream application confirms tritium as the leading explanation without invoking new physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.