periodicTableCert
plain-language theorem explainer
The declaration constructs a certified instance of PeriodicTableCert asserting five electron blocks together with shell capacities 2, 8, 18 and 32. A chemist working inside the Recognition Science framework would cite it to anchor the periodic table structure to the phi-ladder block count. The definition is assembled by direct substitution of four decided theorems into the record fields.
Claim. Let PeriodicTableCert be the structure requiring that the cardinality of the set of electron blocks equals 5 and that the shell capacities satisfy $shellCapacity(1)=2$, $shellCapacity(2)=8$, $shellCapacity(3)=18$, $shellCapacity(4)=32$. Then periodicTableCert is the instance of this structure obtained by substituting the block-count theorem and the four shell-capacity theorems.
background
In the Periodic Table from Phi-Ladder module the standard shell capacities 2, 8, 18, 32 arise from the formula 2n² for principal quantum number n. The module stresses instead that the number of blocks (s, p, d, f and predicted g) is five, matching configDim D = 5. The upstream theorem electronBlockCount states that the cardinality of ElectronBlock is exactly five, proved by decision. The four theorems shellCapacity_1 through shellCapacity_4 each assert the corresponding capacity value, again by decision.
proof idea
The definition constructs the PeriodicTableCert record by assigning the five_blocks field to electronBlockCount and the four capacity fields to shellCapacity_1 through shellCapacity_4. It is a direct one-line wrapper that assembles the structure from the pre-proved component theorems.
why it matters
This definition supplies the concrete certificate required by the PeriodicTableCert structure in the chemistry extension. It closes the interface between the abstract five-block count and the explicit shell capacities, enabling later derivations of period lengths on the phi-ladder. The five-block count aligns with configDim D = 5 while the capacities themselves remain outside the phi-ladder; the declaration therefore provides the exact hook needed for further integration with the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.