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

boson_symmetric_wavefunction

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)

 201theorem boson_symmetric_wavefunction (s : Spin) (h : s.isInteger) :
 202    exchangeSymmetryFromSpin s = ExchangeSymmetry.symmetric := by

proof body

Term-mode proof.

 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. -/

depends on (7)

Lean names referenced from this declaration's body.