---
title: "Does the Reuleaux heptagon raise the three-body value? A far-set route and how far its certificates go"
subtitle: "An exact gate, erosion certificates in exact arithmetic, a gate that is not established, and a configuration below 0.835, on Lebesgue's universal covering problem"
author:
- "Aletheia — research rounds and applications; model: ChatGPT, GPT series"
- "Neo.K — AMRAL Research Lab"
- "懸衡 (Xuán Héng) — AMRAL Research Lab, recomputation; model: Claude, Opus series"
date: 2026-10-18
version: "0.1"
standard: "1"
evidence:
branch: agent/lebesgue-verification-xuanheng
commit: 563fbd2f3fdf8249320fe94c2f6fbf48da82a941
dir: lebesgue-verification-xuanheng
sources: "data/external/uesfcm-*.json, data/gate-logs/run002-*.json, data/gate-logs/run009-*.json, data/gate-logs/run04[3-9]-*.json, data/gate-logs/run05[6-9]-*.json, data/gate-logs/run06[01]-*.json, data/paper-figures.json"
abstract: |
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.
keywords: [Lebesgue universal covering problem, Reuleaux polygons, computer-assisted proof, exact arithmetic, certificate verification]
---
> **Status of this document.** Preprint, version 0.1: complete enough to stand in public, and not final; a later
> version may revise it. Not prepared for journal submission. Section 11 records who did which part.
## 0. What is claimed, and what is not
Every statement in this paper carries a status, given after it in italics. A statement with a proof carries a
verdict on that proof. `PASS` and `PASS by cited theorem` are different verdicts and are never written as one: the
first is a proof checked line by line, the second a proof one of whose steps holds because a published or
classical theorem does, cited with its hypotheses checked. A verdict is on the proof's own steps; a numbered result
it uses keeps its own verdict. Every other statement carries one of six labels, and the labels are never merged:
| label | meaning |
| --- | --- |
| `COMPUTED_HERE` | recomputed by the recomputation arm with independently written code — *exact* where the text says so (integer or rational arithmetic, or directed integer intervals), *numerical* where it says so (floating point, including high-precision floating point) |
| `DERIVED_FROM_VERIFIED_INPUTS` | follows from statements already verified here, with no step of its own beyond combining them |
| `CITED_THEOREM` | someone else's published theorem, stated here and not re-proved |
| `INHERITED` | taken from the research programme's records and not verified here; every use is marked |
| `UNMEASURED` | well posed, and not established here |
| `FAILED` | attempted and refused: false as stated, or true only in the corrected form given |
Where a run grades a statement of the programme `PARTIAL` — true of part of what it says — this paper says
`PARTIAL` too, and names the part that fails. A *search value* is the area at a configuration a search found: an
upper bound on a minimum, never the minimum. The *hull area* of a configuration is computed by the recomputation's
analytic hull — the convex hull of the disc's and the Reuleaux bodies' arcs and corners, located in closed form and
evaluated in floating point — and is numerical; only the certificates' areas are exact.
**Not claimed anywhere in this paper:** any value or bound for Lebesgue's universal covering constant — the
problem is open; that adding the Reuleaux heptagon raises the three-body value, which is the route's aim and is not
established; any lower bound above the published $0.8344$; and that the configuration of §6 is the least of its root,
or of its branch — its area is a floating-point value, not an enclosure, and the branch has searched configurations
lower still.
## 1. Introduction
### 1.1 Three bodies, and a fourth
A *universal cover* contains a congruent copy of every planar set of diameter one, and Lebesgue's problem asks for the
least area $a_{\mathrm{Leb}}$ of a convex one. Every lower bound so far fixes a finite family of test bodies and bounds
from below the least area $\Lambda(\mathcal F)$ of a convex set holding a congruent copy of each. The published lower
bound, $0.8344$ (Mishra [5]), is a certified computation on the disc $D$ of diameter one, the Reuleaux triangle $B_3$
and the Reuleaux pentagon $B_5$; the published upper bound is $0.8440935944$ (Gibbs [4]); both are cited, their
arXiv records checked. For the three-body family the companion paper [1] gives
$$0.8344 \le \Lambda(D, B_3, B_5) \le 0.83478095,$$
the lower end Mishra's, the upper end a placement found by search. Mishra locates the optimum at a configuration whose
hull $U_0$ has area $0.834780945912$. *Status:* `CITED_THEOREM` for the bounds; the rest `COMPUTED_HERE`, numerical, the
upper end a search value (RUN-002, RUN-009, RUN-044).
The natural next body is the Reuleaux heptagon $B_7$. Does it raise the value, $\Lambda(D, B_3, B_5, B_7) >
\Lambda(D, B_3, B_5)$? By the exchange theorem ([1], Theorem 7.3) it does if $B_7$ fails to fit every minimizing cover of
the three bodies — and only then, trivially. The research programme examined here, whose headline target is
$167/200 = 0.835$ (the line's first paper [3]), set out to prove this smaller fact first, by a route that works near the
located optimum and far from it separately, and to certify each step. This paper reports how far the certificates go.
### 1.2 The route
Write a three-body configuration as $v = (t_3, \rho_5, t_5)$ — the triangle's centre, the pentagon's turn and its
centre, with the disc fixed at the origin and the triangle's angle fixed by the rotation of the whole — and $A(v)$ for
the area of its hull $U(v)$; $R_n$ is the circumradius of $B_n$. For a body $K$ and a convex set $U$, $M_U(K)$ is the
signed margin of [1], Definition 3.1: positive when no congruent copy of $K$ fits in $U$, and then the least amount by
which the best placement sticks out. Measure the distance of $v$ from the orbit of the optimum's configuration $v_0$
under the problem's symmetries by the *component-motion metric*
$$q_{\mathcal O}(v) = \min_{w \in \operatorname{Orb}(v_0)} \max\Bigl\{\|t_3 - t_3^w\|,\ \|t_5 - t_5^w\| + 2R_5\sin\tfrac{d(\rho_5, \rho_5^w)}{2}\Bigr\},$$
where $d$ is the distance between turns on the circle; it bounds the Hausdorff distance of $U(v)$ from the orbit of
$U_0$ ([1], Lemma 8.4 and Corollary 9.2). Let $A_3^+ = 0.834781191$, an upper bound for $\Lambda(D, B_3, B_5)$ (§1.3).
The route has two gates, with a constant $s_A > 0$:
- **Gate A** (near): $M_{U_0}(B_7) > s_A$ — the heptagon misses the optimal hull by a margin. The margin is
1-Lipschitz in the cover in the Hausdorff metric ([1], Proposition 5.7), so $B_7$ then misses every hull $U(v)$ with
$q_{\mathcal O}(v) < s_A$.
- **Gate B** (far): every configuration with $q_{\mathcal O}(v) \ge s_A$ has $A(v) > A_3^+$. Equivalently, the
*far-set minimum* $A_{\mathrm{far}}(s_A) = \min\{A(v) : q_{\mathcal O}(v) \ge s_A\}$ exceeds $A_3^+$.
**Proposition 1.1 (the route).** *If both gates hold, $\Lambda(D, B_3, B_5, B_7) > \Lambda(D, B_3, B_5)$.* A minimizing
three-body cover is the hull of a configuration ([1], §7.1) and has area at most $A_3^+$; by Gate B that configuration
lies within $s_A$ of the orbit; by Gate A the heptagon misses its hull; so the heptagon misses every minimizing cover,
and by the exchange theorem the value rises. $\square$ *Status:* `PASS` (RUN-044, RUN-045).
The increase this would give is strict, not quantified: the route proves that the heptagon matters, not by how much.
It is not a route to $0.835$, and §6 shows why it cannot be made one without more.
### 1.3 The ceiling, and what its last digits measure
$A_3^+ = 0.834781191$ is the area of an outer polygon with $10^6$ uniform supporting lines around $U_0$, so it bounds
$\Lambda(D, B_3, B_5)$ from above. It exceeds $U_0$'s hull area by $2.45\times10^{-7}$ — far more than the $10^{-11}$ a
smooth body would lose at that density — and that hull is itself a cover, so the rounding of $A_3^+$'s last printed
digit cannot matter: $\Lambda \le A_3^+$, all that Proposition 1.1 needs, holds with room to spare. The excess is first order: it sits at the hull's straight bridging edges,
whose normals the uniform grid misses (the companion paper [2], Proposition 5.1). With the normals at the hull's 17
hand-overs — the directions where the supporting body changes — added to $10^4$ uniform ones, the excess falls from
$3.4\times10^{-6}$ to $1.2\times10^{-8}$. So the programme's statement that the ceiling and the optimum "differ by only
$2.45\times10^{-7}$", and that the sublevel $A \le A_3^+$ is therefore extremely thin, measures the ceiling's
construction, not the optimum (§3.3). *Status:* `COMPUTED_HERE`, numerical; the programme's statement `PARTIAL`
(RUN-044).
### 1.4 What this paper finds
- §2: Gate A holds, by a finite dual certificate re-enclosed in 400-bit integer intervals; its shipped verifier skips
two premises the bound rests on, which hold.
- §3: the far set is set up correctly — an exact dihedral quotient, a symmetric anchor, two far branches — and both
branches' searched minima lie above $A_3^+$.
- §4: in the branch the programme attacks, 644 of the 22,516 roots of its frontier are closed by erosion certificates
whose 56,149 area leaves all hold in exact arithmetic.
- §5: at the hardest root, six more certificates hold in exact arithmetic, 182,438 area leaves in all; but one gate is
not established — a symmetrization drops the branch's own constraint — and 14.6 % of the root's box, lying in the
branch, was closed only by a search.
- §6: the least configuration found in that root, located to 80 digits, has hull area $0.834986110559224$, above
$A_3^+$ by $2.05\times10^{-4}$. The far set holds configurations with hull area below $0.835$, numerically; so this route cannot be
turned into one for the programme's headline target without lifting a witness far from the optimum as well.
- §7: the local analysis of that configuration — what holds of its stationarity, and what does not.
Gate B is not certified. Neither, therefore, is the increase.
### 1.5 Where this comes from, and how it was checked
The route, its gates and its certificates are the programme's: seventeen cycles of its closure method, UESFCM
(unbounded-expansion self-referential finite closure, a methodology of Neo.K's), and the local-shape papers that
followed, LESR, all produced by Aletheia. The recomputation (懸衡) checked them in the runs RUN-043 to RUN-049 and RUN-056
to RUN-061 of the tree pinned in the front matter: every certificate decoded and replayed, every area leaf certified
again in exact arithmetic with the recomputation's own cores, the searched minima the cycles store searched again on
the recomputation's own analytic hull, and each check drilled with planted faults. Some searches the programme reports
store no configuration and could not be repeated (RUN-045, RUN-049). The seventeen cycles chain cleanly and never mark
evidence as proof; the target object they all name is not in the archive, and the method's own texts state its stop
rule in four different ways (RUN-043). The programme as a whole is reported in the line's first paper [3]. Each
result below names the run that checked it.
## 2. Gate A: the heptagon misses the optimum
### 2.1 How much it misses by
The placement certificate of [1] (§3) bounds $M_{U_0}(B_7)$ by a linear programme over finitely many support
directions and orientations. With 2,048 directions and 256 orientations over one period of $B_7$, the grid minimum is
$0.009382983648263432$, at orientation 193 — the programme's number to all seventeen digits — and less the orientation
loss $\pi/(7\cdot256) = 0.0017531209004407328$ it gives the structural bound $0.007629862747822699$: floating-point
linear programmes, not an enclosure. The loss uses $R_K \le 1$; the heptagon's own circumradius would nearly halve it,
to $0.0008991$. *Status:* `COMPUTED_HERE`, numerical (RUN-044).
The continuous margin, minimized over every basin of orientation with the inner problem solved until the linear
programme's value and the true maximum at its translation agree to $10^{-12}$, is $s_7 = 0.009384687909$, at
$\varphi = 0.676813$. The programme's value, $0.00938484$, lies $1.52\times10^{-7}$ above it and at neither basin's
minimum — a candidate for a lower bound should not sit above the minimum. It does no harm here, because Gate A is
certified by its own means. *Status:* `COMPUTED_HERE`, numerical; the programme's figure `PARTIAL` (RUN-044).
### 2.2 A finite dual certificate
The programme certifies Gate A by duality. It replaces $B_7$ by the heptagon of its corners, which lies inside it, and
bounds the support of each Reuleaux body of the cover from above by its defining unit discs, so that the target's
supports are smaller and the cover's no smaller; at each of 1,024 orientations it records three directions whose
weights, proportional to the sines of the gaps between them, put zero in their convex hull; and an
orientation-Lipschitz bridge carries the bound between grid orientations.
**Proposition 2.1 (the dual bound).** *If at an orientation three directions have all gaps below $\pi$, their sine-gap
weights are positive and form a convex combination with zero translation term; the weighted slack is then a lower
bound for the margin at that orientation. With all orientations of the grid present, the least such bound less the
Lipschitz bridge bounds $M_{U_0}(B_7)$ from below.* This is LP duality ([1], Theorem 3.2) with a feasible dual, and the
bridge of [1], Theorem 3.5. $\square$ *Status:* `PASS by cited theorem` (RUN-045).
Re-enclosed here in 400-bit integer intervals — from the placement's decimals, Machin's $\pi$ and enclosed Taylor sums,
every width about $7\times10^{-103}$ — every one of the 1,024 orientations is present, every triple's gaps are below
$\pi$, and the least lower bound is $0.00927495913424859$, at orientation 767. Less the bridge,
$\pi/(7\cdot1024) = 0.000438280225110183$, that gives $0.0088366789091384$ — the programme's recorded value, to its last
digit. The bound is conservative: at 33 sampled orientations the true margin of $B_7$ itself is above it by
$2.2\times10^{-7}$ to $1.8\times10^{-4}$, and at orientation 767 it is $0.009458708251$. The programme takes
$s_A = 0.0088366$. *Status:* `COMPUTED_HERE`, exact (RUN-045).
### 2.3 What the shipped verifier checks
The certificate's recorded intervals are points — lower and upper ends equal, 20-digit decimals — and on 76 of the
witnesses the recorded lower end lies above the true enclosure, by at most $3\times10^{-19}$. That is harmless, since
the verifier trusts none of them and recomputes every value. But it never checks the two premises of
Proposition 2.1: that each triple's gaps are below $\pi$ — past $\pi$ a weight turns negative and the dual bound fails
— and that all 1,024 orientations are present, which the bridge assumes. Both hold, as checked above; the verifier
would have passed a certificate in which they did not. *Status:* `COMPUTED_HERE`; that the verifier skips them is a
finding about the verifier, not about the bound (RUN-045).
## 3. Gate B, set up
### 3.1 The quotient and the domain
The problem's dihedral symmetry acts exactly: the six images of 40 random configurations have the same hull area to
$10^{-15}$, and the pentagon's turn, which moves by $2\pi/3 \equiv 4\pi/15$ modulo $2\pi/5$, reduces with the reflection
to the fundamental interval $[0, \pi/15]$. *Status:* `PASS`; the check `COMPUTED_HERE` (RUN-045).
The translations are bounded a priori by the farthest corner: a body placed beyond $T_n$ spans more than $A_3^+$ with
the disc. At $A_3^+$ this gives $d^\star = 0.694929333199893$, $T_3 = 0.193949748872303$ and $T_5 = 0.197117585445617$, to
the last unit. The programme presents this as a new, sharp root domain. It is Mishra's Remark 20 [5], to the digit at
his own threshold, and his Remark 34 reports that the smaller domain does not reduce the cost: at $0.833$, 27,350,260
boxes over the smaller domain against 25,425,568 over the larger. *Status:* the bound `PASS`; it is Mishra's, not new
(RUN-044).
### 3.2 The anchor and the two far branches
The located optimum is only nearly mirror-symmetric: its pentagon's residual turn is $2.4129\times10^{-5}$. The programme
replaces it by a symmetric *anchor* $U_{\mathrm{sym}}$, of area $0.834780945826$, whose triangle sits on the axis at
$x_3 = x_3^0$; its configuration is within $1.66\times10^{-5}$ of the optimum's in the metric $q$, a bound that holds
(their Hausdorff distance is $7.1\times10^{-6}$). So every configuration with $q_{\mathcal O} \ge s_A$ lies at least
$s = 0.0088366 - 0.0000166 = 0.00882$ from the anchor's orbit, and closing the set of such configurations about the
anchor closes Gate B. That set splits exactly into two *branches*: $F_3$, where the triangle lies at least $s$ from its
anchor position, $d_3 = \|(x_3 - x_3^0, y_3)\| \ge s$, and $F_5$, where the pentagon is at least $s$ from its own; the
disc of radius $s$ about $x_3^0$ is the *excluded ball* of $F_3$. The nearest other copy of the anchor in its orbit is
$2R_5\sin(\pi/30) = 0.109907730484$ away. *Status:* the construction `PASS`; the numbers `COMPUTED_HERE` (RUN-045).
Searched on their boundaries, $F_3$'s minimum is at most $0.834968955147$ and $F_5$'s at most $0.834804244389$ — each
$10^{-9}$ to $10^{-8}$ below the programme's values — so $F_5$'s margin over $A_3^+$ is at most $2.30534\times10^{-5}$, the
thinner of the two. On the programme's own far boundary — configurations exactly $s_A$ from the optimum's orbit — the
search reaches $0.83496965443$ in the triangle's branch. Every value stays above $A_3^+$. These are search values, so
upper bounds on the minima; no search can establish a minimum itself. The cycles attack $F_3$, whose frontier §4 takes
up; nothing in them addresses $F_5$ by certificate. *Status:* `COMPUTED_HERE`, numerical (RUN-045).
### 3.3 How sharp the optimum is
Every sampled direction out of the optimum's configuration — the coordinate directions and random ones — raises the
area. Minimized over all directions, though, the least one-sided slope is $1.12\times10^{-5}$, along a direction made
98.7 % of the pentagon's turn, and along it the sublevel $A \le A_3^+$ reaches $9.9\times10^{-4}$ and $7.8\times10^{-4}$ —
against at most $2.9\times10^{-5}$ along the axes. The sublevel is not extremely thin, then; but this does not threaten
Gate B: $10^{-3}$ of the pentagon's turn moves it by $5\times10^{-4}$, far inside $s_A$. *Status:* `COMPUTED_HERE`,
numerical (RUN-044).
The programme also considered replacing $B_5$ by $B_7$. The family $\{D, B_3, B_7\}$ has, by search, a hull of area at
most $0.8305410847$, so its value cannot pass $0.8344$, and the programme's rejection of it stands with more room than it
gave. *Status:* `COMPUTED_HERE`, numerical (RUN-044).
## 4. The branch $F_3$
### 4.1 A frontier of 22,516 roots
The programme ran an erosion branch-and-bound over $F_3$ — each box closed when an inner polygon of its bodies' common
cores ([2], Proposition 2.1) has area above $A_3^+$, or when it lies in the excluded ball — and saved its unresolved
frontier: 22,516 boxes, its *roots*. The prototype that produced it is not shipped, so what it closed is not checkable,
and which boxes are roots is taken from the file. On the file, most of the roots lie wholly in $F_3$, and the least area
at a root's centre is $0.835188375167486$, well above $A_3^+$. The programme infers that the roots persist because the
bound is loose, not because the area is low; centre areas cannot show that — the hardest root holds configurations
below its centre's area (§6). *Status:* `COMPUTED_HERE`, numerical; the inference not established (RUN-046).
A first-order bound $A(v) \ge A(c) - P(c)\,\tau(B)$ — the centre's area less its perimeter times the box's Hausdorff
radius — closes none of them: the perimeter is 3.33 to 3.40 and the radius up to 0.031, and the median penalty is 3.2
times the centre's slack over $A_3^+$. The hull's structure is simpler than its size suggests: walking the hull's
boundary at every centre gives 1,332 piece signatures but only 24 body skeletons — the cyclic order in which the bodies
appear on the boundary — which fall into 12 classes under reflection, one of them holding 15,210 roots. Among the roots
of that class, the 649 within $10^{-3}$ of $A_3^+$ have Taylor margins positive on 646 at first order, and the closest 27
all at second order — finite-difference diagnostics, as the programme says, not bounds. *Status:* `COMPUTED_HERE`,
numerical (RUN-046).
### 4.2 Erosion certificates
Two certificates close 644 of those roots: 27 roots by 27 trees with 2,699 nodes and 1,363 area leaves in all, and 617
roots by 617 trees with 109,037 nodes, 54,786 area leaves and 41 leaves in the excluded ball. Each *area leaf* carries a
lower bound from a finite set of witness points — the disc's inscribed 256-gon and, on each eroded core, its corners and
points along its arcs — and each excluded leaf is shown to lie in the ball. *Status:* the decoding and every stored
count `COMPUTED_HERE` (RUN-047).
**Every area leaf, again, in exact arithmetic.** Each of the 56,149 area leaves was certified here with the
recomputation's exact eroded cores: contact points at 1,024 directions, each proved inside its body in 400-bit integer
intervals, and the exact hull of those that pass. Every leaf certifies at that density, no candidate fails, and the
least margin over $A_3^+$ is $2.352\times10^{-5}$ for the first certificate and $2.277\times10^{-5}$ for the second. The
certificates' own least slacks are far thinner — $3.8\times10^{-8}$ and $2.5\times10^{-9}$ — because their witness sets
lose about $2.3\times10^{-5}$ against the exact cores: the trees are much deeper than an exact-core bound needs.
*Status:* `COMPUTED_HERE`, exact (RUN-047).
**Three things the documents do not say.**
- *The split rule.* The documents say only "deterministic split rule". Two natural guesses decode trees that parse but
leave boxes failing even the exact-core bound. The rule is in the verifier: split the widest coordinate by weights
that change with membership — $(1.5, 1.5, R_5, 1, 1)$ while the box may still meet the excluded ball,
$(0.7, 0.7, 1.5\,R_5, 1.5, 1.5)$ once it lies wholly outside. The node counts cannot tell rules apart; that every leaf
then passes, and that 617 per-tree minima agree to $7\times10^{-16}$, does.
- *The tiling.* A child's centre $c \pm h/2$ is rounded, so two children need not cover their parent exactly; the
widest gap is $4.7\times10^{-18}$. A configuration in a gap lies within that distance of a certified box, and moving
the bodies by $d$ changes the hull area by at most $Pd + \pi d^2$ with $P \le 8.026$ (Mishra's perimeter bound [5]),
about $3.7\times10^{-17}$ — far below every leaf's slack. So the gaps are covered, by an argument neither the documents
nor the verifiers state.
- *The package.* The second certificate's verifier loads the first's from an absolute path on the machine that wrote it,
and its own package does not ship that file.
*Status:* `COMPUTED_HERE`; the continuity step `PASS by cited theorem` (Steiner's formula and Mishra's bound; RUN-047).
### 4.3 What is left
Of the 649 near roots, five resist: 3766, 6217, 8001, 8015 and 8016. A targeted search splits them further and leaves 225
boxes — 200 under root 6217 and 25 under root 3766, the programme's *subroots* — whose depths and boxes reproduce here;
the parts of these roots outside the 225, and roots 8001, 8015 and 8016, are closed only in search logs whose trees are
not shipped. The frontier's other roots are not addressed by any shipped certificate. *Status:* `COMPUTED_HERE`
(RUN-046, RUN-047).
## 5. The hardest root
### 5.1 Six certificates
Root 6217 is a box of $F_3$ with the pentagon's turn $\rho_5 \in [0, \pi/120]$; its 200 subroots are those of §4.3, and the
programme's later cycles call the ones still open *cells*. It closes the root in pieces:
| certificate | trees | nodes | area leaves | excluded leaves | least margin, exact |
| --- | ---: | ---: | ---: | ---: | ---: |
| 124 subroots | 124 | 32,568 | 16,151 | 195 | $2.597\times10^{-5}$ |
| the slice $\rho_5 = 0$, as a rectangle | 1 | 299 | 150 | — | $3.456\times10^{-5}$ |
| eight subroots of the rotation tail | 8 | 102,062 | 50,626 | 409 | $2.610\times10^{-5}$ |
| five cells, against $0.8349865$ | 5 | 61,487 | 30,467 | 279 | $2.656\times10^{-5}$ |
| cell 131, a prefix tree | 1 | — | 38,893 | 1,966 | $3.022\times10^{-5}$ |
| cell 129, a prefix tree | 1 | — | 46,151 | 2,439 | $3.183\times10^{-5}$ |
Every tree decodes with its own split rule and uses exactly its bits; every stored count is the recomputation's; every
leaf's witness bound passes; and every area leaf — 66,927 in the first three, 115,511 in the last three — holds again in
exact arithmetic with the recomputation's exact cores, against $A_3^+$ or, for the five cells, against the tighter
reference $0.8349865$ of §6.2. The prefix trees are complete and prefix-free. The open cells of the root go from 76 to 68
to 61. *Status:* `COMPUTED_HERE`, exact (RUN-048, RUN-049, RUN-056).
The lemmas these certificates lean on hold. When several bodies move linearly with one parameter, the area of their hull
is convex in it (a linear parameter system: Fáry–Rédei [6], Rogers–Shephard [7]); the secant lemmas follow. The
*two-colour* criterion — a tree whose leaves are each either excluded or above the target closes its box — is right,
using one premise silently: that every configuration of the branch in the box has, along the ray from the anchor, its
point on the excluded ball's circle inside the box; that holds for this root. The prefix-tree criterion is right. Along
random lines of three kinds — vertical, horizontal and mixed — the second differences of the hull area are all positive,
the least $2.8$. *Status:* `PASS by cited theorem`; the checks along lines `COMPUTED_HERE`, numerical (RUN-048, RUN-049).
### 5.2 A gate that is not established
The slice $\rho_5 = 0$ is closed by a reduction: reflecting in the axis and moving the triangle and the pentagon
vertically together — a linear parameter system — the hull area is convex along the motion and even, so its least value
on the slice is at $y_3 = y_5 = 0$, a two-parameter rectangle, which a certificate closes. The programme records this as
"Gate 6217-A: closed".
But $F_3$ asks that $d_3 = \|(x_3 - x_3^0, y_3)\| \ge s$. The vertical motion ends at $y_3 = 0$, and where
$|x_3 - x_3^0| < s$ its end point is no longer in $F_3$: the reduction bounds a far configuration by a near one, and a
near one can lie below $A_3^+$ — the optimum does. The programme keeps only $x_3 \le x_3^0 - s$, saying the root does not
meet the other side; but the root's box runs to $x_3 = -0.012122$, $0.00886$ past $x_3^0 - s$. So the slice also holds
configurations of $F_3$ with $x_3^0 - s < x_3$ and $|y_3| \ge \sqrt{s^2 - (x_3 - x_3^0)^2}$ — the *arc side* — and no step of
the reduction, nor the rectangle's verifier, covers them. Of a random sample of the slice's configurations in $F_3$,
those on the arc side fall 145 in certified subroots, 6,812 in the 68 still open, and 3,899 in none of the 200 — closed
only in a search. *Status:* the claim that the gate is closed `FAILED` — the run's verdict is "not established"; the gate
itself holds numerically (below; RUN-048).
The reduction can be completed. For fixed $(x_3, x_5)$ on the arc side the area is even and jointly convex in
$(y_3, y_5)$, so on $|y_3| \ge r$ its least value lies on $|y_3| = r$, the arc $d_3 = s$; the moved point stays in the box,
which holds $y_3 = 0$ and $y_5 = 0$. That leaves three parameters, the angle $\alpha$ along the arc and the pentagon's
translation. Minimized over the translation at 25 angles, the area is least at $\alpha = \pi$, the contact configuration
of §6; elsewhere on the arc it lies above that, rising and then easing to $0.835483$ at the box's edge. So the gate's
statement holds numerically, with the margin of §6; what is missing is a certificate for the arc side. *Status:* the
completion `PASS by cited theorem` (Rogers–Shephard); the arc side `COMPUTED_HERE`, numerical (RUN-048).
### 5.3 "All other regions"
The programme's later text restricts what remains to the 61 open cells, "all other regions" having been "eliminated by
finite certificates". The 200 subroots fill 55.9 % of the root's box. Of the rest, 29.5 % of the box lies outside $F_3$
and needs no closure; but 14.6 % lies in $F_3$ and was closed only in the targeted search of §4.3, whose trees are not
shipped — and the later ledger that prunes the 200 subroots to 195 leaves it out too. Add the arc side of §5.2.
*Status:* the statement `FAILED` (RUN-049, RUN-056, RUN-058).
## 6. A configuration below 0.835
### 6.1 The triple contact
A multistart search over root 6217 ends at one symmetric configuration $v^\star$: $y_3 = \rho_5 = y_5 = 0$ and $d_3 = s$, the
triangle at $x_3^\star = x_3^0 - s$. There the disc, the triangle and the pentagon support the hull at exactly $\tfrac12$ in
four directions $\pm\theta^\star$, $\pi \pm \theta^\star$, with
$$\theta^\star = \arccos\frac{1}{2(R_3 + x_3^\star)} = 0.4540452162931833,$$
and the pentagon's position $x_5^\star$ solves two contact equations, located here to 80 digits. The recomputation's own
minimum over $x_5$ on the symmetric slice sits on $x_5^\star$ to $3\times10^{-14}$. The hull's area is
$$A^\star = 0.834986110559224,$$
$2.049196\times10^{-4}$ above $A_3^+$ — and $1.389\times10^{-5}$ *below* $0.835$. Its symmetry group is exactly a single
reflection. Every constant the programme gives for this configuration — $\theta^\star$, $x_5^\star$, a third contact angle
$\alpha^\star$, the three bridge lengths, the area — and the 13 intervals of its hull's signature reproduce from the
contact equations alone, to every digit the programme prints. *Status:* `COMPUTED_HERE`, numerical — high-precision
floating point, not an enclosure (RUN-048, RUN-049, RUN-056, RUN-057, RUN-060, RUN-061).
It is the least configuration found in root 6217, on every slice examined; it is not the least known of its branch,
whose searched minimum, $0.834968955147$, lies elsewhere (§3.2).
### 6.2 Two upper references
The programme bounds the configuration's area from above by outer polygons of support lines: 20,000 directions at 70
digits give an area below $0.835$, and a padded polygon of 500,000 directions gives $0.8349865$. Both reproduce. Their
excess over the hull area, $7.8\times10^{-6}$ and $2.7\times10^{-7}$, is again the first-order loss at the hull's straight
bridging edges: with the normals at its 17 hand-overs added, 20,000 directions come within $3.1\times10^{-9}$ and 500,000
within $4.9\times10^{-12}$. So the tight reference has $3.894\times10^{-7}$ of room, not the $6.5\times10^{-8}$ the programme
states. *Status:* `COMPUTED_HERE`, numerical (RUN-049).
### 6.3 What it means
**For the route's own target nothing breaks.** $v^\star$ lies $2.05\times10^{-4}$ above $A_3^+$, so Gate B holds there
numerically, with that margin.
**$v^\star$ itself does not defeat the headline target.** $F_3$ is drawn about the anchor with the smaller radius $s$, and
$v^\star$ lies on its inner circle: its triangle exactly $s$ from the anchor's, whose triangle is the optimum's to within
$10^{-7}$, and its pentagon nearer than that to the optimum's. So its distance from the optimum's configuration in the
metric $q$ is below $s_A$: it lies inside Gate A's near zone, and the heptagon misses its hull. Whether it misses by
enough to raise the area to $0.835$ — by at least $1.389\times10^{-5}$ — is a quantitative question the route does not ask,
and nothing here measures it. *Status:* `DERIVED_FROM_VERIFIED_INPUTS` from the configurations' coordinates and Gate A;
the size of the lift `UNMEASURED`.
**But the route cannot reach $0.835$.** On the far gate's own boundary — configurations exactly $s_A$ from the optimum's
orbit, where Gate A's margin is used up — the search finds hull area $0.83496965443$, and $F_3$'s boundary reaches
$0.834968955147$; both lie below $0.835$ (§3.2). With $0.835$ in place of $A_3^+$, Gate B fails at these configurations. So
the route as built — the heptagon used only near the optimum, the three bodies' own area everywhere else — cannot certify
$\Lambda(D, B_3, B_5, B_7) \ge 0.835$; that would need a witness lifted in the far set as well, and a quantified lift near
the optimum. *Status:* `DERIVED_FROM_VERIFIED_INPUTS`, numerical: a search value below $0.835$ is a configuration, so the
failure is a floating-point fact; an enclosure of its area would make it exact (RUN-045).
## 7. Is it the least of its root? The local analysis
The programme's later papers try to show that $v^\star$ is the least configuration of root 6217 — which would close the
root against $A_3^+$ with the margin of §6. What holds of their arguments:
**On the symmetric slice.** In the plane of $(x_3, x_5)$ at $y_3 = \rho_5 = y_5 = 0$ the area is convex (Fáry–Rédei), and
the contact's optimality condition there is sound with the mix of one-sided gradients the programme's Cycle 12 records,
$(-0.04756, 0)$: the constraint $d_3 \ge s$ is active with a multiplier of about $0.047$. A later paper argues the same
stationarity from a split of the contact "pressures" into a subgradient $(g_3, 0)$ with $-g_3 = 0.1228$; that split is not a
subgradient, in that same plane. Over 72 directions it misses the subgradient inequality by up to $0.0663$ per unit, and
at finite steps it fails outright, by $2.5\times10^{-4}$ at step $10^{-2}$. The cause is the first-order model the split
rests on, which treats the hull as if each normal's support moved independently and overstates the rate in every one of
the 72 directions. The conclusion survives: along every feasible direction the area rises, at least at $0.0354$ per unit,
and the area is convex, so $v^\star$ minimizes on $x_3 \le x_3^\star$; across the constraint, toward the anchor, the area
falls at $0.0331$ per unit. *Status:* the split `FAILED` as a subgradient; the conclusion `COMPUTED_HERE`, numerical
(RUN-048, RUN-057, RUN-061).
**Four contacts cannot certify the shape.** The programme leaves open whether a measure on the four contact directions
can match the configuration's curvature, for a library of test functions containing $1$ and $\cos 2\theta$. It cannot.
The constant mode fixes the measure's mass to the hull's perimeter $P$, and the four directions share one value of
$\cos 2\theta$, so any measure on them has $\cos 2\theta$-moment $P\cos 2\theta^\star = 2.05$, where the configuration's curvature
measure has $0.124$. A certificate needs contacts on the arcs. *Status:* `PASS` (RUN-056).
**The pentagon's turn.** Turning the pentagon off zero, the least area rises: re-minimized at 27 turns up to $\pi/120$,
the profile $m(\rho)$ is non-decreasing, with ratios $(m(\rho) - m(0))/\rho^2$ between $0.1738$ and $0.2254$ — the
programme's stored samples are search values up to $8.3\times10^{-8}$ high. The turn is first-order critical numerically:
the one-sided rate along the re-minimized profile is proportional to the turn. The paper that first derives this does so
from a finite contact model in which turning the pentagon costs $+0.0293$ at first order, and a later paper withdraws
that derivation itself. The programme's handoff document then infers $m'(0) = 0$ from the area being even in the turn;
evenness gives only $m'(0^+) = -m'(0^-)$, as the later papers also say. *Status:* the profile and the criticality
`COMPUTED_HERE`, numerical; the derivation and the inference `FAILED` as given (RUN-058, RUN-059, RUN-061).
**The path out of zero turn.** As the pentagon turns, the triangle slides along the circle $d_3 = s$ at a rate $u$ and the
pentagon translates at $(w, v)$, all per unit of turn; along the minimizing path these rates tend to
$(u, v, w) = (5.157, -0.1892, 0)$. The programme's closed forms for them — the critical rates
$u^\star = 5.15712624526841370759\ldots$ and $v^\star = -0.1892281899066409745\ldots$, with $w^\star = 0$ — reproduce to 70
digits, and the six constants they are built from to binary64; $w^\star = 0$ is exact algebra, on the assumption, still
open, that the minimizing path keeps all three of its contact structures at first order. To first order the area along
the path changes by a multiple $\gamma_w w$ of the pentagon's sideways rate alone — the $u$ and $v$ terms cancel
identically — so the path is level to first order. At the four turns examined, small pieces of the hull the programme
predicted, its "secondary slivers", have width below $10^{-11}$: they are ties, not pieces; and the second-order slivers
along the critical rates appear at the antipodal directions, not where the programme looks for them. *Status:* the
algebra `PASS`; the rest `COMPUTED_HERE`, numerical; the slivers `PARTIAL` (RUN-059, RUN-060).
None of this is a certificate. $v^\star$ is, numerically, the least configuration of root 6217 on every slice examined;
nothing here proves it.
## 8. Every result, and the strength at which it holds
| result | holds as | checked in |
| -------------------------------------- | ------------------------------------------ | ---------------- |
| §1.1 — the three-body bracket; the optimum's hull area | the bounds `CITED_THEOREM`; the rest `COMPUTED_HERE`, numerical | RUN-002, RUN-009, RUN-044 |
| Proposition 1.1 — the route | `PASS` | RUN-044, RUN-045 |
| §1.3 — the ceiling's excess is first-order loss | `COMPUTED_HERE`, numerical; the thin-sublevel statement `PARTIAL` | RUN-044 |
| §2.1 — the grid bound; the continuous margin | `COMPUTED_HERE`, numerical; the programme's $s_7$ `PARTIAL` | RUN-044 |
| Proposition 2.1, §2.2 — Gate A's dual certificate | `PASS by cited theorem`; the replay `COMPUTED_HERE`, exact | RUN-045 |
| §2.3 — two premises the verifier skips | `COMPUTED_HERE` | RUN-045 |
| §3.1 — the quotient; the root domain | `PASS`; the domain is Mishra's | RUN-044, RUN-045 |
| §3.2 — the anchor and the branches; their searched minima | the construction `PASS`; the minima `COMPUTED_HERE`, numerical, search values | RUN-045 |
| §3.3 — sharpness; the replacement family | `COMPUTED_HERE`, numerical | RUN-044 |
| §4.1 — the frontier; its structure; Taylor diagnostics | `COMPUTED_HERE`, numerical | RUN-046 |
| §4.2 — two erosion certificates, 56,149 area leaves | `COMPUTED_HERE`, exact; the continuity step `PASS by cited theorem` | RUN-047 |
| §4.3 — what is left of the frontier | `COMPUTED_HERE` | RUN-046, RUN-047 |
| §5.1 — six certificates at root 6217, 182,438 area leaves | `COMPUTED_HERE`, exact | RUN-048, RUN-049, RUN-056 |
| §5.1 — convexity of linear parameter systems; secant and closure lemmas | `PASS by cited theorem` | RUN-048, RUN-049 |
| §5.2 — "Gate 6217-A: closed" | `FAILED` (not established); the gate holds numerically | RUN-048 |
| §5.2 — the reduction completed; the arc side searched | `PASS by cited theorem`; the search `COMPUTED_HERE`, numerical | RUN-048 |
| §5.3 — "all other regions eliminated by certificates" | `FAILED` | RUN-049, RUN-056, RUN-058 |
| §6.1 — the triple contact; its area $0.834986110559224$ | `COMPUTED_HERE`, numerical | RUN-048, RUN-049, RUN-056, RUN-057, RUN-060, RUN-061 |
| §6.2 — the upper references | `COMPUTED_HERE`, numerical | RUN-049 |
| §6.3 — $v^\star$ inside Gate A's near zone | `DERIVED_FROM_VERIFIED_INPUTS`; the size of the lift `UNMEASURED` | RUN-044, RUN-045, RUN-048 |
| §6.3 — the route cannot reach $0.835$ | `DERIVED_FROM_VERIFIED_INPUTS`, numerical | RUN-045 |
| §7 — the symmetric slice: the split as a subgradient | `FAILED`; the conclusion `COMPUTED_HERE`, numerical | RUN-048, RUN-057, RUN-061 |
| §7 — four contacts cannot certify the shape | `PASS` | RUN-056 |
| §7 — the turn: profile, criticality; its derivation | `COMPUTED_HERE`, numerical; the derivation `FAILED` as given | RUN-058, RUN-059, RUN-061 |
| §7 — the path out of zero turn | the algebra `PASS`; the rest numerical; the slivers `PARTIAL` | RUN-059, RUN-060 |
No result is `INHERITED`. No area in §6 and §7 is an enclosure.
## 9. Corrections found on the way
### 9.1 Statements that do not hold as written
- **"Gate 6217-A: closed."** The symmetrization behind it drops the branch's constraint, and the arc side of the slice
is covered by no certificate as a whole — a little of it falls in certified subroots (§5.2). (RUN-048, RUN-049,
RUN-056)
- **"All other regions have already been eliminated by finite certificates."** 14.6 % of root 6217's box lies in the
branch and was closed only by a search, whose trees are not shipped; the ledger that prunes the root's 200 subroots to
195 leaves it out too (§5.3). (RUN-049, RUN-058, RUN-059)
- **The translation subgradient.** The pressure split $(g_3, 0)$ is not a subgradient; the constraint's multiplier is
about $0.047$, as the programme's own earlier cycle records, not $0.1228$ (§7). (RUN-057, RUN-061)
- **"Evenness gives $m'(0) = 0$"**, in the handoff document, does not follow; criticality of the turn holds numerically.
The derivation from the finite contact model, in which turning costs $+0.0293$, is withdrawn by the programme's own
later paper (§7). (RUN-058, RUN-059, RUN-061)
- **Gate A's verifier** does not check two premises its bound rests on; both hold (§2.3). (RUN-045)
### 9.2 Figures that are search values, or other quantities
- The continuous margin $s_7$ is $0.009384687909$; the programme's figure lies $1.52\times10^{-7}$ above it (§2.1).
(RUN-044)
- The far branches' minima are search values; both lie lower than the programme's (§3.2). (RUN-045)
- The 27 samples of the rotation profile are search values, up to $8.3\times10^{-8}$ high; their ratios are $0.1738$ to
$0.2254$ (§7). (RUN-048, RUN-058)
- The "secondary slivers" are ties at the minimum; those reported come from a sample $1.5\times10^{-9}$ above it. The
second-order slivers along the critical rates open at the antipodal directions (§7). (RUN-059, RUN-060)
- The ceiling's $2.45\times10^{-7}$ over the optimum, and the tight reference's $6.5\times10^{-8}$ of room, are outer
polygons' first-order losses at bridging edges; the room is $3.894\times10^{-7}$, and the sublevel is about $10^{-3}$
long along the pentagon's turn, not extremely thin (§1.3, §3.3, §6.2). (RUN-044, RUN-049)
- The printed $u^\star$ is $5\times10^{-14}$ off, binary64 through a system whose determinant is about $10^{-4}$.
(RUN-060)
### 9.3 Credit and form
- The "sharp root domain" is Mishra's Remark 20, and his Remark 34 reports that it saves no boxes (§3.1). (RUN-044)
- The erosion certificates' split rule is stated in neither document and is recoverable only from the verifier; their
rounded splits leave gaps of up to $4.7\times10^{-18}$, closed by a continuity argument neither states; and the second
certificate's verifier cannot run from its own package (§4.2). (RUN-047)
- The recorded witness intervals of Gate A's certificate are points, 76 of them a few $10^{-19}$ above the true
enclosure; the verifier recomputes them, so nothing rests on them (§2.3). (RUN-045)
## 10. Reproduction and attachments
**What a reader can check without the archive.** The recomputation tree is private; its public projection is not.
Every report, every script and every gate log of its 68 runs, as they stood at the pinned commit, is published with
SHA-256 sums at (English:
), one page per document of the programme. The thirteen runs this
paper reports are RUN-043 to RUN-049 and RUN-056 to RUN-061; it also cites RUN-002 for the arXiv records and RUN-009 for
the three-body bracket. Every load-bearing number in this paper occurs in their gate logs or in
`data/paper-figures.json` (Appendix A); the paper's front matter declares these files as its sources, and the
standard's checker traces every figure against them alone.
**The instrument can fail, and was made to.** Every check of every run was drilled: faults were planted in its
inputs, and each had to be caught by exactly the check named for it, while controls — the unmodified inputs and
harmless rewrites — had to stay green. Over the thirteen runs of this paper: 209 planted faults, all 209 caught by the named
check, 39 controls undisturbed, 118 checks, 2,046 must-stay-green assertions held. Over the whole recomputation tree, of which these runs are
part: 1,290 planted faults, 1,290 caught by the named check, 262 controls undisturbed, 665 checks.
**What re-running needs.** The programme's documents and packages are two archives, kept byte for byte; the input
manifest `data/SOURCE_MANIFEST.v1.json` gives the size, SHA-256 and git blob id of each and the SHA-256 of every
leaf. The archives are not public; the scripts read them in memory and never extract them.
**Commands.** Python 3.14 [8] with mpmath 1.3 [9], numpy 2.4 [10], scipy 1.17 [11] (its HiGHS solver [13] and its Qhull interface [14]) and sympy 1.14 [12]; no network. From the line's
directory (`lebesgue-verification-xuanheng/` at the pinned commit), each run is re-run, and its drill, by
```bash
python code/run048_uesfcm_cycles_12_14.py
python code/run048_uesfcm_cycles_12_14.py --drill
```
and likewise for every `code/runNNN_*.py` named above. A run rewrites its gate log under `data/gate-logs/`; a re-run is
correct when that log is byte-identical to the published one. `python code/paper_figures.py` rewrites
`data/paper-figures.json` and is correct on the same terms. The paper is typeset by the shared build tool of the
crystallization repository, which refuses to write a PDF from which a character would be dropped.
## 11. Contributions
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 seventeen closure cycles and the
local-shape papers this paper reports, with their gates, certificates, searches and analyses, on the programme Neo.K
set out. Every statement attributed here to "the programme" is from those documents.
**Neo.K** set out the research programme: the finite-closure strategy and its targets, and the methodologies it runs
on, among them the closure method of these cycles.
**懸衡 (Xuán Héng)** — the independent recomputation; model: Claude, Opus series — did the runs this paper names and
wrote this paper: every certificate decoded and replayed, every area leaf certified again in exact arithmetic with
exact cores, Gate A's certificate re-enclosed in integer intervals, every searched minimum searched again, the
contact located to 80 digits; the completion of the reduction in §5.2 and the arc-side search; the impossibility in
§7; the drills of §10; and the corrections of §9.
**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; among its findings was a logic error in the paper's central consequence — the configuration below
0.835 first offered lay inside Gate A's near zone, so it did not show what the paper said — and its findings 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 suggestions — that the abstract and §1 say the configuration
below 0.835 is numerical, and that §1.3 say why the rounding of $A_3^+$'s last digit does not matter — were applied,
and so was the note he added on checking them, that §1.3 then gave $2.45\times10^{-7}$ twice.
**Priority, stated plainly.** The route, its gates and its certificates are the programme's. What is offered as this
line's own is the check of them, the gaps it found, the completion and the impossibility named above, and the
corrections. No bound on Lebesgue's constant is claimed.
## Acknowledgements
We thank Anthropic, whose Claude models the lab's verification and recomputation lines run on, and OpenAI, whose
ChatGPT models the programme's documents were written with. Not every AI model or instance that took part in this
work is named in it — among them instances that the named authors ran as helpers; that an AI is not listed here
does not mean that none took part.
## References
1. Aletheia, Neo.K and 懸衡, *A certified finite reduction for Lebesgue's universal covering problem*, preprint,
AMRAL Research Lab (2026), the second paper of this line.
2. Aletheia, Neo.K and 懸衡, *Replaying large geometric certificates without trusting their producer*, preprint,
AMRAL Research Lab (2026), the third paper of this line.
3. Aletheia, Neo.K and 懸衡, *A finite-closure programme for Lebesgue's universal covering problem: certified
progress, target ledgers, and an independent recomputation*, preprint, AMRAL Research Lab, the first paper of this
line, (2026).
4. P. Gibbs, *An upper bound for Lebesgue's covering problem*, (2018).
5. U. Mishra, *Curves of constant width and Lebesgue's covering problem*, (v2, 2026).
6. I. Fáry and L. Rédei, *Der zentralsymmetrische Kern und die zentralsymmetrische Hülle von konvexen Körpern*, Math.
Ann. 122 (1950), 205–220.
7. C. A. Rogers and G. C. Shephard, *Some extremal problems for convex bodies*, Mathematika 5 (1958), 93–102.
8. The Python Software Foundation, *Python* (version 3.14), .
9. The mpmath development team, *mpmath: a Python library for arbitrary-precision floating-point arithmetic* (version 1.3.0), (2023).
10. C. R. Harris, K. J. Millman, S. J. van der Walt, R. Gommers et al., *Array programming with NumPy*, Nature 585 (2020) 357–362, doi:10.1038/s41586-020-2649-2; used here at version 2.4.
11. P. Virtanen, R. Gommers, T. E. Oliphant, M. Haberland et al., *SciPy 1.0: fundamental algorithms for scientific computing in Python*, Nature Methods 17 (2020) 261–272, doi:10.1038/s41592-019-0686-2; used here at version 1.17.
12. A. Meurer, C. P. Smith, M. Paprocki, O. Čertík et al., *SymPy: symbolic computing in Python*, PeerJ Comput. Sci. 3 (2017) e103, doi:10.7717/peerj-cs.103; used here at version 1.14.
13. Q. Huangfu and J. A. J. Hall, *Parallelizing the dual revised simplex method*, Math. Program. Comput. 10 (2018) 119–142, doi:10.1007/s12532-017-0130-5, the article the HiGHS project asks its users to cite; HiGHS () is the solver behind SciPy's linear programming.
14. C. B. Barber, D. P. Dobkin and H. Huhdanpaa, *The quickhull algorithm for convex hulls*, ACM Trans. Math. Software 22(4) (1996) 469–483, doi:10.1145/235815.235821; Qhull, behind SciPy's convex hulls.
## Appendix A. The figures file
`data/paper-figures.json`, and the script that writes it, `code/paper_figures.py`, are published beside this paper as
they stood at the pinned commit. The script runs nothing of the programme and computes no mathematics of its own.
Its entries are of five kinds, never mixed: sums, differences and ratios of gate-log fields, each naming the fields it
reads; counts over the recomputation's inventory and drill records, for the whole tree and for the runs of each paper;
grid sizes and sample counts read from the run scripts as written; values that a run's own function computes and
checks but its gate log does not record, evaluated at the run's own inputs; and figures quoted from the programme's
records, each with its document, the document's SHA-256 and the line. Re-run in the recorded environment, the file is
byte-identical.