The triangular lattice is not a local minimum of the harmonic zero-point energy for planar Yukawa potentials kappa = 1, 2: classically optimal (H2, conditional), not zero-point optimal, a certified partial result via a moving comparison matrix with exact curvature; Riesz s = 3 and dipolar potentials not certified

For the planar Yukawa pair potentials V(r) = e−κr/r with κ = 1 and κ = 2 and unit-covolume planar Bravais lattices, let E(t) be the harmonic zero-point energy per particle (ℏ = m = 1) along the symmetric shear Lt = Pt Lρ, Pt = [[1, t], [t, 1 + t2]], starting at the triangular lattice. We show that E(t) < E(0) for every 0 < |t| ≤ 10−5, so the triangular lattice is not a local minimum of the zero-point energy over lattice shapes, although it is the classical (static) energy minimiser for these potentials (conditional: cited from an earlier preprint, H2, which is itself conditional on an upstream Lean theorem and is not re-checked here). The linear-response majorant of the earlier Gaussian result cannot give this: its curvature is certified positive here ([2.393, 2.464] and [2.688, 2.723]). The proof uses a moving comparison matrix Xt = D01/2 + tY with XY + YX = D0′; the majorant U2 satisfies U2 ≥ E, U2(0) = E(0) and U2″(0) = E″(0) exactly, and a window bound gives U2″ ≤ Mhi < 0 with Mhi = −2.03704 (κ = 1) and −1.86854 (κ = 2). Per potential. Yukawa κ = 1: certified. Yukawa κ = 2: certified. Riesz r−3 and dipolar d = 0.1, 0.5: not certified; the obstacle is the slowly decaying r−3 lattice-sum tail (a bound on the annulus [Rc, 2Rc) of about 6800/Rc, against a stability margin near 3.8; an Ewald-type remedy is scoped, not attempted), and nothing is claimed for them. Riesz r−4: not attempted; Tier X evidence only (finite-difference E″(0) = +2.754 along the shear, cutoff 40/100) that the triangular lattice is a local minimum for s = 4, not certified in either direction; the earlier refutation was global, via a far competitor, so this is a deviation from the preregistered item. Two of the six preregistered potentials are certified. Tier split. Tier A (Lean 4.34.1, Mathlib; axioms within propext, Classical.choice, Quot.sound): a window lemma (f″ ≤ K on [−t, t] implies f(t) + f(−t) − 2f(0) ≤ t2K), the logic (a majorant window bound with a negative constant excludes a local minimum), the rational certificates and the assembled theorems, whose analytic inputs are explicit hypotheses; planted-sorry, planted-axiom and a false Gaussian a = 2 certificate are caught or rejected. Tier C-ball: the Brillouin-zone integrals, lattice sums and tails are rigorous Arb ball-arithmetic enclosures (86,581 cells for the two Yukawa runs, 0 failed) computed with python-flint; they are not kernel-checked. Tier C-human: the glue (majorant inequality after integration, exact curvature, differentiation under the integral, mirror symmetry, identification with the earlier Ezp). The headline is therefore Tier C overall; only its logic and arithmetic are Tier A. Controls: Gaussian a = 1 certified (positive), Gaussian a = 2 rejected by the certifier, by LeanFlow and by the Lean kernel (negative). A side result Lap Ezp(ρ) in [−2.0824, −1.0185] (κ = 1) and [−1.6088, −0.9343] (κ = 2) needs extra hypotheses (Ezp of class C2, ρ critical with isotropic Hessian) and is Tier C-human. Scope. Local window 10−5, one shear path, harmonic approximation, Bravais lattices, two dimensions. Status. Produced by AI agents (Claude) under the author's direction; the author is responsible for the content. This version has been independently audited by a separate AI agent (verdict ACCEPT_WITH_CORRECTIONS, no blocking item; report AUDIT.md) and applies its corrections (REVISION.md). No human has audited the work or the Lean statements, and there is no statement lock. Kernel replay (leanchecker, Lean 4.34.1) of Programmes.ZeroPointPhys.Taylor, Programmes.ZeroPointPhys.Basic and Programmes.ZeroPointCert.Basic: rc 0 (data/leanchecker_replay.json); replay does not check axioms, the #print axioms audit does. The Elenchus ledger gate exits with code 1 (0 blocking findings, 8 flags LEDGER_UNAUDITED_TIER_A, one per Tier A row, because they ask for a person); it was re-run after the AI-audit field was filled. The result concerns the zero-point energy alone: the classical energy has positive curvature at the triangular lattice, so nothing follows for the total energy at small hbar and no structural transition is claimed. The repository guards antigravity_guard.py and test_rigor_guard.py, and pytest tests/, fail for reasons that predate this work and are reported in the paper. Code docstring errata are stated in the paper.