shellCapacity
plain-language theorem explainer
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.
Claim. Define 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.