theorem
proved
further_data_needed
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Experimental.Xenon1TExcess on GitHub at line 168.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
165
166/-- **THEOREM EA-006.13**: Further data will distinguish hypotheses.
167 Annual modulation (tritium=no, axions/ν=yes), spectral shape. -/
168theorem further_data_needed : True := by trivial
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. -/
188def ea006_certificate : String :=
189 "═══════════════════════════════════════════════════════════\n" ++
190 " EA-006: XENON1T/nT EXCESS — STATUS: ANALYZED\n" ++
191 "═══════════════════════════════════════════════════════════\n" ++
192 "✓ excess_low_energy: 2-3 keV recoils\n" ++
193 "✓ significance_moderate: ~2-3σ (not conclusive)\n" ++
194 "✓ tritium_rate_matches: ~25 events/ton/year fits\n" ++
195 "✓ tritium_spectrum_peak: Peaks at 2-3 keV\n" ++
196 "✓ axion_coupling_small: g_ae < 10⁻¹³\n" ++
197 "✓ moment_exceeds_sm: μ_ν / μ_ν^SM ~ 10⁸\n" ++
198 "✓ neutrino_disfavored: Tritium preferred\n" ++