Foundation Spin Statistics Exchange Sign Fermion

The exchange sign

The exchange sign is a rule of quantum mechanics that governs what happens when two identical particles are swapped. If the sign stays the same, the particles are bosons, and many can occupy one state, which is how lasers work. If the sign becomes negative, the particles are fermions, and no two can share a state, which is why atoms have structure and why matter does not collapse. In the standard account, this spin-statistics connection is a deep theorem of relativistic quantum field theory, proved by Wolfgang Pauli in 1940.

Recognition Science (RS) offers a different route to the same conclusion. Its framework models physical states as entries in a ledger, a discrete record of events, and assigns each kind of particle a period: the number of ticks in its minimal recognition cycle. A fermion is defined as a state whose cycle completes in 4 ticks, half of the fundamental 8-tick period. The framework's library of machine-checked formal theorems then proves that a 4-tick state acquires a phase of -1 under a full 2π rotation, and it identifies the exchange sign with that rotation phase. The declaration exchange_sign_fermion is the theorem that states this result: the rotation phase for a fermion is -1.

This is a formal proof, not a numerical estimate. The theorem is checked by a computer, and it relies on the framework's own definitions of rotation and phase, not on the apparatus of quantum field theory. The framework's library derives the result from its eight-tick cycle, and it certifies that no hypotheses remain in the chain. The Pauli exclusion principle, the rule that no two identical fermions can occupy the same state, follows as a corollary: if a state's amplitude equals its own negative, the amplitude must be zero.

What the declaration does not do is prove the spin-statistics theorem in the sense of standard physics. It does not start from the axioms of relativistic quantum field theory, and it does not engage with the known exceptions, such as anyons, which are quasiparticles in two dimensions that can have any exchange phase. The framework's result is a derivation within its own model, and its connection to the measured world is a separate question. The theorem establishes a mathematical fact about the framework's own definitions, and the framework's claim is that this fact corresponds to the physical one.

/-- A ledger state is fermionic (spin-1/2) if its minimal recognition cycle
    completes in 4 ticks (half the 8-tick period). -/
def IsFermionic (period : ℕ) : Prop := period = 4

/-- Two-particle exchange involves one 2π rotation of the relative coordinate,
    contributing the rotation phase. For fermions: -1. For bosons: +1.

    This is the fundamental RS derivation of the exchange sign. -/
theorem exchange_sign_fermion :
    rotationPhase 4 = -1 := fermion_rotation_phase_neg_one

/-- **PAULI EXCLUSION**:
    If two identical fermions occupy the same state, the antisymmetric
    two-particle amplitude must vanish.

    In RS: if ψ₁ = ψ₂ = ψ, then exchange gives ψ → -ψ (from exchange_sign_fermion),
    but exchange of identical particles gives ψ → ψ.
    So ψ = -ψ → ψ = 0. -/
theorem pauli_exclusion (ψ : ℂ) (h_fermion : ψ = rotationPhase 4 * ψ) :
    ψ = 0 := by
  rw [fermion_rotation_phase_neg_one] at h_fermion
  -- h_fermion : ψ = -1 * ψ, so 2ψ = 0, so ψ = 0
  have h2 : (2 : ℂ) * ψ = 0 := by linear_combination ψ + h_fermion
  exact (mul_eq_zero.mp h2).resolve_left two_ne_zero

What this page does not claim

This does not prove the spin-statistics theorem from the axioms of relativistic quantum field theory. This does not claim the framework's derivation is the only or the original proof of the exchange sign. This does not address the physical mechanism by which discrete recognition cycles correspond to continuous rotations.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/SpinStatistics.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: