axion_coupling_small
plain-language theorem explainer
Recognition Science bounds the solar axion-electron coupling below 10^{-13} to stay compatible with CAST limits. Experimentalists assessing the XENON1T low-energy excess would cite this bound when weighing axion contributions against tritium backgrounds. The proof is a one-line wrapper that unfolds the fixed coupling value and discharges the numerical comparison.
Claim. $g_{ae} < 10^{-13}$
background
The XENON1T/nT module defines axion_coupling as the fixed real 5e-14, representing the solar axion-electron coupling strength under the axion-origin hypothesis for the 2-3 keV recoil excess. This value is selected to lie below CAST upper limits while remaining potentially detectable in the observed rate window. The module contrasts three explanations: tritium background at natural levels, solar axions via Primakoff-like processes, and enhanced neutrino magnetic moments. Upstream, the Axion structure from Cosmology.DarkMatter supplies the light pseudoscalar with mass and decay-constant parameters that enter the coupling definition.
proof idea
The proof is a one-line wrapper. It unfolds axion_coupling to expose the concrete value 5e-14, then applies norm_num to verify the inequality 5e-14 < 1e-13.
why it matters
The result populates the EA-006.6 slot and feeds directly into the ea006_certificate, which states that the excess is most likely tritium background and that axions remain possible but not required when g_ae stays below 10^{-13}. It reinforces the module verdict that minimal BSM physics suffices, consistent with Recognition Science's preference for the tritium fit over new-physics alternatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.