# RUN-012 — Round 09: the cost layer is sound, the common core closes cells 2.2× wider than the representative prune, and dominance pruning has nothing to prune

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-24
**Subject:** `AMRAL_Lebesgue_Finite_Closure_Round_09_Adaptive_Atlas_v0.1.md` (AMRAL-LUC-FC-R09, dated 2026-09-18) and its package (`VALIDATION.json`, `LOCAL_COMPUTE_SPEC.json`, `State_Crystal`, `sanity.py`), read from the archive; `sanity.py` read only after this tree's reconstruction, never run
**Tools:** [`run012_round09_adaptive_atlas.py`](../code/run012_round09_adaptive_atlas.py) — support functions of placed bodies and their hulls; RUN-009's exact hull; exact support pieces for the eroded cores, new here; Mishra's repository at the commit his paper pins
**Logs:** [`run012-round09-adaptive-atlas.json`](../data/gate-logs/run012-round09-adaptive-atlas.json); snapshot [`round09-repository.json`](../data/external/round09-repository.json)

**Verdict: PASS.**

- Round 09 adds no proof domain; it prices Round 08's certificate. Everything it calls
  `PROVED` holds:
  - the Hausdorff radius of a cell (Thm 1.1, §2–4);
  - the sharpened transfer (Thm 6.1);
  - the margin-to-resolution formula;
  - the representative prune;
  - core-dominance reuse (Thm 19.1);
  - witness dominance (Thm 22.1);
  - the finite depth bound;
  - the scheduler's one-step optimality for the radius bound.
- **Round 09 makes the fix this tree recorded twice.** Its "R07-STRENGTHENING-001" —
  `Per ≤ 4 Area` for a hull holding `B_{1/2}` — is why RUN-008 and RUN-010 found
  Round 05's and Round 07's bounds loose by π. On random hulls of the root, the new
  bound is within 5.3% of tight.
- **Every number rebuilds:**
  - `τ_root = 0.6046803712` and the five one-split radii, so the first cut is `φ_5`;
  - `τ⋆ = 4.4738688×10⁻⁴` against Round 07's `1.4246152×10⁻⁴`, ratio 3.1404;
  - the package's values, to `4.5×10⁻¹³` relative.
- **Mishra's code, read at the pinned commit, is as Round 09 describes it.** Its split
  rule weights the angle axis by the pentagon's circumradius, and its body pieces have
  support `cx cos t + cy sin t + r`.
- **The representative prune against the common core, measured.** At RUN-011's two
  leaves, the representative prune closes cells up to half-width `3.3×10⁻⁴` and
  `2.3×10⁻⁴`. The exact common core closes them up to `7.3×10⁻⁴` and
  `5.1×10⁻⁴`: 2.2 times wider in each of eight coordinates. For Reuleaux witnesses,
  both prunes cost one hull of 31 pieces. Trying the representative prune first is
  sound, but near the frontier it never replaces the core.
- **Witness dominance has nothing to prune in the pool Round 08 names.** Every witness
  there has constant width 1. A body of constant width 1 lies in no other set of
  diameter 1 except a congruent copy, so §23's Pareto pruning can only remove
  duplicates.
- **Two corrections to this tree's own RUN-011.**
  - Its inner-point bound left out the cores' corners, and lost `1–4×10⁻⁵` by it.
  - Its estimate of about `4×10⁻⁴` for the widest closing cell near the four-body
    optimum is, with the exact core, `5.1×10⁻⁴`.

  Neither changes a RUN-011 verdict.

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

---

## What Round 09 claims

1. **The cell radius** (§1–4, 結論 A).
   - The convex hull does not increase Hausdorff distance (Thm 1.1).
   - So a cell's hulls stay within `τ(C) = max_i δ_i` of its centre's hull.
   - For `D + B_3 + B_5`, `τ = max(δ_3, δ_5)`; with a witness box added,
     `s = max(τ, δ_K)`.
2. **The transfer** (§5–7, 結論 B–C).
   - A body holding `B_r` has `Area ≥ (r/2) Per`, so `Per ≤ 4 Area` here.
   - So a centre hull of area at least `T + 4Tτ + πτ²` closes its cell (Thm 6.1).
   - This improves Round 07's `4πTτ + πτ²` and is labelled a strengthening, not a
     correction.
