electronBlockCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive shell capacities 2n² from the phi-ladder.
- Does not prove existence or properties of the predicted g block.
- Does not connect block sizes to the Recognition Composition Law.
- Does not address period lengths or element counts beyond block enumeration.
formal statement (Lean)
33theorem electronBlockCount : Fintype.card ElectronBlock = 5 := by decide
proof body
Term-mode proof.
34
35/-- Shell capacities: 2n². -/