shellCapacity_2
plain-language theorem explainer
The shell capacity for principal quantum number 2 equals 8 under the 2n² rule. Periodic table certifiers and quantum chemists cite this when populating the block structure record. The proof is a one-line wrapper that applies the decide tactic to evaluate the closed-form arithmetic definition directly.
Claim. The shell capacity for principal quantum number 2 is given by $2n^2$ and equals 8.
background
In this module shellCapacity is defined by the closed expression 2n² for principal quantum number n. This reproduces the standard count of electron states per shell that follows from angular momentum quantization. The module situates these values inside the periodic table periods, where lengths follow the sequence 2, 8, 8, 18, 18, 32, 32 while the five block types (s, p, d, f, g) total 32 = 2^5. Upstream the PauliExclusion module states the identical formula 2n² and the PeriodicTable module records the explicit sequence beginning 2, 8, 8, 18.
proof idea
This is a one-line wrapper that applies the decide tactic to compute 2 * 2^2 from the local definition of shellCapacity.
why it matters
The result supplies the s2_cap field inside periodicTableCert, which assembles the certified five-block structure of the periodic table. It therefore closes one concrete value in the chemistry tier of the Recognition framework, confirming the deterministic shell fillings that arise from ledger packing constraints and align with the eight-tick octave pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.