moment_requires_bsm
plain-language theorem explainer
The theorem shows that the neutrino magnetic moment needed to account for the XENON1T low-energy excess exceeds the standard-model expectation by eight orders of magnitude. Analysts of xenon recoil data would cite it when weighing a neutrino-magnetic-moment explanation against tritium background. The proof is a one-line wrapper that unfolds the two moment definitions and applies numerical normalization.
Claim. The neutrino magnetic moment required by a neutrino-origin hypothesis satisfies $10^{-11} > 10^{-19}$ (in Bohr magnetons), so any such explanation demands physics beyond the standard model.
background
In the XENON1T/nT module the neutrino magnetic moment is introduced as the value $10^{-11}$ Bohr magnetons that would be needed to produce the observed 2-3 keV electron-recoil excess via enhanced neutrino-electron scattering. Its standard-model counterpart is defined as $10^{-19}$ Bohr magnetons, the negligible value predicted by the standard model. The surrounding analysis compares three candidate sources for the excess: tritium beta decay at natural concentrations, solar axions, and this enhanced neutrino moment, with the module concluding that tritium fits the rate and spectrum with the least new physics.
proof idea
The term proof unfolds the two real-valued definitions neutrino_moment and neutrino_moment_sm, then invokes norm_num to compare the concrete literals 1e-11 and 1e-19 directly.
why it matters
The result supplies the quantitative step behind theorem EA-006.9 and feeds the module verdict that a neutrino origin is disfavored relative to tritium. It reinforces the Recognition Science preference for explanations that avoid large beyond-standard-model enhancements when the data are compatible with known backgrounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.