neutronEDM
plain-language theorem explainer
The neutron electric dipole moment is defined to scale linearly with the QCD theta parameter as d_n = θ × 10^{-16} e·cm. Particle physicists addressing the strong CP problem cite this scaling to convert the experimental bound d_n < 3×10^{-26} e·cm into |θ| < 3×10^{-10}. The definition is a direct one-line encoding of the standard phenomenological relation without deriving the prefactor.
Claim. $d_n(θ) = θ × 10^{-16} e·cm$
background
The StandardModel.StrongCP module frames the strong CP problem via the QCD Lagrangian term θ (g²/32π²) G_μν G̃^μν, where θ ranges over [0, 2π) yet must satisfy |θ| < 10^{-10} experimentally. Recognition Science resolves this via 8-tick symmetry, which imposes discrete phase constraints (multiples of π/4) and selects θ = 0 through J-cost minimization. The module imports EightTick to supply the underlying octave structure and draws on upstream results such as PhiForcingDerived.of for J-cost calibration and SpectralEmergence.of for the SU(3) gauge sector.
proof idea
This is a one-line definition that directly encodes the phenomenological scaling d_n ≈ θ × 10^{-16} e·cm taken from standard QCD literature.
why it matters
The definition supplies the conversion factor that turns the theoretical θ into a measurable quantity, enabling the fine-tuning discussion in the module. It supports the 8-tick symmetry mechanism that forces θ = 0 and connects to sibling declarations such as theta_finetuning and theta_zero_selected that quantify the improbability of small θ by chance. The module documentation cites this scaling to derive the experimental limit |θ| < 3 × 10^{-10}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.