shellCapacity_4
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the 2n² formula from the J-cost or phi-ladder.
- Does not model sub-period splitting or actual element counts.
- Does not incorporate relativistic corrections for heavy nuclei.
- Does not address exceptions such as the 4s–3d inversion.
Lean usage
example : shellCapacity 4 = 32 := shellCapacity_4formal statement (Lean)
41theorem shellCapacity_4 : shellCapacity 4 = 32 := by decide
proof body
42