PauliProofSummary
plain-language theorem explainer
PauliProofSummary bundles the antisymmetry implication for fermionic wavefunctions, the explicit s- and p-subshell occupancies, the non-relativistic degeneracy-pressure exponent, and the bounded Chandrasekhar mass into one record. A physicist working on first-principles atomic structure or white-dwarf stability would cite this summary when tracing exclusion back to ledger single-occupancy. The construction is a direct record literal that assembles already-established component lemmas without additional reasoning steps.
Claim. A record asserting: (i) for any antisymmetric map $ψ:α→α→ℂ$, $ψ(a,a)=0$ for all $a$; (ii) the $l=0$ subshell holds 2 states and the $l=1$ subshell holds 6 states; (iii) degeneracy pressure scales as density to the power $5/3$; (iv) the Chandrasekhar mass limit $M$ satisfies $1<M<2$ solar masses.
background
The module derives the Pauli exclusion principle from Recognition Science ledger single-occupancy. Fermions correspond to odd-phase entries under the eight-tick cycle; antisymmetry of the wavefunction then forces $ψ(a,a)=0$, so no two identical fermions share a quantum state. This yields atomic shell structure, degeneracy pressure, and stellar mass limits as direct consequences.
proof idea
The structure is populated by a direct record literal. The core field invokes the antisymmetry lemma pauli_core; the shell fields pull the precomputed values from s_subshell_capacity and p_subshell_capacity; the pressure and Chandrasekhar fields are supplied by the constant definitions degeneracyPressureExponent and chandrasekharLimit.
why it matters
The record is consumed by pauliProofs, which assembles the complete set of Pauli-derived results for the module. It closes the ledger-to-exclusion step in the Recognition Science chain, linking the eight-tick phase accumulation to observable shell capacities and the Chandrasekhar bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.