QuantumState
plain-language theorem explainer
A quantum state is specified by the tuple of quantum numbers n, l, m, ms together with the bounds l < n, |m| <= l and ms = pm 1. Atomic-structure calculations inside the Recognition Science ledger framework cite this type to label single-occupancy fermion slots before invoking antisymmetry. The declaration is a plain structure definition whose fields embed the standard selection rules.
Claim. A quantum state is a 4-tuple $(n,l,m,m_s)$ with $n,l$ natural numbers, $m$ integer and $m_s=pm1$ satisfying $l<n$ and $|m|leq l$.
background
The QFT.PauliExclusion module derives the exclusion principle from ledger single-occupancy: fermions carry odd phase through the 8-tick cycle, so two identical entries at the same address force the ledger amplitude to vanish. The structure packages the usual atomic labels with their validity predicates. Upstream, QuantumLedger.QuantumState defines a general superposition over ledger configurations with complex amplitudes and normalization |psi|^2=1; the present structure supplies the concrete atomic address used inside that ledger.
proof idea
Structure definition that directly records the four quantum numbers and the three validity predicates as fields. No lemmas or tactics are invoked; the declaration is the type itself.
why it matters
The type supplies the atomic labels required by downstream shell-capacity theorems and by the Born-rule connection in QuantumLedger. It realizes the module target of a first-principles derivation of atomic shell structure from ledger antisymmetry, linking to the eight-tick fermion phase and the J-cost variational principle. It leaves open the explicit construction of degeneracy pressure in white dwarfs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.