Qft Spin Statistics

The spin-statistics connection

The spin-statistics theorem is a fundamental result of quantum physics. It says that particles with half-integer spin, such as electrons, obey Fermi-Dirac statistics: their wavefunction is antisymmetric, meaning two such particles cannot occupy the same quantum state. Particles with integer spin, such as photons, obey Bose-Einstein statistics: their wavefunction is symmetric, and they can crowd into the same state. This distinction explains the structure of atoms, the behavior of lasers, and the stability of matter.

The classical proof of this theorem, due to Wolfgang Pauli in 1940, relies on relativistic quantum field theory and causality. It is a deep result that took decades to establish rigorously. The Recognition Science framework offers a different route: it derives the same connection from a discrete eight-tick cycle. In this account, a full rotation by 2π corresponds to traversing all eight ticks. A particle with half-integer spin needs two cycles, or sixteen ticks, to return to its original phase, accumulating a factor of -1. A particle with integer spin needs only one cycle, accumulating a factor of +1.

In Recognition Science, the framework models this phase accumulation explicitly. It defines a spin value, a cycle phase, and a phase per tick. The central theorems are simple and exact: for a half-integer spin particle, the cycle phase is -1; for an integer spin particle, it is +1. From these phase factors, the framework derives the exchange symmetry: half-integer spin particles have antisymmetric wavefunctions, and integer spin particles have symmetric ones. It also proves the Pauli exclusion principle as a direct consequence: if a wavefunction is antisymmetric, then a particle cannot be in the same state as itself, because that would require ψ(a,a) = -ψ(a,a), which forces ψ(a,a) = 0.

This is a formal derivation within the framework's machine-checked library of formal theorems. The library proves that the phase for the fourth tick is -1 and the phase for the zeroth tick is +1, and that the sum of all eight phases is zero, which the framework interprets as a vacuum fluctuation cancellation. The framework also defines ledger entries for bosons and fermions, recording the accumulated phase and its value. These structures and theorems are all in the module IndisputableMonolith/QFT/SpinStatistics.lean.

What this means in plain language is that the framework offers a discrete, combinatorial origin for a fundamental quantum fact. Instead of starting from continuous fields and causality, it starts from a cycle of eight ticks and derives the same statistical behavior. This is a derivation, not a measurement: it does not prove that the physical world works this way, but it shows that a simple discrete structure can produce the observed spin-statistics connection. The framework's claim is that this is not a coincidence, but a consequence of the same forcing chain that produces other fundamental constants.

/-- **THEOREM (Fermion Phase)**: Half-integer spin particles acquire a minus sign
    under the full 8-tick cycle (2π rotation). -/
theorem fermion_antisymmetric (s : Spin) (h : s.isHalfInteger) :
    cyclePhase s = -1 := by
  unfold cyclePhase Spin.value Spin.isHalfInteger at *
  -- s.twice is odd, so s.twice % 2 = 1
  have hodd : s.twice % 2 = 1 := h
  -- Get k such that s.twice = 2k + 1
  have ⟨k, hk⟩ := Int.odd_iff.mpr hodd
  -- The phase is exp(2πi × (twice/2)) = exp(πi × twice)
  have h_rewrite : 2 * π * I * (s.twice / 2 : ℝ) = π * I * s.twice := by
    push_cast; ring
  rw [h_rewrite, hk]
  push_cast
  -- exp(πi × (2k+1)) = exp(2kπi) × exp(πi) = 1 × (-1) = -1
  have h_split : π * I * (2 * k + 1) = (k : ℂ) * (2 * π * I) + π * I := by ring
  rw [h_split, Complex.exp_add, Complex.exp_int_mul_two_pi_mul_I, one_mul, Complex.exp_pi_mul_I]

/-- **THEOREM (Boson Phase)**: Integer spin particles acquire +1
    under the full 8-tick cycle (2π rotation). -/
