module module

`IndisputableMonolith.QFT.PauliExclusion`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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