The Sandier-Serfaty triangular-lattice conjecture: an independent reproduction of a claimed finite certificate, an adversarial audit of the claimed reduction, and a Lean statement (no proof of the conjecture is claimed)

The Sandier–Serfaty conjecture asks whether the triangular lattice minimizes the renormalized Coulomb energy W of a point set in the plane against a uniform neutralizing background. A preprint in the openai/math release (AI-generated, not peer reviewed) claims a proof by a reduction to square tori plus a finite certificate in exact interval arithmetic. This work does not prove, verify or refute that claim and is not peer review. Every claim is filed in an Elenchus claim ledger with tiers A (kernel-checked Lean), L (cited literature, statements read on the cited page, proofs not re-checked), C (argument not machine-checked) and X (computation, never supporting a mathematical claim by itself). Tier X – independent reproduction of the finite certificate. The unchanged C++ certificate was re-executed on a different toolchain and host (g++ 11.4.0, Boost 1_74, Python 3.10.12 instead of g++ 13.3.0, Boost 1_83, Python 3.12.13): wrapper exit 0, terminal OK, stage validation passed, source hashes unchanged, and all 22 printed integer pairs equal the saved record. Three one-line loosenings of the certificate were run on copies as negative controls: two are rejected by the program's own assertion, one passes; the outcomes of the last two were predicted in writing before they finished, while the fitted break-even multipliers (about 22.6 for the midpoint constant, 1.86 for the Lipschitz allowance of the negative-part assertion) were fitted to coarsened printed pairs and are not blind. The reproduction rests on the manuscript's analytic bounds and tests none of them; runtime trust is assumed. Tier C – adversarial audit of the reduction (by an AI agent). Sections 2–5 of the manuscript were re-derived step by step (31 numbered steps and 14 certificate-stage rows): no step was classified as a gap, with stated limits: the spline pieces outside [p, R0] and the grid-stage values rest on code reading only, no negative control exercised the Hessian stage, the internal proofs of the cited Sandier–Serfaty and Bétermin–Sandier results were not re-checked, and a strong minimum principle used by the manuscript has no verified reference. Independent exact-rational and 45-digit re-computations (calibration identity 6K+λ+2πμ = W(E_tri), λ, μ, K, B(ℓ), tail constants) agree with the certificate's printed values, with negative controls falling outside. Tier A (non-degeneracy only) and Tier C (fidelity) – a Lean statement. The conjecture is stated as Lean Props (manuscript normalization, explicit value, and the original SS2012 normalization). Ten non-degeneracy lemmas are kernel-checked (Lean 4.34.1, Mathlib d13f23b7; axioms within propext, Classical.choice, Quot.sound; planted sorry and planted-axiom controls are caught); the statements themselves are not proved, their fidelity to the manuscript and to SS2012 is a Tier C comparison, and the existence of the puncture limit, the inhabitation of the triangular side and the equivalence of the two normalizations are not formalized. LeanFlow improvement. A Lean data-certificate generator, fail-closed for the sources it renders itself (88 tests pass), turns printed interval data into Lean-checked integer arithmetic; it accepts the 13 inequalities about the positive run's printed pairs and rejects 3 of 10 about the loosened run's. Its Tier A covers the arithmetic on the printed integers only. An independent audit found that the exported checker for arbitrary Lean sources was fail-open (a source using #exit and a forged axiom report was accepted); it is fixed with a per-run sentinel and an #exit refusal, with new tests, and the generator's results were re-run unchanged. The checker is not a sandbox. The step that would conclude the conjecture from the manuscript's analytic bounds, the cited results and the certificate run is stated only conditionally. The Elenchus ledger gate reports 0 blocking findings and 7 flags (exit code 1), one LEDGER_UNAUDITED_TIER_A for each Tier A row. Everything resting on the openai/math manuscript is conditional on it. The work was produced by AI agents (Claude) under the author's direction; producer, auditor and re-compiling agents are instances of the same AI pipeline, no human has audited the statements, the audit or this text, and the author is responsible for the content.