argon_is_noble
plain-language theorem explainer
Argon with atomic number 18 satisfies the noble gas predicate, confirming shell closure under eight-window neutrality. Chemists or foundational physicists working in the Recognition Science framework cite this as a direct check of the forced noble gas sequence. The proof is a one-line native decision procedure that evaluates membership in the fixed noble gas list.
Claim. The atomic number $18$ belongs to the noble gas set, i.e., the predicate that $Z$ is a noble gas holds at $Z=18$.
background
The Periodic Table module supplies a zero-parameter engine that maps chemistry to the eight-tick octave via phi-tier rails and fixed block offsets. Noble gases are defined exactly as the elements where cumulative valence cost returns to 8-window neutrality; this is the chemical counterpart of the 8-tick ledger balance in the fundamental RS scheduler. The predicate isNobleGas(Z) is the membership test Z ∈ nobleGasZ, whose decidable instance is supplied upstream.
proof idea
One-line wrapper that applies the decidable instance for membership in nobleGasZ via native_decide.
why it matters
The declaration verifies the noble gas closure theorem (P0-A0) for argon, confirming the deterministic prediction of the set {2, 10, 18, 36, 54, 86} as 8-window neutrality points. It instantiates the T7 eight-tick octave landmark inside the chemistry domain and supplies a concrete instance for the general noble-gas predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.