The triangular lattice minimises the planar Yukawa energy at every density and for every finite mixture of screening lengths: kernel-checked corollaries of planar universal optimality, a human proof, and an exact-potential CVODE consistency study
- 1SocrateAI Lab
Abstract
The openai/math release contains a Lean 4 proof (AI-generated, Comparator-accepted, not peer reviewed) that the triangular lattice minimises the lower g-energy among all locally finite planar configurations of density one, for every smooth completely monotone g of squared distance. This preprint applies it to the planar Yukawa interaction e^{-κr}/r, the 3D-screened Coulomb potential between particles confined to a plane (2D dusty-plasma and colloidal crystals). It is not the 2D Debye–Hückel Green function K0(κr), which is not treated. Every claim is filed in an Elenchus claim ledger (25 claims) with tiers A (kernel-checked Lean), L (verified literature), C (argument or human proof, not machine-checked) and X (floating-point exploration, never supporting a claim). Tier A, conditional on upstream's universal_energy_minimum and on the fidelity of its definitions (axioms within propext, Classical.choice, Quot.sound; planted sorry and planted-axiom controls caught; independent recompiles by separate AI agent instances): e^{-κr}/r is admissible for every κ > 0, so the triangular lattice minimises its energy at density one, and the minimum is finite; the same at every density ρ > 0 for the rescaled lattice (for a single κ this is a reparametrisation); the same for every finite mixture ∑ wi e^{-κir}/r with wi ≥ 0, κi > 0; negative controls: the admissibility lemma needs the sign condition on the weights; g1 − 2g2 is not admissible, so the theorem does not apply to it (this does not show that optimality fails for it). The mathematics is classical (complete monotonicity of the Yukawa potential in r²; completely monotone functions form a convex cone closed under products). Only the kernel-checked corollaries are new. A step-by-step human proof (Tier C) is given beside each Lean statement. Tier X: this corrects the truncation erratum recorded in doi:10.5281/zenodo.23295142 for the CVODE study of doi:10.5281/zenodo.23293429. With the exact, untruncated potential and a rigorous tail bound (rusty-SUNDIALS crate qf-yukawa-crystal), absolute energies move by the erratum amounts (1.77e-2 at κ = 1), while the square–triangular gap moves by only -2.2e-6. 24 published relaxed stages were re-relaxed under the exact potential, and none fell below the exact triangular energy beyond f64 resolution (one stage, the perfect lattice at κ = 1, sits at gap 0 within rounding). That is a subset of the published study, and annealing was not re-run. Controls: an independent 40-digit mpmath sum agrees to 1.7e-16; the published shifted-force values fail the agreement test; the square lattice is a saddle point. Hugging Face: no dusty-plasma or colloid particle dataset was found on the Hub. The OC20 shard used for the disordered initial conditions (colabfit/OC20_IS2RES_val_id, CC-BY-4.0) is matched by sha256 to revision 6a1dfef1. It supplies disorder, not physics. The Elenchus ledger gate exits 1 with 0 blocking findings and 11 flags. Each flag is a Tier A row whose statement adequacy no human has audited (only AI agents audited it). The work was produced by AI agents (Claude) under the author's direction; the author is responsible for the content. It has not been reviewed by human experts.
Related
- The bilayer dipolar-exciton interaction is completely monotone in r^2: kernel-checked triangular-lattice corollaries at every density and an exact-Ewald CVODE consistency study
- Riesz-energy, finiteness and every-density corollaries of the openai/math planar universal-optimality theorem, kernel-checked in Lean 4
- Planar universal optimality, tiered: kernel-checked consequences, a non-uniqueness theorem, and a CVODE N-body consistency check for the Yukawa interaction
- Machine learning-based thermoelectric materials screening with physical consistency and uncertainty propagation
- The hedgehog uniquely minimises every p-energy
BibTeX
@misc{callens2026triangular,
title = {{The triangular lattice minimises the planar Yukawa energy at every density and for every finite mixture of screening lengths: kernel-checked corollaries of planar universal optimality, a human proof, and an exact-potential CVODE consistency study}},
author = {Xavier Callens},
howpublished = {Zenodo (CERN European Organization for Nuclear Research)},
year = {2026},
month = oct,
doi = {10.5281/zenodo.23646104},
url = {https://doi.org/10.5281/zenodo.23646104},
note = {CC BY},
}
RIS
TY - UNPB
TI - The triangular lattice minimises the planar Yukawa energy at every density and for every finite mixture of screening lengths: kernel-checked corollaries of planar universal optimality, a human proof, and an exact-potential CVODE consistency study
AU - Xavier Callens
PY - 2026
DA - 2026/10/25
PB - Zenodo (CERN European Organization for Nuclear Research)
DO - 10.5281/zenodo.23646104
UR - https://doi.org/10.5281/zenodo.23646104
AB - The openai/math release contains a Lean 4 proof (AI-generated, Comparator-accepted, not peer reviewed) that the triangular lattice minimises the lower g-energy among all locally finite planar configurations of density one, for every smooth completely monotone g of squared distance. This preprint applies it to the planar Yukawa interaction e^{-κr}/r, the 3D-screened Coulomb potential between particles confined to a plane (2D dusty-plasma and colloidal crystals). It is not the 2D Debye–Hückel Green function K0(κr), which is not treated. Every claim is filed in an Elenchus claim ledger (25 claims) with tiers A (kernel-checked Lean), L (verified literature), C (argument or human proof, not machine-checked) and X (floating-point exploration, never supporting a claim). Tier A, conditional on upstream's universal_energy_minimum and on the fidelity of its definitions (axioms within propext, Classical.choice, Quot.sound; planted sorry and planted-axiom controls caught; independent recompiles by separate AI agent instances): e^{-κr}/r is admissible for every κ > 0, so the triangular lattice minimises its energy at density one, and the minimum is finite; the same at every density ρ > 0 for the rescaled lattice (for a single κ this is a reparametrisation); the same for every finite mixture ∑ wi e^{-κir}/r with wi ≥ 0, κi > 0; negative controls: the admissibility lemma needs the sign condition on the weights; g1 − 2g2 is not admissible, so the theorem does not apply to it (this does not show that optimality fails for it). The mathematics is classical (complete monotonicity of the Yukawa potential in r²; completely monotone functions form a convex cone closed under products). Only the kernel-checked corollaries are new. A step-by-step human proof (Tier C) is given beside each Lean statement. Tier X: this corrects the truncation erratum recorded in doi:10.5281/zenodo.23295142 for the CVODE study of doi:10.5281/zenodo.23293429. With the exact, untruncated potential and a rigorous tail bound (rusty-SUNDIALS crate qf-yukawa-crystal), absolute energies move by the erratum amounts (1.77e-2 at κ = 1), while the square–triangular gap moves by only -2.2e-6. 24 published relaxed stages were re-relaxed under the exact potential, and none fell below the exact triangular energy beyond f64 resolution (one stage, the perfect lattice at κ = 1, sits at gap 0 within rounding). That is a subset of the published study, and annealing was not re-run. Controls: an independent 40-digit mpmath sum agrees to 1.7e-16; the published shifted-force values fail the agreement test; the square lattice is a saddle point. Hugging Face: no dusty-plasma or colloid particle dataset was found on the Hub. The OC20 shard used for the disordered initial conditions (colabfit/OC20_IS2RES_val_id, CC-BY-4.0) is matched by sha256 to revision 6a1dfef1. It supplies disorder, not physics. The Elenchus ledger gate exits 1 with 0 blocking findings and 11 flags. Each flag is a Tier A row whose statement adequacy no human has audited (only AI agents audited it). The work was produced by AI agents (Claude) under the author's direction; the author is responsible for the content. It has not been reviewed by human experts.
ER -