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.
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.