module module high

`IndisputableMonolith.QFT.PauliExclusion`

The PauliExclusion module states the core mathematical fact underlying the Pauli exclusion principle for fermions in the Recognition Science QFT setting. Atomic physicists and QFT modelers cite it when linking antisymmetric wavefunctions to zero occupancy at identical states. The argument is a one-line substitution of a = b into the given antisymmetry condition.

claimIf a wavefunction satisfies $ψ(a,b) = -ψ(b,a)$ for all states $a,b$, then $ψ(a,a) = 0$.

background

The module sits inside the QFT derivations and imports the 8-tick phase structure that produces the spin-statistics link: fermions are tied to antisymmetric wavefunctions. It also draws on the base time quantum τ₀ = 1 tick. Sibling definitions introduce QuantumState together with explicit formulas for s, p, d, f subshell capacities and the first three shell capacities.

proof idea

The central theorem is obtained by direct substitution a = b into the antisymmetry hypothesis. The remaining declarations supply closed-form expressions for subshell and shell occupancies that follow from the exclusion rule.

why it matters in Recognition Science

The module supplies the exclusion principle to the parent QFT module, bridging the spin-statistics result (derived from the eight-tick octave) to concrete atomic structure. It completes one Tier 2 derivation step listed in the QFT module documentation.

scope and limits

Does not derive the spin-statistics theorem.
Does not treat bosonic symmetric states.
Does not include interaction terms or relativistic corrections.

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