periodLengths
plain-language theorem explainer
The definition supplies the fixed sequence of period lengths [2, 8, 8, 18, 18, 32, 32] for the periodic table. Researchers modeling chemistry from ledger constraints would cite it when mapping eight-tick neutrality to noble-gas closures. It is introduced as a direct definition that encodes the doubling pattern arising from 2n² shell capacities.
Claim. The period lengths are the list $[2, 8, 8, 18, 18, 32, 32]$, obtained by successive doubling applied to the quadratic capacities $2n^2$.
background
The Periodic Table Engine treats chemistry as an eight-tick ledger balance under the Recognition Composition Law. Noble gases arise exactly where cumulative valence cost returns to zero modulo the 8-window neutrality predicate, reproducing the set {2, 10, 18, 36, 54, 86} without adjustable parameters. The module imports the period function from pulsar regimes, defined as period(k) = phi^k, to anchor the phi-tier rails that generate the observed doubling sequence.
proof idea
This is a direct definition that hard-codes the sequence stated in the module comment. No lemmas are applied; the body simply returns the list that encodes the 2n² doubling pattern.
why it matters
The definition supplies the fixed lengths required by the Noble Gas Closure Theorem (P0-A0) in the same module. It instantiates the eight-tick octave (T7) for chemistry and supports the zero-parameter scaffold that predicts shell closures from ledger packing alone. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.