indexOf
plain-language theorem explainer
indexOf maps each atomic number Z to an Index record pairing a rail integer with one of the blocks s, p, d or f. Chemists using the Recognition Science periodic-table scaffold cite this zero-parameter assignment to locate elements on phi-tier rails. The definition computes the rail by integer division of (Z-1) by 8 and selects the block by case analysis on the remainder modulo 8.
Claim. The function sending each natural number $Z$ (atomic number) to the pair $r = (Z-1) // 8$, $b$ where $b$ is s when the remainder $r' = (Z-1) mod 8$ equals 0 or 1, p when 2, 3 or 4, d when 5 or 6, and f otherwise, packaged as the record with rail field $r$ and block field $b$.
background
The Periodic Table Engine realizes an octave-to-eight-tick mapping for chemistry: phi-tier rails equipped with fixed block offsets s/p/d/f and an eight-window neutrality predicate that detects noble-gas closures. The Index structure is the pair (rail : ℤ, block : Block) where Block is the inductive type with constructors s, p, d, f. Block counts obey the standard formula 2(2l+1) for angular-momentum quantum number l, as recorded in the sibling block_count_formula theorem.
proof idea
The definition binds a local rail to the integer quotient (Z-1)/8 and a local position to the remainder (Z-1)%8, then performs a match on position to choose Block.s, Block.p, Block.d or Block.f before returning the Index record. No lemmas are applied; the construction is a direct computational definition.
why it matters
indexOf supplies the deterministic rail-and-block placement that bandMultiplier invokes to obtain the dimensionless band multiplier via blockFactor. It thereby implements the eight-tick octave (T7) inside the chemistry domain and directly supports the Noble Gas Closure Theorem (P0-A0) that noble gases occur exactly where cumulative valence cost meets eight-window neutrality. The same indexer is referenced by the atomicity scheduler theorems for sequential tick ordering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.