moment_exceeds_sm
plain-language theorem explainer
The theorem shows that the neutrino magnetic moment required to account for the XENON1T low-energy excess exceeds the Standard Model prediction by more than seven orders of magnitude. Analysts of recoil data cite this bound when weighing whether the excess demands beyond-Standard-Model neutrino properties. The proof reduces directly to the ratio of two explicit constants via unfolding and numerical normalization.
Claim. $μ_ν / μ_ν^{SM} > 10^7$, where $μ_ν$ denotes the magnetic moment needed if the excess arises from neutrino-electron scattering and $μ_ν^{SM}$ is the Standard Model expectation.
background
The XENON1T/nT module examines the 2-3 keV electron recoil excess under three hypotheses: tritium background, solar axions, or an enhanced neutrino magnetic moment. The required moment is defined as $10^{-11} μ_B$ under the neutrino-origin assumption, while the Standard Model value is fixed at $10^{-19} μ_B$. Upstream results supply the discrete φ-tier structure for nuclear densities and the J-cost calibration that anchors the numerical constants used here.
proof idea
The term proof unfolds the two moment definitions to expose the literals 1e-11 and 1e-19, then applies norm_num to confirm their ratio exceeds 1e7.
why it matters
This bound supplies one of the quantitative inputs to the EA-006 certificate, which concludes that the excess is most likely tritium background rather than new physics. It quantifies the enhancement that would be required under the magnetic-moment hypothesis and thereby supports the Recognition Science verdict that no BSM neutrino properties are mandated by the data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.