distToClosure

formal source

  32
  33/-- Distance to next noble gas closure (electrons needed to complete shell).
  34    This is the fundamental proxy for electron affinity. -/
  35def distToClosure (Z : ℕ) : ℕ := distToNextClosure Z
  36
  37/-- Electron affinity proxy: higher when closer to closure.
  38    EA_proxy = periodLength - valenceElectrons = distToClosure
  39    Halogens (dist=1) have highest proxy, noble gases (dist=0) have lowest. -/
  40def eaProxy (Z : ℕ) : ℕ := distToClosure Z
  41
  42/-- Normalized EA proxy: fraction of shell remaining.
  43    EA_norm = distToClosure / periodLength ∈ [0, 1)
  44    Higher = more favorable to add electron. -/
  45def normalizedEA (Z : ℕ) : ℝ :=
  46  if periodLength Z = 0 then 0
  47  else (distToClosure Z : ℝ) / (periodLength Z : ℝ)
  48
  49/-- Predicate: element is a halogen (one electron from noble gas closure). -/
  50def isHalogen (Z : ℕ) : Prop := distToClosure Z = 1
  51
  52/-- Halogen set: {9, 17, 35, 53, 85}. -/
  53def halogenZ : List ℕ := [9, 17, 35, 53, 85]
  54
  55/-- Decidable instance for halogen membership. -/
  56instance : DecidablePred isHalogen := fun Z =>
  57  if h : distToClosure Z = 1 then isTrue h else isFalse h
  58
  59/-! ## Sign Predictions -/
  60
  61/-- Noble gases have EA proxy = 0 (at closure, no benefit from adding electron). -/
  62theorem noble_gas_ea_zero (Z : ℕ) (h : isNobleGas Z) : eaProxy Z = 0 := by
  63  simp only [eaProxy, distToClosure]
  64  exact noble_gas_at_closure Z h
  65