QuantumState
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not derive the exclusion principle or antisymmetry constraint.
- Does not encode the radial wave function or energy spectrum.
- Does not treat multi-electron interactions or relativistic corrections.
- Does not specify the full Hilbert-space inner product.
formal statement (Lean)
64structure QuantumState where
65 /-- Principal quantum number (energy level). -/
66 n : ℕ
67 /-- Orbital angular momentum quantum number. -/
68 l : ℕ
69 /-- Magnetic quantum number. -/
70 m : ℤ
71 /-- Spin projection (±1 representing ±1/2). -/
72 ms : Int
73 /-- Validity: l < n. -/
74 l_lt_n : l < n
75 /-- Validity: |m| ≤ l. -/
76 m_bound : m.natAbs ≤ l
77 /-- Validity: ms = ±1. -/
78 ms_valid : ms = 1 ∨ ms = -1
79deriving DecidableEq
80
81/-! ## Atomic Shell Structure -/
82
83/-- Number of states in a subshell with angular momentum l.
84 Formula: 2(2l+1) where factor 2 is for spin. -/
used by (24)
-
born_rule_jcost_connection -
expectedCost -
probability -
prob_nonneg -
prob_sum_one -
QuantumState -
CloningMachine -
innerProduct -
inner_product_self -
QuantumState -
QuantumState -
unitary_preserves_norm -
born_rule_nonneg -
born_rule_normalized -
cost_probability_relation -
filter_map_weight_sum -
isDefinite -
isSuperposition -
measurement_postulate_derived -
measurementProbability -
outcomeCost -
probability_equals_weight -
QuantumState -
stateToLedger