3. **Resolution and scheduling** (§8–14, 結論 D–F).
   - A margin `m` closes cells of radius up to
     `τ⋆(m, T) = (√(4T² + πm) − 2T)/π`.
   - At the four-body search headroom, `τ⋆ ≈ 4.47×10⁻⁴`, against `1.42×10⁻⁴` under
     Round 07's cost.
   - Split the axis that most reduces `τ`. At the `0.835` root that is `φ_5`.
   - Mishra's weight `R_5 h_φ` is the first-order term of `2R_5 sin(h_φ/2)`.
4. **Prunes, tags and reuse** (§15–21, 結論 G–H).
   - A cascade: a-priori, representative, common core, then split.
   - Proof-mode tags `APR`, `REP`, `CORE`, `SUPPORT-CORE`, `OTHER-VERIFIED`.
   - A lift tree closing one base cell also closes any cell whose base core contains
     the first's (Thm 19.1). The containment is checkable in closed form (§20).
5. **Witnesses** (§22–24, 結論 I).
   - A witness containing another lifts at least as high (Thm 22.1).
   - Pareto pruning of the pool.
   - Weighted set cover.
6. **Depth** (§25–28, 結論 J).
   - Full refinement cycles give `τ_r ≤ 2^{−r} S_0`.
   - So a positive margin closes at a finite depth.
   - What survives refinement is the zero-margin frontier.
   - Two scheduling heuristics.
7. **Specifications** (§29–32): the numerical sanity, C09-1 … 5 deferred, Round 10's
   topic and the checklist.

Round 09 has no reference list. It leans on Mishra's code twice (§0 E, §20); X1 reads
that code.

## A, X — sources

**A0.** 30 anchors. There is no reference list to check.

**X1 — Mishra's repository, at `da956b1`.**

| Round 09 | the repository | |
| --- | --- | --- |
| §0 E, §14: the official split weight `R_5 h_{φ5}` | `verifyB.py` halves the widest of `(b[1], b[3], CIRC5*b[5], b[7], b[9])`, with `CIRC5` the pentagon's circumradius | ✓ |
| §20: pieces `c_x cos θ + c_y sin θ + r` | `geom.py`: support `<c_j, u(theta)> + r_j` per piece, "a single sinusoid plus a constant" | ✓ |
| §10: a split halves `h_a` | the children are widened by `1e-11` relative, so that they provably cover the parent | the text's `h/2` is the exact-arithmetic ideal |

## W — the numbers, rebuilt

| check | Round 09 | rebuilt | result |
| --- | --- | --- | --- |
| W1 | §1–4: the cell radius | 80 random cells, base and joint, six placements each | PASS, `d_H/τ ≤ 0.77` |
| W2 | §5–7: `Per ≤ 4 Area`; the transfer | 40 random hulls; 30 cells | PASS, within 5.3% of tight |
| W3 | §8–9, §29: `τ⋆` | closed form by computer algebra; the numbers | PASS |
| W4 | §10–14: the scheduler | the root's radii; the first cut; the Taylor term; both rules for 16 cuts | PASS |
| W5 | §15–16: representative against core | RUN-011's two leaves; the widest closing cells | PASS — the core closes 2.2× wider |
| W6 | §18–21: core dominance | exact core pieces; containment from merged breakpoints; Thm 19.1 | PASS |
| W7 | §22–23: witness dominance | `P_3 ⊆ B_3`, `P_5 ⊆ B_5` at random placements; the pool's width | PASS — the pool is complete |
| W8 | §25: the depth bound | 41 cells × 25 cycles; the root | PASS, 11 cycles |

**W1 — the cell radius.** Each test cell lies inside the `0.835` root: 80 random cells,
half of them with a `B_7` box. Their half-widths range over nine halvings of the
root's. The support difference between the hull at a random placement and the hull at
the centre is the Hausdorff distance, measured here in 4,096 directions. It never
exceeded `τ` (or `s`), and at most it reached 77% of it. The hull moves less than its
worst body, because a body moves the hull only where it is extreme.

**W2 — the transfer.** Over 40 random hulls of the root, half with `B_7`, the smallest
value of `4 Area/Per` is 1.0535, so `Per ≤ 4 Area` is within 5.3% of tight. Round 07's
`Per ≤ 4πT` exceeds it by a factor near π; that is the looseness RUN-008 (§9) and
RUN-010 (D1) recorded. On 30 random cells, the transfer that Steiner's formula and
this inequality give, `Area(H(q)) ≥ (Area(H_C) − πτ²)/(1 + 4τ)`, held with at least
`1.8τ` to spare.