theorem boson_symmetric (s : Spin) (h : s.isInteger) :
    cyclePhase s = 1 := by
  unfold cyclePhase Spin.value Spin.isInteger at *
  -- s.twice is even, so s.twice % 2 = 0
  have heven : s.twice % 2 = 0 := h
  -- Get k such that s.twice = 2k
  have ⟨k, hk⟩ := Int.even_iff.mpr heven
  -- The phase is exp(2πi × (twice/2)) = exp(2πi × k) = 1
  have h_rewrite : 2 * π * I * (s.twice / 2 : ℝ) = (k : ℂ) * (2 * π * I) := by
    rw [hk]
    push_cast
    ring
  rw [h_rewrite, Complex.exp_int_mul_two_pi_mul_I]

/-- **THEOREM**: Fermions have antisymmetric wavefunctions. -/
theorem fermion_antisymmetric_wavefunction (s : Spin) (h : s.isHalfInteger) :
    exchangeSymmetryFromSpin s = ExchangeSymmetry.antisymmetric := by
  simp [exchangeSymmetryFromSpin, h]

/-- **THEOREM**: Bosons have symmetric wavefunctions. -/
theorem boson_symmetric_wavefunction (s : Spin) (h : s.isInteger) :
    exchangeSymmetryFromSpin s = ExchangeSymmetry.symmetric := by
  simp [exchangeSymmetryFromSpin]
  intro h'
  exact absurd (And.intro h h') (Spin.int_half_exclusive s)

/-- **THEOREM (Pauli Exclusion)**: Fermions cannot occupy the same quantum state.

    This follows from antisymmetry: if two fermions are in the same state,
    the wavefunction ψ(1,1) = -ψ(1,1), which implies ψ(1,1) = 0.

    Proof: From x = -x, add x to both sides: 2x = 0. Since char(ℂ) = 0, we have x = 0. -/
theorem pauli_exclusion :
    ∀ (state : Type*) (ψ : state → state → ℂ),
    (∀ a b, ψ a b = -(ψ b a)) → (∀ a, ψ a a = 0) := by
  intro state ψ antisym a
  have heq : ψ a a = -(ψ a a) := antisym a a
  -- x = -x in ℂ implies x = 0 (since char ℂ = 0)
  -- Algebraic proof: x = -x → x - x = -x - x → 0 = -2x → x = 0
  have h2 : (2 : ℂ) ≠ 0 := two_ne_zero
  -- ψ + ψ = ψ + (-ψ) = 0
  have hsum : ψ a a + ψ a a = 0 := by
    nth_rewrite 2 [heq]
    exact add_neg_cancel (ψ a a)
  have h2x : (2 : ℂ) * ψ a a = 0 := by rw [two_mul]; exact hsum
  exact (mul_eq_zero.mp h2x).resolve_left h2

/-- **FOUNDATION CONNECTION**: The fermion phase (-1) derives from the
    Foundation's 8-tick structure at tick k=4.

    This explicitly connects the spin-statistics theorem to the proven
    phase_4_is_minus_one theorem in Foundation.EightTick. -/
theorem fermion_phase_from_foundation :
    Foundation.EightTick.phaseExp ⟨4, by norm_num⟩ = -1 :=
  Foundation.EightTick.phase_4_is_minus_one

/-- **FOUNDATION CONNECTION**: The boson phase (+1) derives from the
    Foundation's 8-tick structure at tick k=0.

    This explicitly connects the spin-statistics theorem to the proven
    phase_0_is_one theorem in Foundation.EightTick. -/
theorem boson_phase_from_foundation :
    Foundation.EightTick.phaseExp ⟨0, by norm_num⟩ = 1 :=
  Foundation.EightTick.phase_0_is_one

/-- **FOUNDATION CONNECTION**: The sum of all 8 phases is zero, which
    underlies vacuum fluctuation cancellation.

    This is proven in Foundation.EightTick.sum_8_phases_eq_zero. -/
theorem vacuum_fluctuation_cancellation :
    ∑ k : Fin 8, Foundation.EightTick.phaseExp k = 0 :=
  Foundation.EightTick.sum_8_phases_eq_zero

What this page does not claim

This module does not prove that the physical world is discrete; it derives a mathematical consequence from a chosen model. The spin-statistics theorem is not derived from the full forcing chain of Recognition Science; it is a standalone module using the eight-tick structure. The framework does not claim to replace relativistic quantum field theory; it offers an alternative derivation of the same result.

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/QFT/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: