ea006_certificate
plain-language theorem explainer
The ea006_certificate assembles a textual summary of the XENON1T low-energy excess analysis, stating that the 2-3 keV electron recoil excess is most likely natural tritium background at moderate 2-3 sigma significance with matching rates and spectrum. Physicists working on direct detection experiments or RS phenomenology would cite it to record the framework's assessment that solar axions remain viable but unnecessary while neutrino magnetic moments are disfavored. The definition works by direct concatenation of verdict strings drawn from the 8
Claim. The certificate records that an electron-recoil excess between 2 and 3 keV carries moderate significance of roughly 2-3 standard deviations, that a tritium background rate of approximately 25 events per ton per year reproduces both the observed rate and the spectral peak at 2-3 keV, that any solar-axion electron coupling satisfies $g_{ae}<10^{-13}$, that a neutrino magnetic moment would require an enhancement of order $10^8$ over the Standard-Model value, and that no beyond-Standard-Model physics is required.
background
The Experimental.Xenon1TExcess module examines the low-energy electron-recoil excess reported by XENON1T/nT. Excess energy lies in the 2-3 keV window below standard WIMP thresholds; significance is quantified as excess_significance; tritium_rate and tritium_spectrum_peak compare the natural tritium hypothesis against data; axion_coupling_small and moment_exceeds_sm bound the alternative explanations. MODULE_DOC states the three candidate mechanisms (tritium, solar axions, neutrino magnetic moment) and records the RS preference for tritium as the explanation requiring no new physics. Upstream theorem axion_coupling_small asserts $g_{ae}<10^{-13}$ to satisfy CAST limits; bsm_not_required asserts that tritium_most_likely holds by reflexivity.
proof idea
The definition is a direct string concatenation that interleaves fixed header lines with the verdicts of the eight upstream theorems: excess_low_energy and significance_moderate supply the energy window and sigma level; tritium_rate_matches and tritium_spectrum_peak confirm the background fit; axion_coupling_small, moment_exceeds_sm, neutrino_disfavored and bsm_not_required supply the coupling bound, moment enhancement, disfavoring comparison and final no-BSM conclusion. No tactics or reductions are applied beyond the literal assembly of these strings.
why it matters
The certificate closes the experimental analysis block of the Xenon1TExcess module by distilling the chain of eight supporting theorems into a single human-readable record. It implements the RS verdict that tritium background suffices, thereby illustrating how the framework accommodates existing data without additional structure beyond the phi-ladder and forcing chain. No downstream theorems depend on it; the open question it leaves is whether future annual-modulation or spectral-distortion measurements will remain consistent with tritium.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.