tritium_rate_matches
plain-language theorem explainer
The theorem establishes that the absolute difference between the predicted tritium background rate and the observed excess rate in XENON1T data is less than 10 events per ton per year. Physicists interpreting the low-energy electron recoil excess would reference this result to support a conventional background explanation over new physics. The proof proceeds by unfolding the two rate constants and applying numerical normalization to confirm the bound holds.
Claim. $|r_T - r_E| < 10$ events/ton/year, where $r_T$ is the tritium event rate prediction and $r_E$ is the excess event rate above background.
background
The module analyzes the XENON1T/nT low-energy electron recoil excess at 2-3 keV. Recognition Science evaluates three explanations: tritium background from natural radioactivity at the $10^{-20}$ level, solar axions via Primakoff-like coupling, and enhanced neutrino magnetic moment scattering. The verdict favors tritium as the most likely cause, requiring no beyond-Standard-Model physics. Excess rate is defined as the constant 20.0 events/ton/year. Tritium rate is defined as the constant 25.0 events/ton/year, consistent with the concentration range that produces 10-40 events/ton/year.
proof idea
The proof is a term-mode reduction. It unfolds the definitions of tritium_rate and excess_rate, then applies norm_num with the abs_of_nonneg lemma to reduce the absolute-value inequality to a direct numerical check.
why it matters
This result feeds directly into the ea006_certificate definition, which assembles the full XENON1T analysis and states that the excess is most likely tritium background. It completes the EA-006.3 step in the module's key theorems list and supports the Recognition Science assessment that natural radioactivity suffices. The parent certificate records the 2-3 keV location, moderate significance, and tritium spectrum match without invoking axions or neutrino moments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.