module module high

`IndisputableMonolith.QFT.PauliExclusion`

The QFT.PauliExclusion module isolates the mathematical core of the Pauli exclusion principle from Recognition Science. It establishes that any antisymmetric two-argument wavefunction vanishes on the diagonal. Researchers deriving fermionic statistics cite this result when applying the 8-tick spin-statistics connection. The argument reduces to a direct substitution into the antisymmetry condition.

claimIf $\psi(a,b)=-\psi(b,a)$ for all $a,b$, then $\psi(a,a)=0$.

background

This module sits inside the QFT tier of Recognition Science derivations and imports the spin-statistics connection. The upstream SpinStatistics module states that fermions obey Fermi-Dirac statistics corresponding to antisymmetric wavefunctions, derived from the 8-tick phase structure. Constants supplies the RS-native time quantum $\tau_0=1$ tick.

The module introduces supporting definitions for quantum states and subshell capacities that realize the exclusion principle in atomic structure. The core theorem is presented as the mathematical heart of Pauli exclusion.

proof idea

The module centers on the pauli_core theorem. The argument is a one-line algebraic substitution: replace the second argument by the first in the antisymmetry relation to obtain $\psi(a,a)=-\psi(a,a)$, hence $\psi(a,a)=0$. Supporting capacity formulas then enumerate the combinatorial consequences for shells and subshells.

why it matters in Recognition Science

The module supplies the Pauli exclusion core to the parent QFT module, which collects Tier 2 derivations. It realizes the fermionic side of the spin-statistics connection that originates from the eight-tick octave. The result closes the direct step from antisymmetry to the exclusion principle inside the Recognition framework.

scope and limits

Does not derive the spin-statistics theorem.
Does not construct explicit multi-particle wavefunctions.
Does not treat bosonic symmetric cases.
Does not connect to experimental observables.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.QFT module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.QFT.SpinStatistics module_import

declarations in this module (33)

theorem pauli_core L48
structure QuantumState L64
def subshellCapacity L85
theorem s_subshell_capacity L88
theorem p_subshell_capacity L91
theorem d_subshell_capacity L94
theorem f_subshell_capacity L97
theorem subshell_capacity_formula L100
def shellCapacity L106
theorem first_shell_capacity L109
theorem second_shell_capacity L112
theorem third_shell_capacity L115
theorem fourth_shell_capacity L118
def nobleGasElectrons L123
theorem helium_electrons L126
theorem neon_electrons L129
theorem argon_electrons L132
theorem shell_filling_pattern L135
def fermiEnergyExponent L144
def degeneracyPressureExponent L147
theorem pressure_energy_relation L150
def chandrasekharLimit L156
theorem chandrasekhar_approx L159
def tovLimit L165
theorem tov_gt_chandrasekhar L168
theorem antisymmetry_implies_exclusion L176
theorem electron_is_fermion L182
theorem fermion_wavefunction_antisymmetric L185
def pauliViolationBound L193
theorem pauli_bound_very_small L196
theorem no_pauli_violation_observed L202
structure PauliProofSummary L216
def pauliProofs L224