neutrino_disfavored
plain-language theorem explainer
The theorem shows that the tritium background rate of 25 events per ton per year exceeds the 10^{-11} Bohr magneton scale assigned to a neutrino magnetic moment by many orders of magnitude, thereby disfavoring a neutrino origin for the XENON1T 2-3 keV excess. Experimentalists working on low-energy recoils or dark-matter searches would cite it when arguing that natural radioactivity suffices. The proof is a direct term reduction that unfolds the two constant definitions and normalizes the resulting numerical comparison.
Claim. The predicted tritium event rate exceeds the neutrino magnetic moment value: $25 > 10^{-11}$, where the tritium rate is given in events per ton per year and the moment is expressed in Bohr magnetons.
background
The module examines the XENON1T/nT low-energy electron-recoil excess at 2-3 keV and weighs three candidate explanations: tritium contamination, solar axions, and an enhanced neutrino magnetic moment. Tritium rate is the noncomputable constant 25.0 that represents the expected event rate from natural tritium at the 10^{-20} level in xenon. Neutrino moment is the noncomputable constant 1e-11 that encodes the magnetic-moment strength required if the excess were attributed to neutrino-electron scattering. Upstream definitions include the inflaton potential V(phi_inf) = Jcost(1 + phi_inf) on the recognition manifold and the structural requirements from DomainBootstrap and OptionAEmpiricalProgram that allow these empirical constants to be stated.
proof idea
The term proof first unfolds the definitions of tritium_rate and neutrino_moment, exposing the concrete values 25.0 and 1e-11, then applies norm_num to discharge the resulting numerical inequality.
why it matters
The result supplies one of the key numerical comparisons inside the EA-006 certificate, which concludes that the excess is most likely tritium background and that no BSM physics is required. It realizes the EA-006.10 step in the module's RS assessment, reinforcing the framework preference for natural radioactivity over new-physics mechanisms such as an enhanced neutrino moment. The theorem therefore closes one branch of the three-way comparison (tritium versus axions versus neutrino moment) that the module uses to reach its overall verdict.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.