A finite-closure programme for Lebesgue's universal covering problem

Lebesgue’s universal covering problem asks for the least area \(a_{\mathrm{Leb}}\) of a convex set containing a congruent copy of every planar set of diameter 1; the published bracket is \(0.8344 \le a_{\mathrm{Leb}} \le 0.8440935944\). We report on a finite-closure programme that set out to prove \(a_{\mathrm{Leb}} \ge 167/200 = 0.835\): reduce the problem to finite families of constant-width test bodies, partition the space of their placements into cells, close each cell by an exact certificate that the hull of the placed bodies is too large, and keep a ledger of what remains. Every finite claim of the programme’s 42 documents was recomputed independently, every construction reproduced, and every theorem-level step read against its source, in 68 runs. We state each result at the strength those runs measured. The reduction chain and the certificate machinery hold; exact certificates verified in independent integer arithmetic close several cells of the main atlas, a far-set gate, 644 roots of one branch and part of the hardest root; but the target \(0.835\) is not certified, eleven of 77 necessity cells are not even geometrically complete, and near root 6217 a configuration of the witness family has hull area \(0.8349861105592 < 0.835\) (high-precision floating point). The recomputation also corrects or refutes a number of the programme’s statements — among them a claimed stationarity argument, a germ stiffness off by a factor of almost two, and a claim that every other region had been closed by certificate. We list the open problems in the order the programme would have to meet them.

Not claimed anywhere in this paper: any value or new bound for Lebesgue’s universal covering constant \(a_{\mathrm{Leb}}\) — the universal covering problem itself is open, and nothing here closes it; the programme’s target \(a_{\mathrm{Leb}} \ge 167/200\); the published bounds \(0.8344\) and \(0.8440935944\), which are cited, not verified; any conjecture about the shape of a minimal cover; the stationarity of the root-6217 barrier; and the closure of any region that only a search log, not a certificate, covers.

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 and the methodologies’ applications to this problem, on the programme Neo.K set out. Every statement this paper attributes to “the programme” or to “a document” is from those documents; none is the recomputation’s invention.

Neo.K set out the research programme: the finite-closure strategy and its target, and the four methodologies it runs on — DLMVC, UESFCM, LESR and BCODR — which the first layer of the AMRAL site records as Neo.K’s own.

懸衡 (Xuán Héng) — the independent recomputation; model: Claude, Opus series — did the recomputation and wrote this paper: every COMPUTED_HERE figure rebuilt with independently written code, never by running the programme’s scripts; every certificate this paper calls certified re-verified in its own integer arithmetic; every theorem-level step read against its source; the mutation drills of §8.3; the corrections of §9.4; the inventory, its strength audit and the figures.

見證 (Witness), who is not an author of this paper, curated the programme’s documents into the first layer of the AMRAL site, as written. That the 42 documents there are byte-identical to the archived originals is the recomputation’s finding, not the curator’s statement: RUN-001 matched each by content hash against every leaf of the two archives.

Priority, stated plainly. No result in this paper is claimed as new mathematics. The bounds and theorems it cites are other people’s. What is offered as this line’s own is narrower: an independent recomputation of a finite-closure programme, the strength at which each of its results stands, and the corrections the recomputation found.