Certified sign classification of the second variation of the harmonic zero-point energy for Gaussian interactions on a in [0.425, 4]: not a local minimum for a in [0.425, 1.579] and a strict minimum along the shear for a in [1.584, 4] (partial result; the full iff for all a > 0 is not claimed)

For the planar Gaussian pair potential V(r) = e−π a r2 let E(a, t) be the harmonic zero-point energy per particle (ℏ = m = 1) of the unit-covolume Bravais lattices Lt = Pt Lρ, Pt = [[1, t], [t, 1 + t2]], sheared from the triangular lattice Lρ, and F(a, t) = ∂t2E(a, t) its exact second variation (not the majorant of the earlier B2 preprint, which cannot reach the sign changes). F is enclosed two-sided by ball arithmetic, in a form affine in a that lets intervals be chained, for every a in an interval and every |t| ≤ 10−8. Result. F < 0 on all of [0.425, 1.579] (71 chained intervals) and F > 0 on all of [1.584, 4] (103 chained intervals). Hence along the shear the triangular lattice is not a local minimum of the zero-point energy for every a in [0.425, 1.579] (E(a, t) < E(a, 0) for 0 < |t| ≤ 10−8), and E(a, 0) < E(a, t) for every a in [1.584, 4], a strict minimum along the shear. A strict local minimum over lattice shapes additionally needs C2, criticality, isotropy (order-3 stabiliser) and the two-dimensional second-derivative test, which are written arguments and not formalised. Each of (0.3745, 0.379) and (1.579, 1.583) contains a zero of a ↦ F(a, 0) (intermediate value theorem); uniqueness, and the absence of other zeros in the uncertified gaps, are not certified. Left of the first root only isolated points are certified (F > 0 at a = 0.33, 0.35, 0.36, 0.37, 0.372, 0.3745). Not claimed. The full equivalence between local minimality and a above the larger root, for all a > 0, is not claimed and is probably false: the earlier preprint P2 sees another sign change near a = 0.123 (Tier X). The intervals in (0.383, 0.425) and everything below 0.33 are not certified; at a = 0.25 and a = 0.30 the certifier could not prove det B > 0 (104 and 9 failed cells near Γ). Nothing is claimed for a > 4, other potentials, other lattices, three dimensions, or the total (classical plus zero-point) energy. Tier split. Tier A (Lean 4.34.1, Mathlib; axioms within propext, Classical.choice, Quot.sound): the logic, the signs of 197 rational records, the interval-chain coverage (decide +kernel), the intermediate-value step and the window lemmas; the assembled theorems take the enclosures as explicit hypotheses. Tier C-ball: the Arb enclosures (python-flint 0.6.0, 96 bits; 1,276,022 certified cells over 202 distinct run records, 0 failed), not kernel-checked. Tier C-human: that F is the second derivative of E (so E is C2 in t), the mirror symmetry, continuity in a, and the isotropy and second-derivative steps for the strict claim over shapes. The headline is therefore Tier C overall; only its logic and arithmetic are Tier A. Controls. Just inside the window at a = 0.40 (negative enclosure; the kernel rejects a claimed local minimum), a tampered certificate (rejected), intervals straddling each root (no sign certified), a planted false sign in the unmodified LeanFlow certifier (rejected) with 197 true signs verified, planted sorry and planted axiom (caught by the axiom gate), and a floating-point cross-check at 609 points (0 misses). Status. Produced by AI agents (Claude) under the author's direction; the author is responsible for the content. An independent AI audit (producer != verifier, 2026-10-26) returned ACCEPT_WITH_CORRECTIONS with no blocking item; its corrections are applied in this version. No human has audited the work or the Lean statements, and there is no statement lock. Kernel replay (leanchecker, Lean 4.34.1, auditor-built oleans) is rc 0 for Programmes.ZeroPointClass.Cert, Controls, Honest and Basic, and for the imports ZeroPoint.Basic and ZeroPointCert.Basic. The Elenchus ledger gate exits with code 1 (0 blocking findings, 8 flags LEDGER_UNAUDITED_TIER_A, one per Tier A row). The repository guards antigravity_guard.py and test_rigor_guard.py fail for reasons that predate this work and are reported in the paper.