shellCapacity
The shellCapacity definition maps shell index n to electron capacity via the explicit sequence 2, 8, 8, 18, 18, 32, 32 for n = 0 onward. Periodic table certificates in the Recognition Science framework cite it to verify noble-gas closures under eight-window neutrality. The definition is realized by exhaustive pattern matching on the input natural number with a default continuation clause.
claimDefine the function shellCapacity : ℕ → ℕ by the cases shellCapacity(0) = 2, shellCapacity(1) = 8, shellCapacity(2) = 8, shellCapacity(3) = 18, shellCapacity(4) = 18, shellCapacity(5) = 32, shellCapacity(6) = 32, and shellCapacity(n) = 32 for all n ≥ 7. This yields the sequence of maximum electrons per principal shell that aligns with the eight-tick ledger balance.
background
The module supplies a zero-parameter periodic table engine built on the eight-tick octave and block offsets (s/p/d/f) from Recognition Science. Shell capacities are the deterministic counts forced by angular momentum quantization derived from ledger packing constraints, with noble gases identified exactly at cumulative 8-window neutrality points. Upstream, PeriodicBlocks.shell scales energy as E_coh times block capacity, while the sibling shellCapacity definitions in PeriodicTableFromPhiLadder and PauliExclusion supply the closed form 2n². The local setting is the Noble Gas Closure Theorem (P0-A0), which treats the listed sequence as the chemical manifestation of the fundamental RS scheduler.
proof idea
The declaration is a direct definition by pattern matching on the natural number argument. Cases are enumerated explicitly for n = 0 through 6, with a default clause returning 32 for all larger inputs. No lemmas or tactics are invoked; the body is the base data structure itself.
why it matters in Recognition Science
This definition supplies the concrete capacities required by PeriodicTableCert to certify five blocks and the specific equalities s1_cap : shellCapacity 1 = 2, s2_cap : shellCapacity 2 = 8, s3_cap : shellCapacity 3 = 18, s4_cap : shellCapacity 4 = 32. It realizes the deterministic sequence forced by the 8-tick neutrality condition and supports the prediction that the noble-gas atomic numbers {2, 10, 18, 36, 54, 86} arise without parameter fitting. The entry closes the interface between the phi-ladder ledger and observable chemistry.
scope and limits
- Does not derive capacities from the J-cost function or phi-ladder.
- Does not compute cumulative electron counts or period assignments.
- Does not accommodate non-integer indices or negative inputs.
- Does not model real-element exceptions or relativistic corrections.
- Does not incorporate external data or fitting parameters.
Lean usage
theorem shellCapacity_3 : shellCapacity 3 = 18 := rflformal statement (Lean)
94def shellCapacity : ℕ → ℕ
95 | 0 => 2 -- 1s²
96 | 1 => 8 -- 2s² 2p⁶
97 | 2 => 8 -- 3s² 3p⁶
98 | 3 => 18 -- 4s² 3d¹⁰ 4p⁶
99 | 4 => 18 -- 5s² 4d¹⁰ 5p⁶
100 | 5 => 32 -- 6s² 4f¹⁴ 5d¹⁰ 6p⁶
101 | 6 => 32 -- 7s² 5f¹⁴ 6d¹⁰ 7p⁶
102 | _ => 32 -- Continuation pattern
103
104/-- Cumulative electron count at shell closure n.
105 These are exactly the noble gas atomic numbers. -/