axion_coupling
plain-language theorem explainer
The axion_coupling definition supplies the fixed numerical value 5 times 10 to the minus 14 for the solar axion-electron coupling g_ae in the XENON1T low-energy excess analysis. Experimental physicists comparing axion hypotheses to tritium backgrounds cite this constant when verifying consistency with CAST limits. It is introduced as a direct constant assignment with no derivation or lemmas.
Claim. Let $g_{ae}$ denote the axion-electron coupling strength for a solar axion origin. Then $g_{ae} = 5 times 10^{-14}$.
background
The module analyzes the XENON1T/nT low-energy electron recoil excess at 2-3 keV, treating solar axions as one of three candidate explanations alongside tritium background and neutrino magnetic moment. The local setting assigns a small coupling value to keep the axion scenario consistent with existing bounds while allowing rate comparisons. The upstream Axion structure defines axions as very light pseudoscalars with mass in the range 10^{-6} to 10^{-3} eV and decay constant in GeV, produced via misalignment.
proof idea
The declaration is a direct constant definition that assigns the real number 5e-14. No lemmas are applied; downstream theorems simply unfold the definition and apply norm_num to obtain the required inequalities.
why it matters
This definition supplies the input value for the theorems axion_coupling_small, axion_viable_not_required, and axion_preferred_over_nu_moment that evaluate whether axions remain viable for the excess. It supports the module verdict that tritium background is most likely while axions are viable but not required. The chosen value lies below the 10^{-13} threshold stated in the module documentation for consistency with CAST constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.