# RUN-009 — Round 06: the exchange compiler holds; its seed ladder is exact at the second rung and strict at the third

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-24
**Subject:** `AMRAL_Lebesgue_Finite_Closure_Round_06_Witness_Exchange_v0.1.md` (AMRAL-LUC-FC-R06, dated 2026-09-18) and its package (`VALIDATION.json`, `State_Crystal`), read from the archive; the package's `sanity.py` was not opened
**Tools:** [`run009_round06_witness_exchange.py`](../code/run009_round06_witness_exchange.py) — an exact hull-area integrator for the disc with placed polygons and Reuleaux polygons; Round 03's certificate LP (RUN-006); differential evolution for the level-three search; Mishra's abstract and full text; Xie's version history
**Logs:** [`run009-round06-witness-exchange.json`](../data/gate-logs/run009-round06-witness-exchange.json); citation snapshot [`round06-citations.json`](../data/external/round06-citations.json)

**Verdict: PASS**, with one bibliographic finding pinned.

- Round 06 compiles Round 05's existence statement into a finite exchange procedure.
  The configuration space of a finite family is compact, with `d_m = 3m − 4` continuous
  parameters. A non-saturated family has one violation margin `δ_F > 0` over its whole
  minimizer set. A finite dictionary batch then separates that set, and a batch with
  separation margin `S_F(B) > 0` strictly raises `Λ`. Certified search must eventually
  find such a batch, and a witness that contains another dominates it. All eight
  `PROVED` hold, each self-contained given Rounds 02–04. Theorem 24.1 assumes certified
  covers of the minimizer set with radii tending to zero; it does not construct them,
  and says so by deferring that to C06-2.
- **The seed ladder, rebuilt exactly.** `λ_1 = π/4`. Pál's value
  `Λ(D, P_3) = π/8 + √3/4` — which Round 06 names but does not cite; Mishra's full text
  traces it to Pál 1920 — is proved again here. For the Reuleaux triangle Round 06
  writes `Λ(D, B_3) ≥ π/8 + √3/4`; it is **equal**, because the triangle's arcs never
  leave the tangent cone of the disc. So the Reuleaux upgrade gains nothing at the
  second rung. At the third it does: this tree places the disc, triangle and pentagon
  with hull area 0.8335974, while Mishra certifies at least 0.8344 for the Reuleaux
  family — a strict gap of at least 0.000803.
- **Mishra's seed, attacked by search.** Differential evolution over the five
  parameters finds 0.83478094595 — Mishra's own located optimum — and nothing below
  0.8344. Mishra's two published placements rebuild exactly under the bounds he states
  for them. So `Λ(D, B_3, B_5) ∈ [0.8344, 0.83478095]`. Round 06 is right that 0.8344
  is a lower bound and not the value; the value lies within `3.8×10⁻⁴` above it.
- **The seed's exchange quantities, exact.** Round 03's certificate LP gives
  `δ_{D,B_3} = 1/√3 − 1/2` to `10⁻¹⁶`. By Jung's theorem the Reuleaux triangle is the
  disc's worst target, so `δ_F` for `F = {D}` is that same number. §19's distance bound
  is attained by the seed hull. §20's modulus, which Round 06 leaves abstract, is exact
  on this family: `γ(s) = Φ(½ + s) − π/4`. The seed exchange gains exactly three times
  it — one tip per vertex.
- **Bibliography.** Round 06 cites Xie by the title of the preprint's first two
  versions. v3 (13 June 2026) retitled it and v4 (8 July) raised its bound to 0.833, both
  before Round 06's date; pinned. Pál 1920 and Gibbs 2014 are named in the text but
  missing from the reference list.
- **The package** is rebuilt value for value. Every value in it is an arithmetic
  restatement — the "toy budget" sets each error to `δ/8` — so it could fail only by an
  arithmetic slip.
- **A tool correction.** The exact envelope routine this tree wrote for RUN-008 had a
  tie bug, found here when the optimizer settled on the tie. It is corrected, and
  RUN-008 re-run with its results unchanged (commit `be12d08`).

Drill: 17 / 17 plants caught by exactly the named checks, 4 / 4 controls undisturbed,
255 / 255 must-stay-green assertions held; each of the thirteen checks, blinded in
turn, is reported blind in exactly as many cases as plants name it.

---

## What Round 06 claims

