PeriodicTableCert
plain-language theorem explainer
PeriodicTableCert records the five electron block types together with the explicit shell capacities 2, 8, 18 and 32 for principal quantum numbers 1 through 4. Chemists tracing the periodic table back to Recognition Science ledger constraints would cite the certificate to confirm that the standard 2n² sequence appears once the block enumeration is fixed. The declaration is introduced as a plain structure definition with no computational content or lemma applications.
Claim. The structure asserts that the inductive type of electron blocks (s, p, d, f, g_predicted) has cardinality 5 and that the shell-capacity function satisfies shellCapacity(1) = 2, shellCapacity(2) = 8, shellCapacity(3) = 18 and shellCapacity(4) = 32.
background
ElectronBlock is the inductive enumeration of the five orbital blocks s, p, d, f and g_predicted, equipped with Fintype. The local shellCapacity function is defined by shellCapacity(n) := 2n², matching the upstream definition in PeriodicTableFromPhiLadder and the PauliExclusion version in QFT. The module documentation states that these capacities are not themselves phi-ladder values but that the number of blocks equals configDim D = 5, while period lengths follow the phi-ladder pattern 2, 8, 8, 18, 18, 32, 32, … . Upstream shellCapacity in PeriodicTable supplies the deterministic sequence forced by angular-momentum quantization derived from ledger packing.
proof idea
The declaration is a structure definition that directly records the Fintype.card equality for ElectronBlock and the four explicit capacity equations; no tactics, lemmas or reductions are applied.
why it matters
PeriodicTableCert supplies the concrete values consumed by the downstream periodicTableCert definition that instantiates the certificate. It bridges the phi-ladder period lengths noted in the module documentation to the standard 2n² shell capacities, aligning with the Recognition Science derivation of angular-momentum quantization. The five-block count corresponds to configDim D = 5 in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.