`halogenZ`

definition

show as: view math explainer →

module: IndisputableMonolith.Chemistry.ElectronAffinity
domain: Chemistry
line: 53 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Chemistry.ElectronAffinity on GitHub at line 53.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  66/-- Halogens have EA proxy = 1 (one electron completes shell). -/
  67theorem halogen_ea_one (Z : ℕ) (h : isHalogen Z) : eaProxy Z = 1 := by
  68  simp only [eaProxy, distToClosure]
  69  exact h
  70
  71/-- Fluorine is a halogen (in list). -/
  72theorem fluorine_in_halogen_list : 9 ∈ halogenZ := by native_decide
  73
  74/-- Chlorine is a halogen (in list). -/
  75theorem chlorine_in_halogen_list : 17 ∈ halogenZ := by native_decide
  76
  77/-- Bromine is a halogen (in list). -/
  78theorem bromine_in_halogen_list : 35 ∈ halogenZ := by native_decide
  79
  80/-- Iodine is a halogen (in list). -/
  81theorem iodine_in_halogen_list : 53 ∈ halogenZ := by native_decide
  82
  83/-- Astatine is a halogen (in list). -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.