pith. machine review for the scientific record. sign in
theorem proved term proof

spin_statistics_theorem

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)

  75theorem spin_statistics_theorem :
  76    -- Fermions antisymmetrize under exchange
  77    (rotationPhase 4 = -1) ∧
  78    -- Bosons symmetrize under exchange
  79    (phaseExp ⟨0, by norm_num⟩ = 1) :=

proof body

Term-mode proof.

  80  spin_statistics_key
  81
  82/-! ## Pauli Exclusion Principle -/
  83
  84/-- **PAULI EXCLUSION**:
  85    If two identical fermions occupy the same state, the antisymmetric
  86    two-particle amplitude must vanish.
  87
  88    In RS: if ψ₁ = ψ₂ = ψ, then exchange gives ψ → -ψ (from exchange_sign_fermion),
  89    but exchange of identical particles gives ψ → ψ.
  90    So ψ = -ψ → ψ = 0. -/

depends on (15)

Lean names referenced from this declaration's body.