shellCapacity_3
plain-language theorem explainer
The theorem confirms that the third electron shell holds exactly 18 electrons under the 2n² capacity rule. Modelers building periodic table certifications from Recognition Science principles reference this value when populating the block structure record. The proof reduces to a direct decision procedure on the closed arithmetic expression.
Claim. The capacity of the shell with principal quantum number 3 equals 18 electrons: $2n^2 = 18$ for $n=3$.
background
The PeriodicTableFromPhiLadder module defines shellCapacity via the standard formula 2n², producing the sequence 2, 8, 8, 18, 18, 32, 32 for successive periods. This matches the casewise definition in the upstream PeriodicTable module, where the n=3 entry is explicitly 18, and the PauliExclusion module encodes the same count as the number of states permitted by angular momentum quantization derived from ledger packing constraints.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the arithmetic identity 2 * 3^2 = 18 taken directly from the definition of shellCapacity.
why it matters
This supplies the s3_cap field inside the periodicTableCert record that assembles the five-block certification of the periodic table. It completes the explicit shell values needed for the phi-ladder period lengths while inheriting the 2n² formula from upstream quantization results. The placement supports the module's link between block counts (totaling 32) and the framework's configDim D = 5, though the capacity formula itself is not re-derived here from the J-cost or phi-ladder primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.