default
plain-language theorem explainer
The default BlockOffsets supplies fixed integer shifts for the four orbital blocks in the Recognition Science periodic table scaffold. Researchers building valence cost models or noble-gas closure predictions cite this when enforcing the eight-window neutrality condition without fitting parameters. It is realized by a direct record construction that pattern-matches on the Block inductive type and returns the offsets 0, 1, 2, 3.
Claim. Let $B$ be the inductive type with constructors $s,p,d,f$. The default BlockOffsets is the structure whose offset function satisfies offset$(s)=0$, offset$(p)=1$, offset$(d)=2$, offset$(f)=3$.
background
The PeriodicTable module implements a fit-free scaffold for the periodic table using φ-tier rails and an eight-window neutrality predicate to locate noble-gas closures. BlockOffsets is the class that supplies an offset : Block → ℤ for each block type. The Block inductive type enumerates the four standard blocks s, p, d, f. Upstream, the shell function from PeriodicBlocks defines shell(n) := E_coh * block_capacity(n), providing the energy scale that these offsets modulate.
proof idea
The definition constructs a BlockOffsets record literal whose offset field is a match expression on the four Block constructors, returning the constants 0, 1, 2, 3 respectively. No external lemmas are invoked; the construction is purely definitional.
why it matters
This definition supplies the canonical offsets required by the Noble Gas Closure Theorem (P0-A0) stated in the module documentation, which identifies noble gases as the points where cumulative valence cost satisfies eight-window neutrality. It is referenced by downstream results including phi_cubed_in_theta_band in PhotobiomodulationDevice and by the AczelRegularityKernel in cost classification. The fixed offsets enforce the zero-parameter discipline of the Recognition Science chemistry engine and align with the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.