Index
The Index structure pairs an integer rail with one of the four blocks s, p, d or f to label positions on the phi-tier periodic table. Downstream code in glass transition, primordial spectra and ILG tensors cites it when mapping atomic number Z to ledger-neutral closures. The declaration is a bare structure with Repr derivation and zero computational body.
claimAn index is a pair consisting of an integer rail $r$ and a block $b$ drawn from the set of four angular-momentum labels $s,p,d,f$.
background
The PeriodicTable module supplies a zero-parameter scaffold that maps the eight-tick octave onto chemistry via phi-tier rails and fixed block offsets. Block is the inductive type with constructors s (l=0), p (l=1), d (l=2), f (l=3) whose electron counts are given by the 2(2l+1) formula. The module document states that noble-gas closures occur exactly where the cumulative valence cost satisfies 8-window neutrality, the chemical counterpart of the fundamental RS scheduler balance. Upstream, the from theorem reduces seven axioms to four structural conditions, while the ILG Action Index supplies the symbolic Nat convention reused for tensor indices.
proof idea
The declaration is a structure definition with an empty proof body. It simply introduces the two fields rail : ℤ and block : Block and attaches the Repr instance; no lemmas or tactics are applied.
why it matters in Recognition Science
Index is the common currency for all periodic-table calculations in the Recognition framework. It is consumed by indexOf (the deterministic Z-to-(rail,block) map), kauzmann_lt_one, the r_prediction bound in cosmology, and the ILG action structures. The construction directly implements the eight-tick octave (T7) and the noble-gas closure theorem (P0-A0) inside the chemistry domain, supplying the phi-ladder rung needed for mass and energy formulas without any per-element tuning.
scope and limits
- Does not assign numerical atomic numbers to specific rails.
- Does not compute electron counts or valence energies.
- Does not incorporate measured spectra or adjustable parameters.
- Does not define the full mapping from Z to Index; that is supplied by indexOf.
formal statement (Lean)
247structure Index where
248 rail : ℤ
249 block : Block
250 deriving Repr
251
252/- Placeholder indexer from atomic number (deterministic, no tuning). -/