Optimal lattices for a three-body power-law energy: steep-decay limits, computer-assisted proofs and the minima of the modular graph functions Cₛ,ₛ,ₛ

We study which Bravais lattice of fixed density minimises the three-body energy T_ν(Λ)=∑'x,y∈Λ(|x|\,|y|\,|x-y|)-ν, the sum over all lattice triangles through the origin of the product of their side lengths to the power -ν. In two dimensions T₂ₛ coincides, up to a factor, with the two-loop modular graph function Cs,s,s(τ). We prove that in the steep-decay limit ν→∞ the minimisers converge to the rectangular lattice with aspect ratio √(√17-1)/2 in $d=2$, by solving exactly the associated max–min problem for the smallest triangle product, and to the body-centred cubic lattice in $d=3$, by a computer-assisted argument. For finite exponents we give computer-assisted proofs, carried out in rigorous interval arithmetic, that C2,2,2, C3,3,3 and C4,4,4 attain their minimum only at the square point τ=i (whereas C1,1,1 is minimal at the hexagonal point), that the square lattice is the unique minimiser also for ν=5,7, that the hexagonal lattice is the unique minimiser for ν=3.5, that the hexagonal and square energies cross in $(3.918364,\,3.918366)$, and that the square lattice loses local minimality at some ν₂∈(8.604,\,8.608). The elementary planar results are formalised in Lean 4. Numerically, in three dimensions BCC is the best lattice found for all tested exponents 3.2≤ν≤12, and hcp is never optimal at the tested exponents. Code and certificates: https://doi.org/10.5281/zenodo.22975868. The computations were carried out with the assistance of the AI system Claude (Anthropic).