1. **The seed** (§1–2): Mishra's certificate `Λ(D, B_3, B_5) ≥ 0.8344` over a
   five-dimensional placement space (486,799,600 nodes; floating-point error bound
   `1.72×10⁻⁹`), under `λ_1 = π/4` and Pál's `Λ(D, P_3) = π/8 + √3/4 ≤ Λ(D, B_3)`. §3
   warns that a search gives upper bounds on `Λ(F)`, never lower bounds.
2. **Compactness** (§4–8): with the disc fixed, `‖t_i‖ ≤ R = 2Ā`; a common rotation is a
   gauge, leaving `d_m = 3m − 4` continuous parameters (5 for Mishra's family, matching
   his setup); the hull area is continuous, the minimizer set `𝔐(F)` compact.
3. **Uniform violation** (§9–12): `W` is 1-Lipschitz in the cover and positive off
   universality, so a non-saturated family has `δ_F = min_{𝔐(F)} W > 0` (Thm 11.1).
4. **Separation and exchange** (§13–20): a Round 02 dictionary finer than `δ_F`
   separates all minimizers (Thm 14.1); a batch with `S_F(B) > 0` strictly raises `Λ`
   (Thm 18.1), forces any new cover to lie at least `s` from the old minimizer set (§19),
   and raises `Λ` by at least an abstract modulus `γ_F(s) > 0` (§20).
5. **The compiler** (§21–25, §31–33): minimizer cells with radii `τ_j`, robust
   cell-witness rule `μ − τ > 0`, finite set cover; if `τ_n + ε_n + ζ_n < δ_F/2` the
   search must succeed (Thm 24.1) — a semi-decision, not a saturation test.
6. **Dominance** (§26–27): `gK ⊆ L` implies `Λ(G ∪ {L}) ≥ Λ(G ∪ {K})`; `P_n ⊆ B_n`, so
   Mishra's step from polygons to Reuleaux polygons is a dominance upgrade.
7. **Seed sanity** (§29, §37): `δ_{D,B_3} = 1/√3 − 1/2 ≈ 0.0773502692`, and the strict
   ladder `0.785398… < 0.825711… < 0.8344`.

§42 claims no new bound and no identification of the next witness.

## A, X — sources

**A0.** 17 anchors pin the formulas below as written.

**A1.** Six external references, re-fetched. Five match. The sixth is the finding:

| | title | versions |
| --- | --- | --- |
| cited by Round 06 (ref. 5) | *A Reproducible Certificate for the Brass–Sharifi Lower Bound in Lebesgue's Universal Cover Problem* | v1 (3 Jun 2026), v2 (4 Jun) |
| on arXiv since | *A Certified Lower Bound for Lebesgue's Universal Cover Problem* | v3 (13 Jun, bound 0.83201), v4 (8 Jul, bound 0.833) |

Round 06, dated 18 September, cites a title that had been replaced three months
earlier, and whose paper had since changed from reproducing Brass–Sharifi's 0.832 to
certifying 0.833 for the same three sets. Round 06 uses no number from it, so nothing
downstream moves; the check pins the stale title and requires it to be exactly v1's or
v2's.

Two sources the text relies on are missing from its reference list. One is Pál 1920,
for `π/8 + √3/4` (§2). The other is Gibbs 2014 (arXiv:1401.8217), for the numerical
Reuleaux search (§3, §35).

**X1.** What §1–3 and §35 say about Mishra's paper, checked against its abstract and
full text (v2):

| Round 06 | Mishra | |
| --- | --- | --- |
| test sets: disc, Reuleaux triangle, Reuleaux pentagon; `a_Leb ≥ 0.8344` | the same sets; "area at least 0.8344" | ✓ |
| five-dimensional placement space; 486,799,600 nodes | the same | ✓ |
| floating-point error bound `1.72×10⁻⁹` | `η = 1.72×10⁻⁹`, the sum of two bounds (§5.4) | ✓ |
| Pál's classical value `π/8 + √3/4` for disc and triangle | Pál (1920), disc and equilateral triangle, "evaluates the minimum by hand" | ✓ |
| Gibbs 2014's numerical values are upper bounds for the family, not lower bounds | Gibbs' 0.83699098 is an upper bound, and "a better optimiser does not repair it" | ✓ |
| — | reflections allowed ("a reflection where a reflection helps") | matches `E(2)` |

## W — the seed, rebuilt

