shellCapacity_1
plain-language theorem explainer
The first electron shell holds exactly 2 electrons. Chemists or physicists building periodic table structure from Recognition Science would cite this base case. The proof is a one-line decision procedure that evaluates the defining equation 2n² at n=1.
Claim. The electron shell capacity for principal quantum number $n=1$ is $2n^2=2$.
background
In the Recognition Science treatment of chemistry the electron shell capacities follow the deterministic sequence 2, 8, 8, 18, 18, 32, 32, … . The local definition sets shellCapacity(n) := 2 * n², matching the formula already established in the PeriodicTable and QFT.PauliExclusion modules. The module doc notes that these capacities arise from angular momentum quantization derived from ledger packing constraints, while period lengths themselves follow a phi-ladder pattern.
proof idea
One-line wrapper that applies the decide tactic to the equality obtained by substituting n=1 into the definition shellCapacity(n) := 2 * n².
why it matters
This base case supplies the s1_cap field inside periodicTableCert, which certifies the five-block (s, p, d, f, g) structure of the periodic table. It completes the n=1 entry required by the Chemistry.PeriodicTableFromPhiLadder construction and rests on the upstream shellCapacity definitions that encode the 2n² rule forced by prior quantization results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.