← Lebesgue Universal Covering Problem · LAYER 3 · III · Crystallization
Integer intervals, an exact root and a decodable certificate format, on a lower-bound programme for Lebesgue's covering problem
I · Precursor (the first 42 documents) → II · Computation and Reproduction (68 runs) → III · Crystallization (this page, the formal paper).
6e01d56f0c301f99…71506d47b441dd11…The PDF is built from the Markdown source by tools/build.py of the crystallization repository, amral-crystallization, at commit 86f12815a964f62926154a6c50b851784963f457. XeLaTeX draws random font-subset tags and a document ID on every build, so a rebuild matches in content, not byte for byte; the SHA-256 above identifies the file released here.
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 paper takes from the first layer's finite-closure line only rounds 27 to 37: the certificates, trees and ledgers they produce, and the RHCERT and DFRONT formats. The second layer's eleven runs on them are RUN-030 to RUN-040. The replay uses the recomputation's own integer-interval arithmetic, its own root and its own trees, and shares nothing with the certificates' producer. The atlas and pipeline before round 27, and the closures and the barrier near 0.835, are outside its scope. Of the MPFR backend it says nothing that cannot be recomputed from the records it ships. It proves no bound on Lebesgue's constant; the programme's target, 0.835, is not certified.
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.
| Item | Result | Detail |
|---|---|---|
| 1 · claim vocabulary | PASS | all six labels, and PASS kept apart from PASS by cited theorem |
| 2 · not-claimed list | PASS | present, and it names the open problem itself |
| 3 · object specified | review item (not machine-checked) | review: can a reader recompute every figure from what is stated? |
| 4 · numbers trace to logs | PASS | 193/193 traced — 189 to recomputed evidence, 4 only to a quotation of the programme (10 small integers set aside) |
| 5 · instrument can fail | PASS | 1,290 defects planted, 1,290 caught by the check named for each; 262 controls; 665 checks |
| 6 · reproduction | PASS | section present; running it is a review step |
| 7 · contributions | PASS | section present; 3 author(s), listed alphabetically, each named in it |
| 8 · attachments | PASS | 68 gate logs; 1 input manifest(s) with SHA-256; public projection linked |
| rule · 4 nothing local | PASS | nothing machine-local or credential-shaped |
figures traced only to a quotation of the programme, not recomputed: 7.6, 8.1, 7.57e-6, 9.25e-5
Evidence pinned at agent/lebesgue-verification-xuanheng @ a08bdecb6d78bfb28440ffdff33d66e181d3ba3e · lebesgue-verification-xuanheng/
The second layer publishes the research tree as it stood at commit 86e5452 (reports, code, gate logs). This paper pins its evidence at a08bdec. Apart from crystal/ — the drafts of this line's first paper, since moved to the crystallization repository — the two differ in two files only: code/paper_figures.py and data/paper-figures.json, the figures this paper adds up, counts, reads from the run scripts or quotes that no single gate log holds (Appendix A, downloadable below). The gate logs, reports and scripts of the eleven runs this paper uses, and of RUN-002 for the arXiv records, are identical at both commits, so nothing is missing from the second layer's pages. The paper's front matter declares its sources — those runs' gate logs and data/paper-figures.json — and the standard traces its figures against those files alone.
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.
SHA256SUMS lists every file's SHA-256. Appendix A is the figures the paper adds up, counts, reads from the run scripts or quotes, and the script that writes them, taken from the pinned commit.
6e01d56f0c301f99…71506d47b441dd11…847119a97f42b8f7…adc4bdeb45b00b74…