shell_sum_to_noble
The theorem verifies that the cumulative shell closures for indices 0 through 5 produce exactly the noble gas atomic numbers list. Chemists using Recognition Science ledger models would cite it to anchor the eight-window neutrality condition for periodic closures. The proof reduces to a single native_decide evaluation that computes the finite list equality by direct substitution of the shell values.
claimThe list obtained by applying the cumulative shell closure function to each integer from 0 to 5 equals the noble gas atomic numbers $[2, 10, 18, 36, 54, 86]$.
background
The Periodic Table Engine maps the eight-tick octave to chemistry via phi-tier rails, fixed block offsets, and an eight-window neutrality predicate that detects noble-gas closures. Noble gases arise exactly where the running valence cost returns to zero under this ledger balance, without any per-element fitting. The cumulative shell closure function supplies the electron count at each successive closure, while nobleGasZ supplies the target list of the first six such numbers including Oganesson.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the list equality by direct computation of the six cumulative shell values.
why it matters in Recognition Science
This result confirms the Noble Gas Closure Theorem (P0-A0) stated in the module documentation by exhibiting the exact match between shell sums and the canonical noble gas list. It supplies the concrete anchor for the subsequent period structure theorems (P0-A1) that derive period lengths from ledger packing. In the broader framework it realizes the eight-tick octave (T7) as the chemical expression of ledger neutrality, with the Structure inductive type and the from theorem on structural conditions providing the upstream axiomatic support.
scope and limits
- Does not derive the shell capacity values from the Recognition functional equation or J-cost.
- Does not extend the equality beyond the first six periods.
- Does not incorporate crystal structure types into the summation.
- Does not propagate measurement uncertainties through the map operation.
formal statement (Lean)
213theorem shell_sum_to_noble :
214 (List.range 6).map (fun i => cumulativeShellClosure i) = nobleGasZ := by
proof body
Term-mode proof.
215 native_decide
216
217/-! ## Period Structure Theorems (P0-A1) -/
218
219/-- Period lengths are forced by the ledger packing constraints.
220 The sequence {2, 8, 8, 18, 18, 32, 32} emerges from 2n² with doubling. -/