The triangular lattice is not a local minimum of the harmonic zero-point energy for exp(-pi r^2): a certified linear-response majorant along a symmetric shear

For the Gaussian pair potential V(r) = exp(−π r2) 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. The proof bounds E above by a majorant U that is affine in the dynamical matrix (a tangent form of the concavity of tr√·) and certifies that the second difference of U is at most −1.84156 t2. This is an upper bound on a curvature, not a two-sided enclosure of the Laplacian of Ezp at the triangular point. Tier split. Tier A (Lean 4.34.1, Mathlib; axioms within propext, Classical.choice, Quot.sound): the 2×2 concavity inequality, the logic (a majorant window bound with a negative constant excludes a local minimum), the rational certificate (Upp0_hi + trW_hi·esum_hi < 0 and a positive stability margin) and the assembled theorem, whose analytic inputs are explicit hypotheses; planted-sorry, planted-axiom, tampered-certificate and a = 2 controls are caught or rejected. Tier C-ball: the Brillouin-zone integrals, lattice sums and tails are rigorous Arb ball-arithmetic enclosures (206,468 cells, 0 failed) computed with python-flint; they are not kernel-checked. Tier C-human: the glue (E ≤ U after integration, the window identity, mirror symmetry, identification with the earlier Ezp). The headline is therefore Tier C overall; only its logic and arithmetic are Tier A. A corollary Lap Ezp(ρ) ≤ −0.92078 needs extra hypotheses (E of class C2; Ezp of class C2 near ρ; ρ critical and the Hessian isotropic, both by the order-3 stabilizer, P2 3.1) and is Tier C-human. A negative control at a = 2 (where the triangular lattice is a local minimum) is not certified, as it must be; the same certificate also works at a = 1/2, which was not preregistered. Deviation from the preregistration. The preregistered item asked for a certified, Lean-checked negative Laplacian of Ezp at a = 1; that two-sided statement is not established (a direct certified enclosure of E″(0) with the same Duffy machinery appears feasible and is left open). The window is small (10−5), the path is one shear, and the setting is harmonic, Bravais, two-dimensional. Status. Produced by AI agents (Claude) under the author's direction; the author is responsible for the content. An independent adversarial audit by a separate AI agent instance (AUDIT.md, verdict ACCEPT_WITH_CORRECTIONS) recompiled the Lean files, re-ran the ball arithmetic with coarser cells and re-implemented the quantities in floating point; its corrections are applied (REVISION.md). The main theorem statement is locked in results/proposal2/2026-10-26/B2/STATEMENT_LOCK.json. No human has audited the work or the Lean statements. The Elenchus ledger gate still exits with code 1 (0 blocking findings, 8 open flags, one per Tier A row): the gate clears LEDGER_UNAUDITED_TIER_A only for a human audit, so the AI audit is recorded in a separate ai_audit field and the flags stay open. The repository guards antigravity_guard.py and test_rigor_guard.py fail for reasons that predate this work and are reported in the paper. The main-run text log of the a = 1 run was not archived.