xenon_is_noble
plain-language theorem explainer
Xenon at atomic number 54 satisfies the noble gas predicate defined by membership in the fixed closure set. Modelers of fit-free chemistry via eight-tick ledger balance would cite this verified instance. The proof reduces to a single native decision on set membership.
Claim. The atomic number 54 belongs to the noble gas set, i.e., $54$ satisfies the eight-window neutrality closure condition.
background
The module frames the periodic table as an octave mapping with phi-tier rails and fixed block offsets. Noble gases arise exactly where the cumulative valence cost returns the running sum to zero modulo 8, manifesting the 8-tick ledger balance. The predicate isNobleGas Z holds precisely when Z lies in the precomputed nobleGasZ list whose elements are the forced shell closures {2, 10, 18, 36, 54, 86}.
proof idea
One-line wrapper that applies native_decide to discharge the membership goal for 54 against nobleGasZ.
why it matters
The result instantiates the Noble Gas Closure Theorem (P0-A0) for Z=54 inside the forced set. It supplies a concrete data point for the eight-tick neutrality condition that links directly to the T7 octave in the forcing chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.