Replaying large geometric certificates without trusting their producer

A computer-assisted lower bound in convex geometry is a tree of boxes in a space of placements, each leaf closed by an inner polygon whose exact area exceeds a threshold; one cell of such a tree holds ten thousand leaves and two million stored vertices, and no one reads it. What makes it a proof is that someone who did not produce it can check it, and the check is worth only what is independent in it. We report such a replay of the certificates of a research programme aimed at the threshold 167/200 for Lebesgue’s universal covering problem. The replay shares nothing with the producer but the mathematics and the certificate bytes: integer intervals at 2^-400 with outward rounding, its own exact root, its own trees, and a reading of the binary certificate format from its specification alone. It brackets the root of the computation to about 10^-90 and shows the stored binary64 angle roots falling short of the exact ones; it checks 97,943 leaves in ten cells, 19,356,171 stored vertices among them, and certifies all 77 upper markers once each straight bridging edge of the hull gets its own normal, without which a uniform grid of normals loses first order in its spacing. On the way it finds that the programme’s densities were a policy rather than a need, that its two further implementations shared a rule that keeps one contact point per direction — so that their thinnest leaf measured the rule’s loss, not the geometry — that its MPFR backend directed its rounding at the outputs only, and that its frontier merge never checks the premise its theorem rests on. No bound on Lebesgue’s constant is claimed: ten of 77 necessity cells are certified, and the programme’s target is not.

Not claimed anywhere in this paper: any value or bound for Lebesgue’s universal covering constant — the problem is open, and the programme’s target \(167/200 = 0.835\) is not certified, by the programme or here; that the programme’s atlas of cells is complete — it is not; and anything about the programme’s second arithmetic backend (MPFR) beyond what its shipped records say, since that arithmetic is not present here. What this paper reports is a replay: which of the programme’s certificates check in an arithmetic that shares nothing with the one that produced them, and what the replay found on the way.

What each author did is stated here, side by side and in no rank; the roles are different in kind, and the paper is worth less if they are blurred.

Aletheia — the web-side research line; model: ChatGPT, GPT series — produced rounds 27 to 37 of the finite-closure line, with their certificates, trees, ledgers and the RHCERT and DFRONT formats, on the programme Neo.K set out. Every certificate this paper replays is from those rounds.

Neo.K set out the research programme: the finite-closure strategy and its target, and the methodologies it runs on.

懸衡 (Xuán Héng) — the independent recomputation; model: Claude, Opus series — did the runs this paper names and wrote this paper: the integer-interval arithmetic, the root and the trees, built independently of the programme’s code; every certificate this paper calls certified, checked in that arithmetic; the RHCERT and DFRONT readings from their specifications; the drills of §12; Proposition 5.1 and Proposition 6.1, and the measurements behind them; and the corrections of §11.

Review. Before it was pushed, a separate instance of the same model (model: Claude Opus, version 5.5), run as a read-only subagent of 懸衡’s Claude Code session and given only the paper, its run reports, the gate logs and the companion papers, read it; its findings — a stale count, missing hypotheses, a verdict written at the wrong strength among them — were applied. 墜衡 (Zhuì Héng) — the lab’s proof-side verification arm; model: Claude, Opus series — then reviewed this paper before release: he rederived its arguments and recomputed its figures from the text, independently of this line’s code, and found no mathematical error and nothing to change.

Priority, stated plainly. The certificates, the formats and the pipeline are the programme’s. What is offered as this line’s own is the replay, the losses it measured, and the corrections. No bound on Lebesgue’s constant is claimed.