pauli_exclusion
plain-language theorem explainer
The theorem shows that any complex amplitude ψ satisfying ψ equals the 4-tick rotation phase times itself must vanish, which encodes the Pauli exclusion principle for identical fermions in Recognition Science. Researchers deriving spin-statistics relations from the eight-tick ledger would cite this when connecting rotation phases to wavefunction antisymmetry. The tactic proof substitutes the explicit fermion phase value of negative one, forms the equation 2ψ = 0 by linear combination, and invokes the absence of zero divisors in the logic ring.
Claim. Let $ψ ∈ ℂ$ satisfy $ψ = ρ_4 ψ$, where $ρ_4$ is the phase factor acquired by a 4-tick fermion state under a $2π$ rotation. Then $ψ = 0$.
background
This declaration belongs to the SpinStatistics module, which derives the full spin-statistics connection from the RS eight-tick structure. The rotationPhase definition computes the phase accumulated under a $2π$ rotation for a given tick period via phaseExp on the residue class modulo 8. The companion result fermion_rotation_phase_neg_one establishes that this phase equals -1 precisely when the period is 4, corresponding to spin-1/2 fermions.
proof idea
The tactic proof begins by rewriting the hypothesis with fermion_rotation_phase_neg_one to replace rotationPhase 4 by -1, yielding ψ = -ψ. It then applies linear_combination to obtain the auxiliary equation 2ψ = 0. Finally it invokes mul_eq_zero from IntegersFromLogic, which states that the logic integers have no zero divisors, and resolves the left factor 2 ≠ 0 to conclude ψ = 0.
why it matters
The result supplies the concrete Pauli exclusion corollary inside the Recognition Science spin-statistics theorem, which the module lists as one of its four key outcomes. It is used directly by the corresponding statement in the QFT.SpinStatistics module. The argument rests on the eight-tick octave (T7) and the forced phase -1 for 4-tick rotations that enforces antisymmetry under particle exchange, thereby linking the foundational ledger to observable fermionic statistics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.