pith. machine review for the scientific record. sign in
def definition def or abbrev

thetaContributions

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  83def thetaContributions : List String := [

proof body

Definition body.

  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
  93    Introduce a new U(1)_PQ symmetry.
  94    When broken, a Goldstone boson (axion) appears.
  95    The axion field dynamically relaxes θ → 0.
  96
  97    Axion mass: m_a ~ f_π m_π / f_a
  98    where f_a is the PQ breaking scale. -/

depends on (12)

Lean names referenced from this declaration's body.