**W3 — resolution.** Computer algebra confirms that `τ⋆(m, T, r)` solves
`(2T/r)τ + πτ² = m`, and that it reduces to the text's form at `r = ½`. At
`m = 0.001494901`:

| | rebuilt | text |
| --- | ---: | ---: |
| `τ⋆` | `4.47386884564525×10⁻⁴` | `4.47387×10⁻⁴`, `0.0004473869` |
| Round 07's | `1.42461518527477×10⁻⁴` | `1.42462×10⁻⁴`, `0.0001424615` |
| ratio | 3.14040513669 | ≈ 3.14 |

The old root is written here as `(m/π)/(√(4T² + m/π) + 2T)`. The direct form
`√(4T² + m/π) − 2T` loses about four digits to cancellation. The package's values show
it at `4×10⁻¹³` relative.

**W4 — the scheduler.** At the root, with `h_{x3} = h_{y3} = t_3`, `h_φ = π/5` and
`h_{x5} = h_{y5} = t_5`:

| | rebuilt | text |
| --- | ---: | ---: |
| `d_3` | 0.2755682538 | 0.2755682538 |
| `τ_root = d_5` | 0.6046803712 | 0.6046803712 |
| `τ` after halving `x_3` or `y_3` | 0.6046803712 | 0.6046803712 |
| after halving `φ_5` | **0.4442456056** | 0.4442456056 |
| after halving `x_5` or `y_5` | 0.5460899294 | 0.5460899294 |

So the first cut is `φ_5`. §14's expansion
`2R sin(h/2) = Rh − Rh³/24 + O(h⁵)` is confirmed by computer algebra.

Mishra's weight rule also cuts `φ_5` first. After that the two rules part: the exact
rule cuts `φ_5, φ_5, x_5, φ_5, x_3, …`, Mishra's `φ_5, x_5, y_5, x_3, y_3, …`. Along
one path, after 16 cuts, the exact rule reaches `τ = 0.0545` and Mishra's 0.0556, 2%
apart. Mishra's rule spends cuts on `B_3`'s axes that leave `τ` unchanged. They still
help the core prune, which depends on each body's radius separately.

Round 09 claims optimality only "for the certified radius bound", and that is exactly
right. Which rule makes the smaller certificate is C09-5, deferred.

**W5 — two prunes at RUN-011's leaves.** The two leaves are:

- the seed with `B_7` at its best lift;
- the four-body optimum.

Each is a product box of half-width `h` in all eight coordinates. The representative
bound is the exact area at the centre, minus `4Ts + πs²` with `s` the largest motion
radius. The core bound is the exact area of `conv(D ∪ C_3 ∪ C_5 ∪ C_7)`.

| leaf | `h` | centre area | representative | exact core | RUN-011's inner points |
| --- | ---: | ---: | ---: | ---: | ---: |
| seed, `B_7` at its best lift | `10⁻⁴` | 0.8371345 | 0.8364865 | 0.8368352 | 0.8368148 |
| | `10⁻³` | | 0.8306433 | 0.8342397 | 0.8342258 |
| four-body optimum | `10⁻⁴` | 0.8364914 | 0.8358434 | 0.8361916 | 0.8361550 |
| | `10⁻³` | | 0.8300002 | 0.8337265 | 0.8337170 |

- Both bounds stay below every exact hull RUN-011 sampled in the box.
- Both close at `10⁻⁴` and fail at `10⁻³`.
- The widest cell each closes, found by bisection:

| leaf | representative | core | ratio |
| --- | ---: | ---: | ---: |
| seed, `B_7` at its best lift | `3.29×10⁻⁴` | `7.30×10⁻⁴` | 2.22 |
| four-body optimum | `2.30×10⁻⁴` | `5.08×10⁻⁴` | 2.21 |

The representative prune charges the whole perimeter for moving by `s`. The core pays
nothing where the disc, which never moves, forms the hull. §9's "3.14× relaxation"
compares the new representative cost with the old one, not with the core.

