indexOf
plain-language theorem explainer
The definition maps each atomic number Z to an Index pair consisting of rail floor((Z-1)/8) and one of the four blocks s/p/d/f selected by the remainder modulo 8. Modelers of fit-free valence structure in the periodic table cite it to generate rail-block coordinates from the eight-tick ledger without parameter adjustment. The body performs two integer operations on (Z-1) followed by a four-way case distinction on the position.
Claim. The map sending natural number atomic number $Z$ to the structure whose rail component is $\lfloor(Z-1)/8\rfloor$ and whose block component is s when the remainder is 0 or 1, p when 2-4, d when 5-6, and f otherwise.
background
Index is the record type pairing an integer rail with a Block value; Block is the inductive type with four constructors s, p, d, f. The module implements the Periodic Table Engine that converts the eight-tick octave into chemistry via fixed block offsets and an eight-window neutrality predicate for noble-gas closures.
Block assignments follow the angular-momentum formula 2(2l+1) as recorded in the block_count_formula theorem. The setting forbids per-element tuning and treats noble gases as exact points where cumulative valence cost returns to zero modulo 8.
Upstream dependencies include the Block inductive definition and the Z anchor map from the Masses module; the period definition from PulsarEmissionRegimes supplies the phi-power convention used elsewhere in the rail construction.
proof idea
Direct definition: compute period as integer division of (Z-1) by 8 and pos as the remainder; match pos against the four cases to select the Block constructor; assemble the Index record from the rail and chosen block.
why it matters
Supplies the rail and block coordinates required by bandMultiplier to produce the dimensionless band multiplier. Realizes the eight-tick octave (T7) inside the chemistry domain and supplies the deterministic indexer presupposed by the noble-gas closure theorem (P0-A0) that forces the set {2, 10, 18, 36, 54, 86}. It is also referenced by the atomic_tick, exists_sequential_schedule and topoSort_respects theorems in the Atomicity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.