shellCapacity_4
plain-language theorem explainer
The fourth electron shell holds exactly 32 electrons under the 2n² capacity rule. Quantum chemists and periodic-table modelers cite this when verifying the f-block and higher-period structure forced by angular-momentum quantization. The proof is a one-line wrapper that applies the decide tactic to evaluate the arithmetic definition directly.
Claim. The capacity of the electron shell with principal quantum number $n=4$ is $2n^2=32$.
background
In the Recognition Science chemistry module the electron-shell capacities are defined by the standard quadratic formula shellCapacity n := 2 * n^2. This matches the sequences recorded in the upstream PeriodicTable and PauliExclusion modules, which list the deterministic filling order {2, 8, 8, 18, 18, 32, 32, …} arising from angular-momentum quantization derived from ledger-packing constraints. The local module PeriodicTableFromPhiLadder places these capacities inside the broader phi-ladder pattern of observed period lengths while retaining the 2n² rule itself.
proof idea
One-line wrapper that applies the decide tactic to reduce 2 * 4 ^ 2 to the numeral 32 using the local definition of shellCapacity.
why it matters
The theorem supplies the s4_cap field inside the periodicTableCert certificate that aggregates block counts and shell capacities for the full periodic table. It completes the n=4 case of the 2n² sequence before the module links capacities to the five-block structure (s, p, d, f, g) and the phi-ladder period lengths. Within the Recognition Science chain this step confirms the quantization rule that later feeds the chemistry tier of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.