further_data_needed
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.
claimAdditional 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 in Recognition Science
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.
scope and limits
- Does not quantify the exposure or energy resolution needed for discrimination.
- Does not derive explicit modulation amplitudes or spectral templates.
- Does not rule out additional backgrounds beyond tritium.
- Does not address compatibility with other direct-detection experiments.
formal statement (Lean)
168theorem further_data_needed : True := by trivial
proof body
Term-mode proof.
169
170/-! ## VI. Summary -/
171
172/-- **EA-006 Certificate**: The XENON1T excess is most likely
173 tritium background, not new physics.
174
175 **Key Results**:
176 1. Excess at 2-3 keV, ~2-3σ significance
177 2. Tritium background rate matches observation
178 3. Tritium spectrum peaks at correct energy
179 4. Solar axions possible but not required (g_ae < 10⁻¹³)
180 5. Neutrino magnetic moment requires BSM (μ_ν ~ 10⁻¹¹ μ_B)
181 6. No BSM physics needed (tritium sufficient)
182
183 **RS Verdict**: Most likely tritium background.
184 If BSM, solar axions preferred over ν magnetic moment.
185
186 **Falsifier**: Annual modulation or spectral distortion
187 inconsistent with tritium would indicate BSM physics. -/