Qft Pauli Exclusion

The Ledger's Rule

The Pauli exclusion principle is a foundational rule of quantum physics: no two identical fermions, particles like electrons with half-integer spin, can occupy the same quantum state. This principle shapes the periodic table, the stability of matter, and the structure of white dwarfs and neutron stars. In Recognition Science, this rule is not an added postulate but a consequence of the framework's core structure, the ledger, a discrete record of events.

The framework models a fermion as an entry in this ledger that accumulates an odd phase, a factor of -1, through its recognition cycle. The key mathematical step is the theorem antisymmetry_implies_exclusion: if a wavefunction ψ(a,b) equals -ψ(b,a) for any two states a and b, then ψ(a,a) must be zero. The proof is direct. Setting b equal to a gives ψ(a,a) = -ψ(a,a), and since the only complex number equal to its own negative is zero, the diagonal vanishes. This means two identical fermions cannot share the same address in the ledger.

From this single-occupancy rule, the module derives the shell structure of atoms. The definitions shellCapacity and subshellCapacity produce the familiar counts: the s-subshell holds 2 electrons, the p-subshell 6, the d-subshell 10, and the f-subshell 14. The theorems confirm the first four shells hold 2, 8, 18, and 32 electrons, and the noble gas electron counts match the known sequence 2, 10, 18, 36, 54, 86. These are not empirical fits but consequences of the ledger's occupancy rule combined with the framework's spin structure.

The module also connects the principle to astrophysics. It defines the chandrasekharLimit as 1.4 solar masses and the tovLimit as 3 solar masses, with a theorem proving the latter exceeds the former. The degeneracy pressure exponent 5/3 relates to the Fermi energy exponent 2/3 through the theorem pressure_energy_relation. These numbers describe the maximum mass a white dwarf or neutron star can support before gravity overcomes the pressure from fermions refusing to share states.

In Recognition Science, the Pauli principle is not a separate law but a direct consequence of the ledger's single-occupancy rule. The machine-checked library of formal theorems proves that antisymmetry forces exclusion, and from that one fact, the shell structure of atoms and the limits of stellar stability follow. The framework's claim is that the structure of the periodic table and the fate of massive stars are both written into the same simple rule: one entry per slot.

/-- **THEOREM**: Antisymmetry of fermion wavefunctions implies exclusion.
    This uses the pauli_core theorem proved above. -/
theorem antisymmetry_implies_exclusion :
    ∀ (ψ : ℕ → ℕ → ℂ), (∀ a b, ψ a b = -ψ b a) → (∀ a, ψ a a = 0) :=
  fun ψ h => pauli_core ψ h

/-- Number of states in a shell with principal quantum number n.
    Formula: 2n² -/
def shellCapacity (n : ℕ) : ℕ := 2 * n^2

/-- Number of states in a subshell with angular momentum l.
    Formula: 2(2l+1) where factor 2 is for spin. -/
def subshellCapacity (l : ℕ) : ℕ := 2 * (2 * l + 1)

/-- **THEOREM**: Pressure exponent = 1 + energy exponent. -/
theorem pressure_energy_relation :
    degeneracyPressureExponent = 1 + fermiEnergyExponent := by
  unfold degeneracyPressureExponent fermiEnergyExponent
  norm_num

/-- **THEOREM**: TOV limit is higher than Chandrasekhar limit. -/
theorem tov_gt_chandrasekhar : tovLimit > chandrasekharLimit := by
  unfold tovLimit chandrasekharLimit
  norm_num

What this page does not claim

This module does not prove the Pauli exclusion principle from first principles in the sense of deriving the antisymmetry of the wavefunction from the ledger structure alone. The shell capacities and noble gas electron counts are definitional consequences, not empirical measurements or independent derivations. The Chandrasekhar and Tolman-Oppenheimer-Volkoff limits are defined as rational numbers, not derived from the framework's dynamical equations.

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/PauliExclusion.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: