The July 2026 Darvas–Peng–Tao manuscript solving Erdős–Herzog–Piranian (1958) defines its extremal constant D from the unique zero of a 3-dimensional nonlinear system. This page re-verifies the computational fragment in independent arithmetic — existence AND local uniqueness of the zero by the interval Krawczyk operator, a refinement to width < 10⁻⁴⁰, and a digit-for-digit audit of every decimal expansion the manuscript prints. All of it re-ran during this build: 26 checks green, 4 mutation controls rejected, verdict CONFIRMED.
An independent re-verification that lands just inside the manuscript's own box would confirm very little. These enclosures are narrower than that box by fifteen orders of magnitude, which is what makes the printed decimals decidable rather than merely consistent.
1 — Every constant the manuscript prints checks out. The p.24 block — q*, u*, v*, p*, α, r*, z*, and D to 18–19 decimals — matches the certified enclosures as exact truncations. The extremal value is real, unique in its box, and printed correctly.
2 — The headline D on p.2, printed to 30 decimals ending “…635125…”, is not an expansion prefix: the true expansion continues …6351247861…, so the 30th decimal of the expansion is 4, not 5. The printed value is a correct half-up ROUNDING, accurate to under 5·10⁻³¹ — but a trailing ellipsis conventionally promises an expansion. Not an error in the mathematics; a presentation defect only certified digit arithmetic can even see. (The same half-ulp class appears in the Erdős #852 audit — it is the benign end of the failure taxonomy named there.)
The verifier re-derives everything from the manuscript's Appendix A definitions alone: consistency of the displayed derivatives with automatic differentiation; the certified face inequalities on the box B*; existence and LOCAL UNIQUENESS of the zero by the interval Krawczyk operator (a genuinely different route than the manuscript's scalar intermediate-value argument — Lemma A.1 confirmed both ways); containment of B* in the uniqueness box, so the manuscript's triple and ours are the SAME zero; and a BigInt fixed-point refinement to width < 10⁻⁴⁰ with directed rounding and explicit series tails. The authors' python-flint/Arb scripts were read for scope only — no line of theirs runs here, and no numeric value of theirs enters except the CLAIMED decimals under audit.
New in this rebuild: the verifier now runs against THIS repository's interval instruments (instruments/interval/, the lifted eqcert toolkit) staged at the core/interval path it searches for — a second implementation substrate reaching the identical verdict, re-established on every build.
That D is the INFIMUM — the entire proof of the paper's Theorem 1.1 (normal form, forcing lemma, dual measure construction, endpoint certificate, sharpness) — was not audited: this page verifies the DEFINITION of D and its claimed digits, not its extremality. Also unchecked: the manuscript's other Arb and SymPy certificates (read for scope only), the authors' own κ sign-change proof of Lemma A.1 (the Krawczyk route replaces it; the lemma itself is confirmed), and the AI-use chronology. A verification note that does not draw this line invites the reader to assume more than was checked.
This page supersedes the one cited in the Erdős #1038 GitHub issue (Pengbinghui/pipeline-math#5, 2026-08-05); that page is preserved byte-identically in the repository (the citation path 301s here), beside the verifier itself — hash-pinned through this repository's lift provenance. Re-run it from the repository: node tools/build-report-lemniscate.js rebuilds this page and refuses unless the verifier is green.