A certified finite reduction for Lebesgue's universal covering problem

Lebesgue’s universal covering problem asks for the least area of a convex set that contains a congruent copy of every planar set of diameter one. Every lower bound for it is a computation that replaces a continuum — of orientations, translations and candidate covers — by finitely many samples, and is a theorem only if each replacement carries a proved error term. We give the whole chain from the problem to finitely many checkable inequalities, with every error term explicit: the reduction to bodies of constant width one, with the mirror branch shown to be necessary; an exact linear-programming certificate for one target in one cover, with a two-sided bracket; finite dictionaries of targets and of covers with proved Hausdorff and area errors; the completeness of finite families of targets, with an exact second rung; the exchange of witness bodies; a conditional lift certificate whose finitely many boxes are closed by common cores; and the cost of such a certificate — how fine its boxes must be, which prune closes wider boxes, and the depth a positive margin needs. Every step was checked by an independent recomputation and is stated at the strength that check measured. The paper proves no bound on the covering constant itself, and lists the corrections found on the way, among them two audit constants taken from a grid on the unsafe side and a certificate specification with no place for mirror-image placements.

Not claimed anywhere in this paper: any value or bound for Lebesgue’s universal covering constant \(a_{\mathrm{Leb}}\) — the universal covering problem itself is open, and this paper is the machinery a certified bound would pass through, not a bound; the published bounds \(0.8344\) and \(0.8440935944\), which are cited, not verified; the target \(0.835\) of the research programme this framework was built for; and any statement about which finite family of test bodies is best.

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 the rounds of the finite-closure line from which this framework comes, and the deep lagged audits of its cover compiler, on the programme Neo.K set out. Every statement this paper attributes to “the programme” is from those documents.

Neo.K set out the research programme: the finite-closure strategy, its target, and the methodology of deep lagged multi-pass verification under which the audits of §5.5 were run.

懸衡 (Xuán Héng) — the independent recomputation; model: Claude, Opus series — did the twelve runs this paper names and wrote this paper: every COMPUTED_HERE figure rebuilt with independently written code, never by running the programme’s scripts; every theorem-level step read against its source; the drills of §12; and the additions marked as the recomputation’s where they occur — the counterexamples of Theorem 2.4 and Proposition 3.7, the analysis of the test instance in §3.6, the proof of Proposition 6.4, the sharper constants of Proposition 6.3 and Proposition 8.3, the moment comparison of §4.2, the measurements of §9.4, the second part of Proposition 9.6, 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 — reporting issues, none mathematical — 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. His two suggestions — the margin function’s name in the proof of Theorem 7.1, and the convention for a vertex inside the disc in Proposition 6.4 — were applied.

Priority, stated plainly. The framework is the programme’s. What is offered as this line’s own is narrower: an independent check of every step of it, the strength at which each step stands, the few sharpenings and counterexamples listed above, and the corrections. The theorems it cites are other people’s. The programme as a whole — its target \(0.835\), its ledger of closed and open cells, and where it stopped — is reported in a companion paper [1]; this paper can be read without it.