For Reuleaux witnesses, both prunes compute one hull of 31 support pieces. So
representative-first saves work only where cores are dear: the certified cores of
Fourier witnesses (Round 08 §25). Near the frontier it never replaces the core. That
is a measurement at two points, not a count, and Round 09 defers the count (C09-4, 5).

**W6 — core dominance.** Checking §20's claim needs the eroded cores exactly. Each core
`∩B(V_j, 1 − δ)` is represented here by support pieces:

- an arc of radius `1 − δ` about each corner;
- the points where the arcs about adjacent corners meet, which are its own corners.

At `1 − δ = 1` the pieces are the Reuleaux polygon's own. With its corners added, a
dense set of points inside the cores comes within `6.2×10⁻⁷` of the exact core hull.
Without the corners it falls up to `9.5×10⁻⁵` short: a core's corner is often an
extreme point of the whole hull.

§20's test was then rebuilt. The breakpoints of both envelopes are merged. On each
interval the difference `h_a − h_b` is one sinusoid plus a constant, and its least
value is taken in closed form. Over 36 pairs of base cells, that minimum is attained
at the angle it names, and no dense sample falls below it. The containing pairs were:

| pairs | containing |
| --- | ---: |
| same centre, the second coarser | 12 of 12 |
| centres shifted | 11 of 12 |
| a parent's core inside its child's | 5 of 12 |

Thm 19.1 held in all 56 trials with a `B_7` core.

The parent–child row is worth knowing. Refinement does not make cores monotone: a
child is eroded less, but around a different centre. So a cache cannot infer
containment from ancestry, and §21's explicit check is needed every time. Nothing is
lost by this: a parent's certificate already covers its children.

**W7 — witness dominance.** Thm 22.1 was tested with the triangle inside the Reuleaux
triangle and the pentagon inside the Reuleaux pentagon, at the same placement, over
random base hulls. The Reuleaux body's hull was never smaller; it was larger by up to
0.091.

Round 08's pool, however, is `B_7, B_11, B_13, B_9` and constant-width Fourier bodies.
All have width 1, and the regular ones are checked to `2.2×10⁻¹⁶`. The argument:

1. For two bodies of constant width 1,
   `h_L(θ) − h_K(θ) = −(h_L(θ + π) − h_K(θ + π))`.
2. So if `h_K ≤ h_L` everywhere, the difference is zero everywhere.
3. Hence a body of constant width 1 lies inside another set of diameter 1 only if the
   two are congruent.

Within the named pool, dominance matches congruent copies only, and §23's pruning has
nothing to remove. It matters for non-complete witnesses, such as polygons or an
oracle's output.

**W8 — depth.** Over 41 cells, `τ` after `r` full cycles stays below `2^{−r} S_0` for
all `r ≤ 24`. At the root:

- `S_0 = 0.6101`;
- `⌈log₂(S_0/τ⋆)⌉ = 11` cycles, and 11 are needed;
- that is 55 halvings on every path. Uniform refinement to that depth would make
  `2^55` cells, as the text itself calls "extremely conservative".

The theorem needs `m` to bound the margin of every representative the refinement
meets, as §26 says. 結論 J's "some representative" is looser than what the proof
uses. A margin at a single centre promises nothing about the children: any cell
around the seed, whose base area is below 0.835, never closes on the base alone.

## P — the package

**P1.** `VALIDATION.json` rebuilds to `4.5×10⁻¹³` relative:

- the root's `δ_3`, `δ_5` and `τ`;
- the five child radii, the best axis and its radius;
- `τ⋆` new and old, and their ratio;
- `Ω` new and old at `10⁻⁴`.

The compute spec's target is 0.835. Two gaps against the text:

- its proof modes are §17's tags less `OTHER-VERIFIED`;
- `SUPPORT-CORE` is a declared mode with no leaf count among its metrics.

**P2.** The package's description of both documents matches the archive: SHA-256,
bytes, `$$` count and parity, and the two flags. So does its digest of the compute
spec.

**`sanity.py`, read after the reconstruction.**

- It computes exactly the recorded numbers.
- It uses `R_5` rounded to 12 digits and the direct formulas for both roots, which
  accounts for the `4×10⁻¹³`.
- It asserts nothing: `"status": "PASS"` is written as a constant.

## RUN-011, revisited