| check | Round 06 | recomputed | result |
| --- | --- | --- | --- |
| W1 | §2: `λ_1 = π/4`; `Λ(D, P_3) = π/8 + √3/4`; `Λ(D, B_3) ≥` it | exact hull areas; the lower side proved (RUN-008 W2); 96 displaced placements | PASS — equality for `B_3` |
| W2 | §29: `δ_{D,B_3} = 1/√3 − 1/2` | Round 03's certificate LP over both reflection branches, `M = 3072`, with Theorem 17.1's bracket; 40 random targets against the disc | PASS — to `10⁻¹⁶` |
| W3 | §19–20 on the seed | the distance bound, attained and never undercut (300 placements); `γ` exact, never undercut (300 covers) | PASS |
| W4 | §6: common rotation gauge; `d_m = 3m − 4` | area invariant under 20 random common rotations (`10⁻¹²`), changed by turning one body alone; `m = 2 … 7`; `d_3 = 5` against Mishra | PASS |
| W5 | §1, §27: the seed; dominance | Mishra's placements rebuilt; differential evolution over both families | PASS — table below |
| W6 | §26–27: `P_n ⊆ B_n` | support functions, `n = 3, 5, 7, 9` | PASS |

**W1 — the second rung is not a step.** The hull of the disc and the equilateral
triangle of side 1, placed concentrically, is the disc plus three tips; its area is
`π/8 + √3/4 = 0.8257117836`. The lower bound — no placement does better — is RUN-008's
W2 argument, which uses only the three vertices and so covers the triangle and the
Reuleaux triangle alike. For the Reuleaux triangle the hull is *the same set*. Each arc
leaves its vertex along a line tangent to the disc (the tangent sits at distance
`A·(A − B) = ½`) and bends inward, never leaving the tangent cone. So
`Λ(D, B_3) = Λ(D, P_3)` exactly, and Round 06's `≥` is an equality. The dominance upgrade
`P_3 → B_3` costs nothing and gains nothing here.

