Stability of matter

Stability of matter in nonnegative extended additive form, from Baxter’s electrostatic inequality and the kinetic Lieb–Thirring inequality.

theorem LiebThirring.stability_of_matter (q : ℕ) (hq : 1 ≤ q) (Z : NNReal) : ∃ (C : NNReal), 0 < C ∧ ∀ (N M : ℕ) (z : Fin M → NNReal) (R : Fin M → Position) (ψ : State N q), (∀ (k : Fin M), z k ≤ Z) → antisymmetric ψ → ‖ψ‖ = 1 → ∫⁻ (x : Configuration N), attraction z R x * ↑‖↑↑ψ x‖₊ ^ 2 ≤ (kineticEnergy ψ + ∫⁻ (x : Configuration N), electronRepulsion x * ↑‖↑↑ψ x‖₊ ^ 2) + nuclearRepulsion z R + ↑C * ↑(N + M)