bandEnergy
plain-language theorem explainer
The declaration defines the predicted dimensionful band energy for atomic number Z as the product of the universal coherence energy E_coh and the block-dependent multiplier computed from Z under BlockOffsets. Researchers deriving fit-free valence energies or testing eight-window noble-gas closures in Recognition Science would cite this when building periodic-table predictions. The definition is a direct one-line wrapper that invokes bandMultiplier after applying the BlockOffsets instance.
Claim. The predicted band energy for atomic number $Z$ is $E_{coh} times m(Z)$, where $m(Z)$ is the band multiplier obtained from the rail and block indices of $Z$ using the offsets supplied by the BlockOffsets class.
background
The Periodic Table Engine models chemistry through an eight-tick octave mapping onto phi-tier rails with fixed block offsets for s/p/d/f shells. The BlockOffsets class supplies the default phi-packing offsets s=0, p=1, d=2, f=3. bandEnergy relies on bandMultiplier, which itself calls blockFactor on the indexOf Z together with those offsets, and on the coherence energy constant E_coh drawn from the CPM Constants bundle. Upstream, the applied theorem from EnergyConservationDomainCert guarantees energy conservation under time-translation symmetry for Newtonian trajectories, supplying the domain in which coherent energies are well-defined. The module establishes a zero-parameter API whose central result is the Noble Gas Closure Theorem: noble gases occur exactly where cumulative valence cost returns to 8-window neutrality.
proof idea
This is a one-line wrapper that applies the bandMultiplier definition to Z under the BlockOffsets instance and scales the result by the coherence energy constant E_coh.
why it matters
This definition supplies the dimensionful band energy used in the fit-free periodic-table scaffold and directly supports the Noble Gas Closure Theorem (P0-A0) stated in the module, which forces the set {2, 10, 18, 36, 54, 86} at 8-window neutrality points. It instantiates the eight-tick ledger balance from the fundamental RS scheduler and the T7 eight-tick octave landmark. No downstream theorems are recorded yet, so the declaration remains a basic display layer rather than a closure of an open question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.