pauli_core
plain-language theorem explainer
An antisymmetric complex-valued map on any type must vanish on the diagonal. Condensed-matter and particle physicists cite the fact as the algebraic origin of the Pauli exclusion principle for fermions. The short tactic proof rewrites the antisymmetry hypothesis into 2x = 0 and resolves it via the absence of zero divisors in ℂ together with mul_eq_zero.
Claim. Let a map $ψ : α → α → ℂ$ satisfy $ψ(a,b) = -ψ(b,a)$ for all $a,b$. Then $ψ(a,a) = 0$ for every $a$.
background
The QFT-004 module derives the Pauli exclusion principle from Recognition Science ledger single-occupancy. Fermions correspond to odd-phase ledger entries through the eight-tick cycle, so their wavefunctions must be antisymmetric; ledger balance then forces ψ(a,a) = 0 and single occupancy of each state. The local setting imports the spin-statistics connection and treats the algebraic core as the direct translation of that balance condition.
proof idea
Fix an arbitrary a. The antisymmetry hypothesis yields ψ a a = -ψ a a. Adding both sides and simplifying with ring produces 2 ψ a a = 0. The proof rewrites this via two_mul as (2 : ℂ) * ψ a a = 0, applies mul_eq_zero.mp from IntegersFromLogic, and resolves the left factor with two_ne_zero to conclude ψ a a = 0.
why it matters
The theorem supplies the algebraic heart of the Pauli exclusion principle stated in the module documentation. It is invoked directly by antisymmetry_implies_exclusion and pauliProofs to construct the full exclusion argument and shell-capacity results. Within the Recognition Science chain it closes the step from odd-phase fermions (via the eight-tick octave) to single-occupancy, supporting the PRB paper proposition on first-principles derivation of atomic shell structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.