**W2 — the margin, by the certificate machinery.** With the vertex directions on the
grid (`M = 3072` is divisible by 3), the grid LP is exact: `M_D(B_3) = 0.0773502691896258`,
equal to `1/√3 − 1/2` to `10⁻¹⁶`, and Theorem 17.1's bracket contains it. The disc's
worst target: a body of diameter 1 has circumradius at most `1/√3` (Jung's theorem), with
equality for the Reuleaux triangle. So `W(D) = δ_{D,B_3}`, and for `F = {D}` Round 06's
`δ_F` is exactly this number. 40 random constant-width targets reach at most `0.0264`
against the disc.

**W3 — §19 and §20 made concrete.** For `F = {D}` the minimizer set is `{D}` and
`B = {B_3}` separates it with `s = δ`. Every cover of `B_3` that holds `D` lies at least
`s` from `D` — attained exactly by the seed hull (`d_H = 0.0773502692`); 300 random
placements come no closer than `0.0832`. §20's `γ_F(s)` is abstract in Round 06; here it
is exact. `d_H(V, D) ≥ s` means `V` has a point at distance `½ + s`, so by Round 05's
§22, `γ(s) = Φ_{1/2}(½ + s) − π/4`, attained by a single tip. At `s = δ` that is
`0.0134379`. The seed exchange actually gains `√3/4 − π/8 = 0.0403136` — exactly three
tips, one per vertex. The bound holds and is loose by the number of vertices.

**W5 — the third rung.**

| | Mishra's placement, rebuilt | his stated bound | this tree's search | |
| --- | ---: | ---: | ---: | --- |
| disc, `B_3`, `B_5` | 0.8347809459 | ≤ 0.834781191 | 0.8347809460 | no placement below 0.8344 |
| disc, `P_3`, `P_5` | 0.8335975366 | ≤ 0.833597897 | **0.8335973878** | none below 0.833 (Xie) |

Mishra's two placements, read from his text and rebuilt with this tree's exact hull,
fall under his stated bounds. Those bounds are outer-polygon values rounded up; the
exact hulls lie `2.5×10⁻⁷` and `3.6×10⁻⁷` below them. The search is differential
evolution over the gauge-fixed box, then Nelder–Mead, each value confirmed against a
sampled hull to `10⁻¹⁰`. For the Reuleaux family it finds Mishra's optimum again, to
`1.2×10⁻¹¹`: his placement turned by 120°, which maps the triangle to itself. For the
classical family it finds a
placement `1.5×10⁻⁷` below Mishra's published one. Mishra never claimed his was
optimal ("any arrangement would give a valid bound"); this only tightens the ceiling
on what those three sets can give.

What follows for Round 06:

- **§1 reads the seed correctly.** `Λ(D, B_3, B_5)` lies in `[0.8344, 0.83478095]`,
  so 0.8344 is a lower bound within `3.8×10⁻⁴` of the value.
- **§27's dominance upgrade is strict at the third rung.**
  `Λ(D, B_3, B_5) − Λ(D, P_3, P_5) ≥ 0.8344 − 0.8335974 = 0.000803`. The lower side of
  that gap is Mishra's certificate; the upper side is a placement.
- **The refutation attempts fail.** No placement goes below Mishra's 0.8344 or below
  Xie's 0.833. A search can refute a certified lower bound; it cannot confirm one.

## D — the Lipschitz transfers

**D1.** §9 and §13 rest on the margin being 1-Lipschitz in both the cover and the
target. On Round 03's grid LP this is exact: the LP value is a minimum over placements
of a maximum of 1-Lipschitz functions of the supports. Eight random cover–target pairs
were tried, each with the cover grown, the cover wobbled and the target wobbled by
`ε ∈ [0.01, 0.025]`. The wobbles were kept small enough that both bodies stay legal.
No margin moved by more than `ε`. §22's cell rule and §24's error budget are the same
inequality applied twice more.

## P — the package

**P1.** Every value in the package's `VALIDATION.json` is rebuilt:

- `λ_1`, Pál's value, 0.8344, the upper bound and the gap;
- the strict-ladder flag;
- the disc-to-triangle margin;
- `d_3 = 5` and the dimension table for `m = 2 … 7`;
- the "toy exchange budget": `δ` with `ε = τ = ζ = δ/8`, leaving a robust margin of
  `5δ/8`.

All of them are arithmetic restatements of the text — the budget, in particular,
illustrates Theorem 24.1's hypothesis rather than testing it. The package could fail
only by an arithmetic slip; the seed's substance is in W1–W5, not here.

**P2.** The package's description of its two documents — SHA-256, bytes, `$$` count
and parity, the unicode-escape and bracket-delimiter flags — matches the archive.

## The theorems, read

| Round 06 | statement | verdict | note |
| --- | --- | --- | --- |
| §1 | Mishra's seed | PASS by cited theorem | X1; the certificate itself is outside the corpus |
| §2 | the seed ladder | PASS; PASS by cited theorem for the third rung | W1: the second rung is an equality |
| §3 | search gives upper bounds only | PASS | Mishra says the same of Gibbs' search |
| §4–5 | compact domain, `‖t_i‖ ≤ R` | PASS | `t_i ∈ g_iK_i ⊆` hull `⊆ B_R`. Round 05's `Φ` sharpens it: the hull holds `conv(D ∪ {t_i})`, so `Φ(‖t_i‖) ≤ Ā` and `‖t_i‖ ≤ Φ⁻¹(Ā) = 0.7212`; Mishra uses 0.70 at his target 0.8344 |
| §6 | gauge; `d_m = 3m − 4` | PASS | W4 |
| §7–8 | continuity; `𝔐(F)` compact | PASS | a minimizing cover of `F` equals a placement hull (equal area, one inside the other) |
| §9–10 | `W` 1-Lipschitz; positive off universality | PASS | Round 04 Thm 17.1; Round 03's attained minimum |
| Thm 11.1 | `δ_F > 0` if non-saturated | PASS | on the seed, `δ_{{D}} = 1/√3 − 1/2` (W2, Jung) |
| §13–16 | dictionary transfer; Thm 14.1; separating batch | PASS | |
| §17–18 | `S_F(B)`; Thm 18.1 | PASS | Round 05's Thm 11.1 argument, made quantitative |
| §19 | `d_H(V, 𝔐(F)) ≥ s` | PASS | margins are invariant under moving the cover, so the bound holds against every copy of `𝔐(F)`; attained on the seed (W3) |
| §20 | `γ_F(s) > 0`; `Λ` rises by `γ` | PASS | exact on the seed (W3) |
| §21–23 | cells, robust rule, set cover | PASS | |
| Thm 24.1 | eventual success | PASS | conditional on certified minimizer-cell covers with `τ_n → 0` |
| §25 | a semi-decision | PASS | stated as such |
| Thm 26.1, §27 | dominance; `P_n ⊆ B_n` | PASS | W6; the upgrade is null at rung two, strict at rung three (W1, W5) |
| §28 | witness-ancestry labels | n/a | definitions; the set differs from Round 05 §35's plan (`REDUCED`, `EXTENSION`, `NOVEL` are gone) |
| §29 | seed sanity | PASS | W2, W3 |
| §30–33 | strategy, oracle, compiler, search/certificate separation | PASS | procedures |
| §34 | Mishra does not do the exchange | PASS | his §6 treats a fourth body only as a cost |
| §35 | Gibbs 2014 as a search prior | PASS | X1 |
| §36 | C06-1 … 6 | n/a | deferred, each with inputs and outputs |
| §37 | S1–S3 | PASS | W4, W2, W1 |

**Placements and reflections.** `Λ` ranges over `E(2)` (§2 of Round 05), and Mishra's
definition allows reflections too. Every body in the seed ladder is achiral, so
reflections add nothing there. §6 sets reflection aside as "a discrete branch" without
counting it. With chiral witnesses it is one parity per non-disc body, halved by a
global reflection, since the disc is achiral: `2^{m−2}` branches for `m ≥ 2`. The watch
item carries on.

## A tool correction

This round's exact hull integrator shares its envelope routine with RUN-008. The
routine compared two pieces by the sign change of their difference and, when a
crossing fell exactly on a grid angle, placed the cut one step early. The level-three
optimizer found such a placement: two polygon vertices tie at the grid angle
89.296875°, and there the old integrator returned a hull `4.4×10⁻⁵` smaller than a
sampled hull of the same points — which is impossible. An optimizer is an adversary to
its objective's artefacts.

The routine now bisects on the maximizing piece, follows every hand-over inside a grid
step, takes angles mod 2π, and raises an error on a chain that does not close. The
rewrite's first version still mishandled a hand-over lying exactly at angle 0, and
RUN-008's own drill caught that. RUN-008 was re-run with the corrected routine: every
check and every logged number is unchanged, to `2×10⁻¹⁵` (commit `be12d08`). This
round's numbers all come from the corrected routine, and every hull value is also
confirmed against a sampled hull.

## The status registry

Round 06's 27 judgments are reviewed, and its eight first-used phrases defined. Six of
the eight are §28's witness-ancestry labels. So are seven of the 27 judgments: the
census meets them as headings, and they are recorded as labels, not judgments.

| verdict | judgments |
| --- | ---: |
| PASS | 15 |
| PASS by cited theorem | 1 |
| n/a | 11 |

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| the margin's decimal edited in the document | 1 | A0 |
| a reference's year; the pin on Xie's title dropped | 2 | A1 |
| Mishra's error bound misquoted; Pál's pair misnamed | 2 | X1 |
| Pál's value with `√3/2` | 1 | W1 |
| the margin as `1/√3 − 1/3` | 1 | W2 |
| `γ` too small (half the distance); `γ` too large (twice it) | 2 | W3 |
| `d_m = 3m − 3` | 1 | W4 + P1 |
| Mishra's bound claimed as 0.8350; the classical family's as 0.8340 | 2 | W5 |
| the Reuleaux pentagon shrunk by 1 % | 1 | W6 |
| the margin claimed ½-Lipschitz | 1 | D1 |
| the package's robust budget margin edited | 1 | P1 |
| the package's recorded SHA-256 | 1 | P2 |
| a review dropped | 1 | R1 |

Controls: the unmodified inputs; `γ` written with `arctan(√(s² − r²)/r)` in place of
`arccos(r/s)`; the document with CRLF line endings; `d_m` written `3(m − 1) − 1`.

**17 / 17 plants, 4 / 4 controls, 255 / 255 must-stay-green assertions; no check
without a plant.** The level-three search is computed once and cached under the hash
of the code it depends on, so every case and every blind run reads the same search.

| check blinded | cases reported blind | plants naming it |
| --- | ---: | ---: |
| A0 | 1 | 1 |
| A1 | 2 | 2 |
| X1 | 2 | 2 |
| W1 | 1 | 1 |
| W2 | 1 | 1 |
| W3 | 2 | 2 |
| W4 | 1 | 1 |
| W5 | 2 | 2 |
| W6 | 1 | 1 |
| D1 | 1 | 1 |
| P1 | 2 | 2 |
| P2 | 1 | 1 |
| R1 | 1 | 1 |

## What this round does not establish

- The next witness: Round 06 defers it (C06-2 … 6), and nothing here searches for one.
- Mishra's `0.8344`: only its statement, its setup and his two published placements are
  checked; the certificate is not re-run.
- That certified minimizer-cell covers with `τ_n → 0` can be built in practice —
  Theorem 24.1's hypothesis.
- `Λ(D, P_3, P_5)` or `Λ(D, B_3, B_5)` themselves: the searches give upper bounds only.