Conditional stability of matter

The universally quantified Baxter and kinetic Lieb–Thirring inequalities yield a positive stability constant chosen before particle counts, charges, nuclei, and the state.

theorem LiebThirring.Assembly.stability_of_matter_of_baxter_of_lt (hB : ∀ (N M : ℕ) (Z : NNReal) (R : Fin M → Position) (x : Configuration N), attraction (fun (x : Fin M) => Z) R x + baxterCorrection Z R ≤ electronRepulsion x + nuclearRepulsion (fun (x : Fin M) => Z) R + nearestNucleusControl Z R x) (hLT : ∀ (q : ℕ), 1 ≤ q → ∀ (N : ℕ) (ψ : State N q), antisymmetric ψ → ‖ψ‖ = 1 → ↑ruminConstant * ↑q ^ (-2 / 3) * ∫⁻ (x : Position), density ψ x ^ (5 / 3) ≤ kineticEnergy ψ) (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)

Conditional assembly with the exact stability conclusion.