pauli_exclusion_simple
plain-language theorem explainer
The theorem shows that any complex amplitude ψ satisfying ψ = -ψ must be zero, giving an algebraic core for the Pauli exclusion principle inside the Recognition Science spin-statistics development. Workers deriving fermionic antisymmetry from the eight-tick ledger would cite it as an immediate corollary. The proof obtains 2ψ = 0 by linear combination and applies the no-zero-divisors property to discard the factor 2.
Claim. Let ψ ∈ ℂ. If ψ = −ψ, then ψ = 0.
background
The module derives the full spin-statistics theorem from the eight-tick ledger structure. Fermions (4-tick states) acquire a minus sign under 2π rotation, forcing antisymmetry under exchange; the simplified exclusion follows at once for the amplitude. Upstream, the mul_eq_zero result from IntegersFromLogic states that a * b = 0 implies a = 0 or b = 0, forced by the ring isomorphism with the integers.
proof idea
A linear_combination tactic applied to the hypothesis ψ = −ψ produces the auxiliary equation 2ψ = 0. The mul_eq_zero lemma then splits the product; the case 2 = 0 is ruled out by two_ne_zero, leaving ψ = 0.
why it matters
The result supplies the basic algebraic step for the pauli_exclusion corollary listed in the module doc-comment and in the paper RS_Spin_Statistics_Theorem.tex. It realizes the T7 eight-tick octave implication that a phase of −1 under exchange excludes identical fermions. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.