III · Crystallization

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.

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.

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.

The published lower bound 0.8344 for Lebesgue’s universal covering constant is a certified computation on three test bodies, the disc and the Reuleaux triangle and pentagon. Does a fourth, the Reuleaux heptagon, raise their value? By the exchange theorem it does if the heptagon misses every minimizing cover of the three. A research programme set out to prove this by two gates: near the located optimum, the heptagon misses the optimal hull by a margin; far from it, every configuration of the three bodies has hull area above the three-body ceiling. We report how far the programme’s certificates go, each replayed by an independent recomputation. The near gate holds, by a finite dual certificate re-enclosed in 400-bit integer intervals, though its shipped verifier skips two premises the bound rests on. The far gate is not certified: in the branch the programme attacks, 644 of 22,516 frontier roots are closed by erosion certificates whose 56,149 area leaves all hold in exact arithmetic, and at the hardest root six more certificates hold, 182,438 area leaves in all; but a symmetrization there drops the branch’s own constraint, leaving one side of a slice uncovered, and 14.6 % of that root’s box, inside the branch, was closed only by a search. The least configuration found in that root, located to 80 digits, has hull area 0.834986110559224, above the ceiling by 2.05e-4, so the far gate holds there numerically. The far set does hold configurations with hull area below 0.835, numerically, the programme’s headline target; so this route, which uses the heptagon only near the optimum, cannot certify 0.835 without lifting a witness far from it as well. We also give what holds of the programme’s local analysis of the hardest root’s configuration: its conclusions numerically, several of its arguments not as given. No bound on the constant is claimed.