halogen_max_ea
Within each period, the electron affinity proxy given by distance to next noble gas closure decreases monotonically with atomic number Z. Chemists modeling periodic trends under Recognition Science would cite this to confirm halogens achieve the highest EA in their period. The proof is a one-line wrapper that unfolds the distance definition and lets omega discharge the resulting arithmetic comparison.
claimLet $n(Z)$ be the next noble gas closure after atomic number $Z$ and let $d(Z) = n(Z) - Z$. For natural numbers $Z, Z'$ with $Z ≤ n(Z)$, $Z' ≤ n(Z')$, $n(Z) = n(Z')$, and $Z' < n(Z')$, the inequality $d(Z') ≤ d(Z)$ holds if and only if $Z ≤ Z'$.
background
The module derives electron affinity from φ-ladder scaling (CH-006). Electron affinity follows an approach-to-closure pattern: halogens (one electron short of closure) release high energy on electron addition, noble gases (at closure) show near-zero or negative EA, and alkali metals (one past closure) show low EA. The RS mechanism ties EA to cost reduction toward 8-tick neutrality. Upstream, nextClosure(Z) returns the next noble gas Z-value (2, 10, 18, 36, 54, …) and distToNextClosure(Z) is defined as nextClosure(Z) − Z, equaling zero precisely at noble gases.
proof idea
The proof is a one-line wrapper. simp only [distToNextClosure] unfolds the distance definition, converting the target inequality into an arithmetic statement of the form (n − Z′) ≤ (n − Z). The omega tactic then discharges the comparison directly from the shared n and the assumption Z′ < n.
why it matters in Recognition Science
The result fills the halogen-maximum claim in the CH-006 electron-affinity ordering and rests on the periodic closure structure (T7 eight-tick octave). It supplies the monotonicity needed for sibling statements such as halogen_ea_one and the element-specific lists (fluorine_in_halogen_list, …). No downstream theorems are recorded, yet the lemma anchors the broader prediction that EA ordering follows distance to closure across the φ-ladder.
scope and limits
- Does not compute numerical EA values or binding energies.
- Does not incorporate relativistic or spin-orbit corrections for heavy elements.
- Does not address EA sign changes or negative values for noble gases.
- Does not extend beyond the finite list of closures encoded in nextClosure.
formal statement (Lean)
100theorem halogen_max_ea (Z : ℕ) (Z' : ℕ)
101 (hZle : Z ≤ nextClosure Z)
102 (_ : Z' ≤ nextClosure Z')
103 (hSamePeriod : nextClosure Z = nextClosure Z')
104 (hZ'lt : Z' < nextClosure Z') :
105 distToNextClosure Z' ≤ distToNextClosure Z ↔ Z ≤ Z' := by
proof body
Term-mode proof.
106 simp only [distToNextClosure]
107 omega
108
109/-! ## Specific Element Theorems -/
110
111/-- Fluorine (Z=9) is a halogen. -/