fermion_antisymmetric_wavefunction

formal source

 193  else ExchangeSymmetry.symmetric
 194
 195/-- **THEOREM**: Fermions have antisymmetric wavefunctions. -/
 196theorem fermion_antisymmetric_wavefunction (s : Spin) (h : s.isHalfInteger) :
 197    exchangeSymmetryFromSpin s = ExchangeSymmetry.antisymmetric := by
 198  simp [exchangeSymmetryFromSpin, h]
 199
 200/-- **THEOREM**: Bosons have symmetric wavefunctions. -/
 201theorem boson_symmetric_wavefunction (s : Spin) (h : s.isInteger) :
 202    exchangeSymmetryFromSpin s = ExchangeSymmetry.symmetric := by
 203  simp [exchangeSymmetryFromSpin]
 204  intro h'
 205  exact absurd (And.intro h h') (Spin.int_half_exclusive s)
 206
 207/-! ## Pauli Exclusion Principle -/
 208
 209/-- **THEOREM (Pauli Exclusion)**: Fermions cannot occupy the same quantum state.
 210
 211    This follows from antisymmetry: if two fermions are in the same state,
 212    the wavefunction ψ(1,1) = -ψ(1,1), which implies ψ(1,1) = 0.
 213
 214    Proof: From x = -x, add x to both sides: 2x = 0. Since char(ℂ) = 0, we have x = 0. -/
 215theorem pauli_exclusion :
 216    ∀ (state : Type*) (ψ : state → state → ℂ),
 217    (∀ a b, ψ a b = -(ψ b a)) → (∀ a, ψ a a = 0) := by
 218  intro state ψ antisym a
 219  have heq : ψ a a = -(ψ a a) := antisym a a
 220  -- x = -x in ℂ implies x = 0 (since char ℂ = 0)
 221  -- Algebraic proof: x = -x → x - x = -x - x → 0 = -2x → x = 0
 222  have h2 : (2 : ℂ) ≠ 0 := two_ne_zero
 223  -- ψ + ψ = ψ + (-ψ) = 0
 224  have hsum : ψ a a + ψ a a = 0 := by
 225    nth_rewrite 2 [heq]
 226    exact add_neg_cancel (ψ a a)