Gravity at the everyday level: the Newtonian binding energy of positive masses at distinct positions is negative
ProvedEveryday.newtonian_bindingThe image's gravity label is the Einstein–Hilbert term (m_p²/2) R, and the post notes that gravity is understood "perfectly well at the everyday level": there, the Einstein–Hilbert term reduces to Newtonian gravitation. The item is the Newtonian sector's everyday content: gravitation binds. For finitely many positive masses at pairwise distinct positions, the gravitational binding energy — half the sum of the pair energies -G m_i m_j / |q_i - q_j| over ordered pairs of distinct particles — is strictly negative. Assemblies of positive masses attract, and the binding energy of an everyday gravitational system is negative.
Formalization Note The sum runs over ordered pairs of distinct particles, so each unordered pair is counted twice; the factor 2 in the denominator implements the halving, making the sum the binding energy. The hypotheses are positivity of G, positivity of every mass, distinctness of distinct particles' positions, and the existence of at least two particles, carried as the nontriviality of the index type. The index type also carries decidable equality, the proof-irrelevant bookkeeping instance required to form the filtered sum; it imposes no restriction on the physical content. The conclusion is the strict negativity of the binding sum.
import Mathlib import Definitions.Def_Everyday_spacetime import Definitions.Def_Everyday_sectors
open scoped BigOperators
namespace Everyday
/-- Gravity, at the everyday level: Newtonian gravitation is
attractive. For finitely many positive masses at pairwise distinct
positions, the gravitational binding energy — half the sum of the pair
energies over ordered pairs of distinct particles — is strictly
negative. This is the everyday face of the (m_p²/2) R sector: at the
everyday level the Einstein–Hilbert term reduces to Newtonian
gravitation, and Newtonian gravitation binds. -/
theorem newtonian_binding (ι : Type) [Fintype ι] [DecidableEq ι] [Nontrivial ι]
(G : ℝ) (m : ι → ℝ) (q : ι → ℝ)
(hG : 0 < G) (hm : ∀ i, 0 < m i) (hq : ∀ i j, i ≠ j → q i ≠ q j) :
∑ p ∈ Finset.univ.filter (fun p : ι × ι => p.1 ≠ p.2),
-(G * m p.1 * m p.2 / (2 * |q p.1 - q p.2|)) < 0 := by sorry
end Everyday
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for every type ι equipped with the structures of a finite type, decidable equality, and nontriviality — the presence of at least two distinct elements — every real number G, and every pair of functions m and q assigning real numbers to the elements of ι, if G is strictly positive, every m i is strictly positive, and q i and q j differ whenever i and j differ, then the sum — over the ordered pairs p of elements of ι whose two components differ — of the negation of (G times m of the first component times m of the second component, divided by twice the absolute value of the difference of q of the two components), is strictly negative. The conclusion is a strict inequality between real numbers.