indexOf
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute numerical electron energies or binding energies.
- Does not incorporate relativistic corrections or spin-orbit coupling.
- Does not predict deviations from the ideal s/p/d/f block sequence.
- Does not apply the phi-ladder mass formula or yardstick scaling.
Lean usage
let idx := indexOf Z; blockFactor idx.rail idx.blockformal statement (Lean)
253def indexOf (Z : ℕ) : Index :=
proof body
Definition body.
254 let period : ℕ := (Z - 1) / 8
255 let pos : ℕ := (Z - 1) % 8
256 let b : Block :=
257 match pos with
258 | 0 | 1 => Block.s
259 | 2 | 3 | 4 => Block.p
260 | 5 | 6 => Block.d
261 | _ => Block.f
262 { rail := (period : ℤ), block := b }
263
264/- Dimensionless predicted band multiplier for atomic number `Z`. -/