noble_gas_at_closure
plain-language theorem explainer
Noble gases sit exactly at shell closure points under the Recognition Science valence ledger. Researchers modeling chemical periodicity from the eight-tick neutrality condition would cite this result to anchor electron affinity and electronegativity proxies at zero for elements 2, 10, 18, 36, 54 and 86. The proof reduces membership in the fixed noble-gas list to six exhaustive cases and dispatches each by native decision.
Claim. If $Z$ is a noble gas then the distance to the next shell closure satisfies $distToNextClosure(Z)=0$.
background
The PeriodicTable module supplies a zero-parameter engine for the periodic table by mapping the RS eight-tick octave to shell closures via an 8-window neutrality predicate. Noble gases are the atomic numbers in the list [2, 10, 18, 36, 54, 86] at which cumulative valence cost returns to zero; distToNextClosure(Z) is defined as nextClosure(Z) - Z and therefore vanishes precisely at these points. The module states that noble gases are exactly the elements where the running valence sum mod 8 returns to zero, the chemical counterpart of the fundamental 8-tick ledger balance.
proof idea
The term proof first unfolds isNobleGas and nobleGasZ inside the hypothesis, then simplifies list membership to a disjunction of six equalities. Case analysis on those equalities yields six subgoals, each of which is discharged by native_decide.
why it matters
The result realizes the Noble Gas Closure Theorem (P0-A0) and supplies the key lemma for the downstream theorems noble_gas_ea_zero and noble_gas_zero_en in the ElectronAffinity and Electronegativity modules. It directly embodies the eight-tick octave (T7) and the requirement that shell closures occur at 8-window neutrality points, closing the definition of noble gases without external fitting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.