krypton_is_noble
plain-language theorem explainer
Krypton with atomic number 36 satisfies the noble gas predicate under the eight-window neutrality definition. Modelers of chemical shell closures via the RS ledger would cite this verification as part of the forced closure set. The proof is a one-line native decision that evaluates membership in the noble gas set.
Claim. The atomic number 36 belongs to the noble gas set, i.e., $36$ is an element where the cumulative valence cost achieves 8-window neutrality.
background
The Periodic Table Engine implements an octave-to-eight-tick mapping for chemistry using fixed block offsets and an eight-window neutrality predicate. Noble gases are defined exactly as the closure points where the running valence sum returns to zero modulo 8. The predicate isNobleGas(Z) holds if and only if Z lies in the set nobleGasZ encoding the forced closures {2, 10, 18, 36, 54, 86}.
proof idea
The proof is a one-line wrapper that invokes the decidable predicate instance for isNobleGas and applies native_decide to confirm membership of 36 in nobleGasZ.
why it matters
This instance fills a concrete slot in the Noble Gas Closure Theorem (P0-A0) stated in the module, which identifies noble gases as the 8-tick ledger balance points. It directly instantiates the eight-tick octave landmark (T7) for the chemical domain without introducing parameters or fitting. No downstream theorems depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.