- **The inner points.** RUN-011's inner-point bound was a valid lower bound, but it
  left out the cores' corners. At the two leaves it fell `0.95–3.7×10⁻⁵` below the
  exact core hull; with the corners it comes within `1.3×10⁻⁷` (W5). Round 08 §9 would do
  well to say that a verifier's inner points should include each core's corners, which
  are exact intersections of two circles.
- **The widest cell.** Near the four-body optimum, RUN-011 estimated that leaves must
  be narrower than about `4×10⁻⁴`, by a linear extrapolation from two widths. The
  exact core closes up to `5.1×10⁻⁴`.

Both RUN-011 verdicts stand.

## The theorems, read

| Round 09 | statement | verdict | note |
| --- | --- | --- | --- |
| Thm 1.1, §2 | the hull is Hausdorff non-expansive; the family radius | PASS | `X ⊆ Y + δB` gives `conv X ⊆ conv Y + δB`; W1 |
| §3–4 | `τ = max(δ_3, δ_5)`; `s = max(τ, δ_K)` | PASS | Round 08's motion bound per body; W1 |
| §5 | `Area ≥ (r/2) Per` | PASS | `h_U ≥ r`, and `Area = ½∫h dS`; W2 |
| Thm 6.1, §7 | the sharpened transfer | PASS | Steiner, and §5 applied to the hull whose area is bounded; only that one needs to hold `B_r`; W2 |
| §8–9, §29 | margin to resolution | PASS | W3 |
| §10–14 | the exact split scheduler | PASS | optimal for `τ` among single bisections, as claimed; W4 |
| §15–17 | representative prune; cascade; tags | PASS | Thm 6.1 on the joint box; W5 measures what it closes |
| §18–21 | core dominance; containment; cache | PASS | Thm 19.1 is monotonicity of the hull; §20 rebuilt; W6 |
| Thm 22.1, §23 | witness dominance; Pareto pruning | PASS | W7; vacuous within a constant-width pool |
| §24 | weighted set cover | PASS | coverage alone carries correctness |
| §25–26 | depth bound; the zero-margin frontier | PASS | with `m` a uniform lower bound on every representative's margin, as §26 states; W8 |
| §27–28 | priority score; split or lift | n/a | heuristics, kept out of the verifier by the text itself |
| §30–33 | deferred runs; Round 10; checklist; handoff | n/a | |

## The status registry

Round 09's 15 judgments are reviewed, and its 4 first-used phrases defined: `REP`,
`PROVED FOR THE CERTIFIED RADIUS BOUND`, `R07-STRENGTHENING-001` and
`STILL COMPUTE-DEFERRED`. The census as first run listed two of §0's three boxed
verdicts. The third, "HEAVY 0.8350 CERTIFICATE: STILL COMPUTE-DEFERRED", was missed
then and is read by census v3 (RUN-003); §32 records the same state as `NOT YET CERTIFIED`.

| verdict | judgments |
| --- | ---: |
| PASS | 10 |
| n/a | 5 |

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| the document's `τ_root` edited | 1 | A0 |
| Mishra's split weight misread | 1 | X1 |
| the family radius without its rotation term | 1 | W1 |
| `Per ≤ 2 Area` | 1 | W2 |
| `τ⋆` off in its tenth digit; the ratio as 3.14² | 2 | W3 |
| `τ_{x5}` off in its tenth digit; the first cut as `x_5` | 2 | W4 |
| the representative cost without its 4; the representative prune claimed to close wider cells | 2 | W5 |
| containment decided at interval ends only | 1 | W6 |
| dominance reversed | 1 | W7 |
| `S_0` without its rotation term | 1 | W8 |
| a recorded child radius; `OTHER-VERIFIED` assumed in the spec | 2 | P1 |
| the crystal's recorded digest | 1 | P2 |
| a review dropped | 1 | R1 |

Four controls:

- the unmodified inputs;
- the radius's `2 sin(x/2)` written as `4 sin(x/4) cos(x/4)`;
- the document with CRLF line endings;
- the representative cost factored as `s(4T + πs)`.

**17 / 17 plants, 4 / 4 controls, 256 / 256 must-stay-green assertions; no check
without a plant.**

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

## What this round does not establish

- **The scheduler's or the cache's gain.** Round 09 defers both (C09-3, 5). The
  measurements here are two points and one path.
- **How often cross-cell reuse applies** in a real atlas: that too is C09-3.
- **Any bound above 0.8344.** Round 09 claims none.