electronBlockCount
plain-language theorem explainer
The finite set of electron block types has cardinality five. A chemist deriving periodic table structure from the phi-ladder would cite this count to fix the number of blocks at five. The proof is a one-line decision procedure that evaluates the automatically generated Fintype instance on the five-constructor inductive type.
Claim. The finite cardinality of the set of electron block types is five: $|E| = 5$ where $E = {s, p, d, f, g_{predicted}}$.
background
The module constructs periodic table shells from the phi-ladder while separating block count from capacity formulas. ElectronBlock is the inductive type whose five constructors enumerate the canonical blocks s, p, d, f and the predicted g block. The module document states that these five blocks equal configDim D = 5, distinct from the 2n² shell capacities that appear in the same file.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. Decide computes Fintype.card directly from the derived Fintype instance on the inductive type ElectronBlock.
why it matters
The result supplies the five_blocks field inside PeriodicTableCert, the top-level certificate for the periodic table construction. It records the Recognition Science claim that configuration dimension equals five, consistent with the eight-tick octave and the forcing chain step that fixes D = 3 spatial dimensions while allowing five orbital blocks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.