`neon_ea_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.Chemistry.ElectronAffinity
domain: Chemistry
line: 127 · 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 127.

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

formal source

 124theorem astatine_is_halogen : isHalogen 85 := by native_decide
 125
 126/-- Neon (Z=10) has zero EA proxy. -/
 127theorem neon_ea_zero : eaProxy 10 = 0 := by native_decide
 128
 129/-- Argon (Z=18) has zero EA proxy. -/
 130theorem argon_ea_zero : eaProxy 18 = 0 := by native_decide
 131
 132/-! ## Falsification Criteria
 133
 134The electron affinity derivation is falsifiable:
 135
 1361. **Sign violation**: If noble gases have positive EA (they should be ≤ 0).
 137
 1382. **Halogen not maximum**: If any halogen does NOT have maximum EA in its period.
 139
 1403. **Ordering violation**: If EA ordering doesn't follow "closer to closure = higher EA"
 141   for main group elements (allowing d/f-block anomalies).
 142
 143Note: Actual EA values in eV are NOT predicted without a scale anchor.
 144Only the ORDERING and SIGNS are fit-free predictions.
 145-/
 146
 147end
 148end ElectronAffinity
 149end Chemistry
 150end IndisputableMonolith

papers checked against this theorem

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