further_data_needed
plain-language theorem explainer
The declaration asserts that further experimental observations are required to separate the tritium background hypothesis from possible solar axion or neutrino magnetic moment contributions to the XENON1T 2-3 keV excess. Direct-detection experimentalists would cite it when summarizing the current status of the anomaly and planning follow-up runs. The proof is a one-line term application of the trivial tactic that discharges the goal True.
Claim. Additional data, specifically checks for annual modulation (absent for tritium, present for axions or neutrino moments) and spectral shape deviations, are required to distinguish the tritium background from solar axion or enhanced neutrino magnetic moment explanations of the XENON1T low-energy electron recoil excess.
background
The module analyzes the XENON1T/nT low-energy excess at 2-3 keV electron recoils with ~2-3σ significance and rate ~10-30 events. Three RS-compatible explanations are considered: natural tritium at ~10^{-20} level in xenon (fits rate and spectrum), solar axions via Primakoff-like coupling with g_ae < 10^{-13}, and neutrino magnetic moment μ_ν ~ 10^{-11} μ_B requiring BSM. The local setting states that tritium background is most likely, with no new physics required, while axions remain possible but not demanded. Upstream results supply foundational structures for stating empirical conditions (DomainBootstrap.required) and collision-free program properties (OptionAEmpiricalProgram.is), plus constants and ledger constructions that anchor the experimental mapping.
proof idea
The proof is a term-mode one-line wrapper that applies the trivial tactic directly to the goal True. No lemmas from the depends_on list are invoked; the tactic discharges the proposition without reduction steps or hypothesis discharge.
why it matters
This theorem closes the EA-006 analysis by marking the point at which the RS verdict (tritium most likely, BSM not required) is asserted while leaving an explicit falsifier path. It feeds the summary certificate that lists tritium rate match, spectrum peak, and the preference for axions over neutrino moments if BSM is confirmed. The result touches the Recognition framework's experimental interface by supplying a concrete discriminator (annual modulation or spectral distortion) that would force revision of the no-BSM conclusion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.