pauliProofs
plain-language theorem explainer
The pauliProofs definition assembles a complete record of Pauli exclusion consequences from the ledger antisymmetry constraint. Researchers deriving atomic shell structure or white-dwarf stability from first principles would reference this summary when citing the full chain from antisymmetry to the Chandrasekhar bound. It is constructed as a record literal that directly references the core antisymmetry theorem together with the explicit capacity and limit lemmas.
Claim. Let $ψ:α→α→ℂ$ satisfy $ψ(a,b)=-ψ(b,a)$ for all $a,b$. The summary record asserts $ψ(a,a)=0$ for all $a$, the subshell capacities $2$ for $l=0$ and $6$ for $l=1$, the degeneracy pressure scaling $P∝n^{5/3}$, and the Chandrasekhar limit bounds $1<M<2$ in solar masses.
background
In the QFT-004 module the Pauli exclusion principle is obtained from ledger single-occupancy: fermions correspond to odd-phase entries in the eight-tick cycle, so that the ledger balance condition forces antisymmetry of the two-particle wavefunction. The core mathematical step is the theorem that any antisymmetric function vanishes on the diagonal. Subshell capacities follow from the angular-momentum degeneracy in the recognition ladder, while the pressure exponent and Chandrasekhar bound are recovered by standard thermodynamic arguments once single occupancy is enforced.
proof idea
The definition is a one-line record constructor that supplies the core field by applying the pauli_core theorem to the supplied antisymmetry hypothesis, then directly inserts the already-proven s_subshell_capacity, p_subshell_capacity, and chandrasekhar_approx lemmas into the remaining fields.
why it matters
This definition packages the entire set of Pauli-derived results so that downstream work on atomic structure or stellar stability can cite a single object. It completes the ledger-to-exclusion step in the Recognition Science chain and directly supports the paper proposition on first-principles derivation of atomic shell structure. The construction relies on the eight-tick octave for the odd-phase fermion identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.