shellCapacity_3
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the 2n² formula from phi-ladder or J-cost axioms.
- Does not address real-world exceptions such as energy level crossings in heavier elements.
- Does not extend the certification to relativistic or many-body corrections.
Lean usage
def periodicTableCert : PeriodicTableCert where ... s3_cap := shellCapacity_3formal statement (Lean)
40theorem shellCapacity_3 : shellCapacity 3 = 18 := by decide