isNobleGas
plain-language theorem explainer
isNobleGas Z holds exactly when the atomic number Z belongs to the fixed list of shell-closure points [2, 10, 18, 36, 54, 86]. Modelers of chemical periodicity inside Recognition Science cite this predicate when establishing zero electron affinity or peak ionization energy at noble-gas closures. The declaration is a direct membership definition equipped with a decidable instance that performs a simple list check.
Claim. For a natural number $Z$, the predicate isNobleGas$(Z)$ holds if and only if $Z$ is an element of the list of noble-gas atomic numbers $[2, 10, 18, 36, 54, 86]$.
background
The Periodic Table Engine maps chemistry onto an eight-tick ledger in which each element adds a valence imbalance and noble gases mark the points where the running sum returns to neutrality modulo 8. This is the chemical counterpart of the 8-tick octave in the fundamental RS scheduler. The predicate is defined directly in terms of nobleGasZ, the canonical list of the first six period closures together with Oganesson. The module states that these closures are forced by the requirement of 8-window neutrality under a deterministic valence proxy with no per-element fitting.
proof idea
The declaration is a definition that expands isNobleGas Z to the proposition Z ∈ nobleGasZ. A separate DecidablePred instance implements the check by a direct if-then-else on list membership, yielding isTrue or isFalse without further lemmas.
why it matters
This predicate is the single interface used by all subsequent chemical theorems: noble_gas_ea_zero, noble_gas_zero_en, noble_max_ionization, and sawtooth_reset all take an isNobleGas hypothesis. It realizes the Noble Gas Closure Theorem (P0-A0) and thereby imports the eight-tick octave (T7) into chemistry. The list itself is treated as the deterministic output of the 8-window neutrality condition rather than an empirical input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.