pith. machine review for the scientific record. sign in
theorem proved term proof

argon_ea_zero

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 130theorem argon_ea_zero : eaProxy 18 = 0 := by native_decide

proof body

Term-mode proof.

 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

depends on (13)

Lean names referenced from this declaration's body.