PeriodicTableCert
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the 2n² formula from the phi-ladder or J-cost.
- Does not address period lengths beyond n = 4 or the full periodic table.
- Does not invoke the forcing chain T0–T8 or Recognition Composition Law.
- Does not prove uniqueness or completeness of the five block types.
formal statement (Lean)
43structure PeriodicTableCert where
44 five_blocks : Fintype.card ElectronBlock = 5
45 s1_cap : shellCapacity 1 = 2
46 s2_cap : shellCapacity 2 = 8
47 s3_cap : shellCapacity 3 = 18
48 s4_cap : shellCapacity 4 = 32
49