The triangular lattice is not a local minimum of the harmonic zero-point energy for Riesz s = 3 and dipolar potentials, certified with an Ewald split

For a radial pair potential and unit-covolume planar lattices, let E(t) be the harmonic zero-point energy per particle (hbar = m = 1) along the symmetric shear Lt = Pt Lρ that starts at the triangular lattice. An earlier preprint (N2, doi:10.5281/zenodo.23663551) certified E(t) < E(0) for two Yukawa potentials but could not treat r−3 tails, because the real-space lattice sums converge too slowly. Here an Ewald split (a fast-decaying real-space part and a smooth Fourier part) removes the obstacle, and we certify E(t) < E(0) for every 0 < |t| ≤ 10−5 for seven potentials: Riesz r−3; the bilayer point dipole 2(1/r − 1/√(r²+d²))/d² at d = 1/10 and d = 1/2 (N2 covolume units); and at the four preregistered ratios d/a = 0.06, 0.09, 0.1, 0.5. So the triangular lattice is not a local minimum of the model's harmonic zero-point energy over lattice shapes for all seven. The hoped-for first certified positive (local minimum) statement for an r−3 potential did not happen: all seven signs are negative. What this is not. Not a statement about real excitons, bilayers, moiré devices or any material; no melting, no structural transition, no instability claim; not a global statement. It concerns the harmonic zero-point energy of a model crystal in model units. Tier split. Tier A (Lean 4.34.1, pinned Mathlib; the theorems of Programmes.ZeroPointDipolar.Basic, namely the logic and the signs of rational endpoints; the generic window lemmas are N2's ZeroPointPhys and are reused; axioms within propext, Classical.choice, Quot.sound, e.g. 'ProgZeroPointDipolar.riesz3_not_localMin_of_certificate' depends on axioms: [propext, Classical.choice, Quot.sound]; leanchecker replay rc 0, run by the producer and re-run by an independent AI auditor; the final theorems are conditional on the non-kernel inputs). Tier C-ball (Arb ball arithmetic, not kernel-checked): enclosures of the window curvature M for the seven potentials ([-3.17029, -1.66310] for Riesz 3; [-3.33620, -1.85185] and [-5.38812, -4.11598] for d = 1/10 and 1/2; [-3.23699, -1.74649], [-3.32496, -1.84069], [-3.36115, -1.88023], [-5.49473, -4.24958] for d/a = 0.06, 0.09, 0.1, 0.5), each containing the Tier X value of E''(0); the Ewald-split certificate (short part in real space with incomplete-gamma closed forms and N2's shell tail lemma at Qmax 300; long part in reciprocal space with the exact Fourier transform 4 sqrt(pi alpha) exp(-x²/(4 alpha)) − 2 pi x erfc(x/(2 sqrt(alpha))), the k = 0 term and the first shell exact, the rest by rigorous Cauchy-estimate balls of at most 1.6e-10). Tier C-human: the written glue inherited from N2 and the new Ewald items (mixture representation, Poisson summation, Cauchy estimates, Voronoi integral lemmas). Tier X: floating-point scans and Lindemann ratios in model units. Controls. Positive: Gaussian a = 1 [-8.23325, -7.15778]; Gaussian a = 2 and Yukawa kappa = 2 bit-identical to N2; Yukawa kappa = 1 [-4.16485, -2.03702] contains N2's interval but is not bit-identical; Ewald-specific point checks against an independent direct float sum. Negative: Gaussian a = 2 (M in [+3.4496, +4.4631]) not certified; r−3 without the split refused by the tail lemma; a false Lean certificate fails to compile (rc 1); planted sorry and axiom caught by the axiom gate. Weakness: the producer run had no negative control of the reciprocal-space code. The independent audit added one: corrupted transforms are detected far beyond the ball radii, and a known Gaussian is reproduced through the Poisson code. No corruption confined to the reciprocal code flips the sign, because that part contributes only about 1e-2 to E''. Status. Written by AI agents under the author's direction. An independent AI audit (a separate AI agent instance, producer ≠ verifier; verdict ACCEPT_WITH_CORRECTIONS, corrections applied) re-ran the kernel replay of the whole import chain (five modules, leanchecker rc 0), re-derived the Ewald formulas, recomputed E(0) and E''(0) for all seven potentials by two independent methods (Tier X; all inside the enclosures, all negative) and added a negative control for the reciprocal-space code. It did not independently re-derive the M enclosures, which remain the producer's Tier C ball arithmetic and depend on N2's certifier. No human audit exists. No statement lock. Claim ledger gate: exit code 1, 0 blocking findings, 4 flags (one per Tier A row: no person has certified the statements). Not peer reviewed.