argon_ea_zero
plain-language theorem explainer
Argon at atomic number 18 has zero electron affinity proxy under the distance-to-closure measure. Chemists applying Recognition Science to periodic trends would cite this to confirm the model's closure prediction for noble gases. The proof is a direct native decision on the proxy definition.
Claim. The electron affinity proxy for argon satisfies $eaProxy(18) = 0$, where the proxy equals distance to shell closure.
background
Electron affinity follows the approach-to-closure pattern on the phi-ladder. The proxy is defined as distToClosure Z, which equals period length minus valence electrons; halogens sit at distance 1 and noble gases at distance 0. The module sets the local setting that noble gases at closure must have near-zero or negative EA while halogens achieve the period maximum.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the proxy definition at Z=18.
why it matters
This result fills the noble-gas case of the CH-006 prediction that EA ordering runs halogens greater than chalcogens down to noble gases with sign at most zero. It rests on the upstream eaProxy definition and the eight-tick neutrality mechanism. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.