noble_gas_ea_zero
plain-language theorem explainer
Noble gases sit at shell closure so their electron affinity proxy vanishes. A chemist modeling periodic EA trends or a materials theorist checking RS scaling would cite this to fix the zero point of the proxy. The proof is a one-line term wrapper that unfolds the proxy definition and invokes the upstream closure theorem for noble gases.
Claim. Let $Z$ be a natural number. If $Z$ satisfies the noble-gas predicate (i.e., $Z$ belongs to the list of shell-closure atomic numbers), then the electron-affinity proxy of $Z$ equals zero.
background
The module derives electron affinity from the Recognition Science approach-to-closure pattern on the eight-tick octave. Electron affinity is proxied by the number of electrons still needed to reach the next noble-gas shell; this distance is called distToClosure and is set equal to eaProxy. Noble gases are defined by the predicate isNobleGas, which holds precisely when $Z$ is one of the known closure numbers (He, Ne, Ar, Kr, Xe, Rn).
proof idea
The proof is a term-mode one-liner. It applies simp to replace eaProxy and distToClosure by their definitions, exposing distToNextClosure, then feeds the hypothesis that $Z$ is a noble gas directly into the upstream theorem noble_gas_at_closure.
why it matters
This result fixes the zero of the EA proxy at shell closure, confirming the CH-006 prediction that noble gases exhibit EA proxy = 0 and therefore lie at the bottom of the RS ordering (halogens highest, noble gases lowest). It closes the boundary case required by the Recognition Composition Law and the eight-tick neutrality condition. No downstream uses are recorded yet, but the lemma is the natural anchor for any later quantitative EA formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.