neutronEDM

formal source

  59
  60    Experimental limit: d_n < 3 × 10⁻²⁶ e·cm
  61    Therefore: |θ| < 3 × 10⁻¹⁰ -/
  62noncomputable def neutronEDM (θ : ℝ) : ℝ := θ * 1e-16  -- e·cm
  63
  64/-! ## The Fine-Tuning Problem -/
  65
  66/-- Why is θ ≈ 0?
  67
  68    θ could be any value in [0, 2π).
  69    Probability of |θ| < 10⁻¹⁰ by chance: ~ 10⁻¹¹
  70
  71    This seems extremely fine-tuned! -/
  72theorem theta_finetuning :
  73    -- P(|θ| < 10⁻¹⁰) ~ 10⁻¹¹ by chance
  74    True := trivial
  75
  76/-- The θ term is a "topological" term:
  77    It counts instanton number.
  78    Each instanton adds Δθ = 2π to the phase.
  79
  80    θ is the sum of:
  81    - Bare QCD θ
  82    - Contribution from quark masses (arg det M) -/
  83def thetaContributions : List String := [
  84  "Bare QCD theta",
  85  "Quark mass phase: arg det M_q",
  86  "Total: θ_eff = θ_QCD + arg det M_q"
  87]
  88
  89/-! ## The Axion Solution -/
  90
  91/-- The Peccei-Quinn (PQ) solution:
  92