# RUN-010 — Round 07: the lifting theorems hold, every external number checks, and one recorded lift is not a minimum

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-24
**Subject:** `AMRAL_Lebesgue_Finite_Closure_Round_07_Minimizer_Atlas_v0.1.md` (AMRAL-LUC-FC-R07, dated 2026-09-18) and its package (`VALIDATION.json`, `LOCAL_COMPUTE_SPEC.json`, `State_Crystal`, `search_prior.py`), read from the archive; `search_prior.py` read only after this tree's reconstruction, never run
**Tools:** [`run010_round07_minimizer_atlas.py`](../code/run010_round07_minimizer_atlas.py) — RUN-009's exact hull of the disc and placed Reuleaux polygons; differential evolution for the lifts and the four-body family; Mishra's full text; his repository's logs and scaling script at the commit his paper cites
**Logs:** [`run010-round07-minimizer-atlas.json`](../data/gate-logs/run010-round07-minimizer-atlas.json); snapshot [`round07-citations.json`](../data/external/round07-citations.json)

**Verdict: PASS.**

- Round 07 turns Round 06's exchange into a computation whose size need not grow with
  the number of witnesses. Its three `PROVED` all hold:
  - a new witness only has to be placed over base configurations still below the
    target (Thm 10.1);
  - different base cells may be closed by different witnesses — the witness-switching
    bound `Λ(F ∪ B) ≥ min_q max_K J_K(H(q))` (Thm 11.1);
  - a cell's representative transfers to the whole cell at an explicit area cost
    (Thm 17.1).

  Thm 17.1's cost `ω_T(τ) = 4πTτ + πτ²` is loose by π, for the same reason as Round
  05's §9: a hull holding the disc has perimeter at most 4 × its area.
- **Every external number checks.** They were read against Mishra's paper and against
  his repository at the commit the paper cites: the seed's placement, its exact and
  rigorous areas, the translation domain, the four-body optimum 0.836494901, the
  throughputs and the cost extrapolation. Round 07's §3 "domain function" `f` is
  Round 05's `Φ_{1/2}` under another name.
- **The fixed-seed lifts, rebuilt exactly.**
  - `J_{B_7} = 0.8371345`, `J_{B_11} = 0.8361324`, `J_{B_13} = 0.8359056` and
    `J_{B_9} = 0.8356307`, so the recorded ranking `B_7 > B_11 > B_13 > B_9` holds.
  - The package's sampled values run `1.4–1.8×10⁻⁶` low, as inner hulls should.
  - **B₁₃ is the exception:** the recorded 0.8359676 is not a minimum. A placement
    `6.2×10⁻⁵` lower exists; the package's small search stopped in a local minimum.
  - This tree's own search missed `B_11`'s minimum in the same way, and the package's
    placement found it. Search rankings are fragile in both directions.
- **The four-body family, searched.** An 8-D search over disc, `B_3`, `B_5`, `B_7`
  finds hull area 0.8364914, confirmed by a sampled hull to `10⁻¹⁰`. That is
  `3.5×10⁻⁶` below the repository's logged optimum, so
  `Λ(D, B_3, B_5, B_7) ≤ 0.8364914`. It is still far above 0.835: nothing here refutes
  gate R07-G1, which is equivalent to `Λ(D, B_3, B_5, B_7) ≥ 0.835`. It is also below
  the fixed-seed lift by `6.4×10⁻⁴`, which is §24's point: the base moves when the
  fourth body arrives.
- **The cost extrapolation** (5.527×10¹² boxes, 5635.8 days) is rebuilt exactly by the
  repository's own rule. That rule takes the least-squares exponent and anchors it at
  the run *farthest* from the target. Anchored at the nearest run, or at the
  least-squares centre, the same counts give 4.85–4.95×10¹² boxes, about 5,000 days,
  so the order of magnitude is robust and the digits are not.

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

---

## What Round 07 claims

1. **The seed, fixed from outside** (§1–5, §20):
   - Mishra's `D, B_3, B_5` over `q = (x_3, y_3, φ_5, x_5, y_5)`, `φ_5 ∈ [0, 2π/5)`;
   - a translation domain `|t_n| ≤ t_n(T)` from the disc–point area function `f`
     (`d⋆ = 0.693830648713` at `T = 0.8344`);
   - the best exhibited placement `q†`, with exact-kernel area 0.834780945912 and
     rigorous outer area 0.834781190917;
   - Mishra's certificate stores one bit per node, so it holds no atlas (§5).
2. **The atlas** (§6–8): only the sublevel set `Q_{<T} = {q : A(q) < T}` needs a new
   witness; cells pruned by the base bound never grow new dimensions (§13).
3. **Lifting** (§9–17): `J_K(H) = min_g Area(conv(H ∪ gK))`. Each cell is closed
   either by the base or by one witness (Thm 10.1); the witness-switching bound
   (Thm 11.1); erosion extends to a lifted witness (§14); the robust transfer
   (Thm 17.1).
4. **The first milestone** (§19–27):
   - `T_1 = 0.8350`, with the domain widened to `t_3 ≤ 0.194856180909`,
     `t_5 ≤ 0.197820670401` and a headroom of `2.19×10⁻⁴` above the seed;
   - the four-body optimum 0.836494901 and a naive 8-D cost of 5.527×10¹² boxes;
   - a search-only ranking `B_7 > B_11 > B_13 > B_9`;
   - gate R07-G1: every base placement below 0.835 is lifted by `B_7` to at least 0.835.
5. **Specifications** (§28–35, §38): the witness pool, cell schema, lineage,
   status taxonomy, a local compute spec and certificate formats; C07-1 … 5 deferred.

§43 claims no new bound and no certified witness.

## A, X — sources

**A0.** 18 anchors. **A1.** Four arXiv references re-fetched, all matching. Gibbs 2014
(arXiv:1401.8217) is new here; Round 06 had named it without listing it. Reference 2 is
Mishra's repository, cited without a commit. His paper pins commit `da956b1…`, and
that is the state read here.

**X1 — the paper (v2).**

| Round 07 | Mishra | |
| --- | --- | --- |
| worst leaf slack `1.240900×10⁻⁵` | "the smallest margin being 1.2409×10⁻⁵" | ✓ |
| rigorous floating error `1.72×10⁻⁹`; 486,799,600 nodes | the same (RUN-009) | ✓ |
| `D + B_3 + B_5 + B_7`, optimum 0.836494901 | §6.3: adding the Reuleaux heptagon raises the attainable value to 0.836494901, and the parameters from five to eight | ✓ |
| throughput | 19,648 and 11,351 boxes per second | ✓ |

**X2 — the repository, at `da956b1`.**

| Round 07 | log | |
| --- | --- | --- |
| `q†` (§20) | `ceilings.log`, all five coordinates | ✓ to `10⁻¹²` |
| exact-kernel 0.834780945912; outer 0.834781190917 | `ceilings.log` | ✓ |
| `d⋆ = 0.693830648713`; `t_3 = 0.192366411526`, `t_5 = 0.195890714644` | `domain.log` | ✓ |
| four-body optimum 0.836494901 | `scaling.log` | ✓ |
| `~5.527×10¹²` boxes, `~5635.8` days at `T = 0.835` | `scaling.log` | ✓ |

## W — the numbers, rebuilt

| check | Round 07 | rebuilt | result |
| --- | --- | --- | --- |
| W1 | §3–4: `f`, `d⋆`, `t_n(T)` | `f ≡ Φ_{1/2}` at 40 digits; `d⋆` by root-finding; `t_n` derived; 120 placements beyond the bound | PASS |
| W2 | §20: the seed | exact hull at `q†`; the classical family at the log's placement; the normalized angle; the headroom | PASS |
| W3 | §22–23: four fixed-seed lifts and their ranking | exact minima (search, and a polish from the package's placement), each confirmed by a sampled hull | PASS — with the `B_13` finding |
| W4 | §21, §24, §26: four bodies | an 8-D search, confirmed by a sampled hull | PASS |
| W5 | §21: the cost | the repository's rule, from the logged counts | PASS |

**W1 — the domain.** The area of the hull of the disc and one point at distance `d` is
Round 05's `Φ_{1/2}(d)`. Round 07's `f(d)`, taken from Mishra's `domain.py`, is the
same function written another way; they agree at 40 digits. `t_n(T)` is derived here
before reading any code. Some corner of `B_n` lies within `π/n` of the direction of its
translation `t`. So that corner sits at least `√(t² + R_n² + 2tR_n cos(π/n))` from the
centre, and past `d⋆(T)` the hull of the disc and that one corner already has area `T`.
Solving gives the text's formula. At `T = 0.8344` it matches the log to `5×10⁻¹³`. At
`T_1 = 0.8350` the text, the package's JSON and its compute spec agree with it:
`t_3 = 0.194856180909`, `t_5 = 0.197820670401`. The exclusion was also tested: 120
random placements of `B_3` or `B_5` just beyond the bound all give hulls of area at
least 0.8344.

**W2 — the seed.** At the log's full-precision `q†` this tree's exact hull is
0.8347809459115, and the log's exact kernel is 0.834780945912. The classical family at
the log's placement gives 0.833597536505196, against 0.833597536505 logged. The
normalized angle `φ_5 mod 2π/5` is `2.4128951×10⁻⁵`, and the headroom to 0.835 is
`2.1905×10⁻⁴`.

**W3 — the lifts.** For each witness, the true minimum `J_{B_n}(H†)` is taken as the
smaller of this tree's search and a polish started at the package's recorded placement:

| witness | exact minimum | found by | package, sampled | exact at the package's placement | Round 07 |
| --- | ---: | --- | ---: | ---: | ---: |
| `B_7` | 0.8371345 | search | 0.8371328 | 0.8371346 | 0.83713 |
| `B_11` | 0.8361324 | polish from the package's placement | 0.8361309 | 0.8361326 | 0.83613 |
| `B_13` | **0.8359056** | search | 0.8359676 | 0.8359690 | 0.83597 |
| `B_9` | 0.8356307 | search | 0.8356292 | 0.8356308 | 0.83563 |

The ranking by exact minima is `B_7 > B_11 > B_13 > B_9`, as recorded. All four
recorded values sit `1.4–1.8×10⁻⁶` below the exact hull at their own placement — the
deficit of a hull sampled in 1536 directions. For three of them that placement is the
minimum. For `B_13` it is not: a placement exists `6.2×10⁻⁵` below the recorded value.
The package's script, read afterwards, runs differential evolution with population 12
for 80 generations, which stopped in a local minimum. The ranking survives, because
`B_13` still sits between `B_11` and `B_9`.

The fragility runs both ways. This tree's larger search missed `B_11`'s minimum by
`7.7×10⁻⁶`, and the package's placement found it. Round 07 labels the ranking
`SEARCH-ONLY` and does not build on it. That is the right status: two independent
searches disagreed on two of four entries, and neither error changed the order.

**W4 — four bodies, and gate R07-G1.** Differential evolution over the gauge-fixed
eight parameters, then Nelder–Mead, gives hull area **0.8364914416**. A sampled hull of
the same placement agrees to `1.1×10⁻¹⁰`. That is `3.46×10⁻⁶` below the repository's
logged optimum 0.836494901, which is a numerically located value, not a claimed
minimum. So `Λ(D, B_3, B_5, B_7) ≤ 0.8364914`.

Gate R07-G1 asks that every base placement below 0.835 be lifted by `B_7` to at least
0.835. That is the same as `Λ(D, B_3, B_5, B_7) ≥ 0.835`, since base placements at or
above 0.835 need no lift. A placement below 0.835 would refute it; the search found
none, and the best lies `1.49×10⁻³` above the target. That is evidence for the gate,
not a proof of it. The four-body value also lies `6.4×10⁻⁴` below the fixed-seed lift
`J_{B_7}(H†)`, which is §24's point: when `B_7` arrives, `B_3` and `B_5` move, so no
single old minimizer can stand in for the atlas.

**W5 — the cost.** Mishra's `scaling.py` takes the least-squares exponent of the six
logged 8-D counts (5.5035) and anchors the power law at the largest-margin run
(m = 0.030), with the margin measured from the four-body optimum. Rebuilt from the
counts that way, it gives 5.5272×10¹² boxes and 5635.8 days at the median 11,351
boxes per second — the logged figures exactly.

The choice of anchor matters more than the digits suggest:

| anchored at | boxes | days |
| --- | ---: | ---: |
| the largest margin (the log's rule) | 5.527×10¹² | 5,636 |
| the least-squares centre | 4.946×10¹² | 5,043 |
| the smallest margin (nearest the target) | 4.848×10¹² | 4,943 |

The log's own local exponents run from 4.0 to 7.2, and the extrapolation spans a factor
of 7 to 20 in margin. "About five thousand days" is what these counts support.
Round 07 quotes the figure exactly and calls it an empirical extrapolation (§21), so
nothing depends on the digits.

## D — the theorems' inequalities

**D1.** Thm 17.1's `ω_T(τ) = 4πTτ + πτ²` is Steiner's increment with
`Per(C_q) ≤ 2π · 2T` (Round 04's radius bound for a hull of area below `T` holding the
disc). It holds. It is loose by π: a hull holding `B_{1/2}` has `Area ≥ Per/4`
(Round 05 §21), so `Per(C_q) < 4T` and `4Tτ + πτ²` would do.

**D2.** Thm 11.1 rests on the full hull being at least each single-witness hull. At `q†`
this tree searched the joint placement of `B_7` and `B_9`. The best joint hull is
0.8379417 (sampled: agreement `1.3×10⁻¹⁰`). That is at least both single-witness hulls
at the same placement (0.8371356 and 0.8358768), and at least both minima (0.8371345,
0.8356307), as the theorem needs. Lifts are not additive: `J_7 + J_9 − Area(H†)`
would claim 0.8379843, more than the joint minimum.

## P — the package

**P1.** Every value in `VALIDATION.json`'s search-prior block is rebuilt:

- the official areas, against the repository;
- the normalized angle and `t_{3,5}(0.835)`, to `10⁻¹³`;
- the sampled inner area, below the exact one as it must be;
- the ranking and the expected strongest witness.

The local compute spec agrees with the text on the threshold, the `φ_5` domain, both
translation bounds, the primary witness `B_7` and the fallback pool.

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

`search_prior.py`, read after the reconstruction, confirms how the package worked. It
builds hulls from 1536 sampled support directions, uses the same body orientations as
this tree, and runs a small differential evolution. That explains the `1.7×10⁻⁶`
deficits and the `B_13` local minimum; nothing else in it differs from the text.

## The theorems, read

| Round 07 | statement | verdict | note |
| --- | --- | --- | --- |
| §1, §5 | external audit; the certificate holds no atlas | PASS | X1, X2; one bit per node, as the paper describes |
| §2–4 | parameterization; the domain | PASS | W1; the reflection branch adds nothing — every body is achiral |
| §6–8 | the threshold atlas; the emitter covers `Q_{<T}` | PASS | a pruned cell's points all have area `≥ L ≥ T` |
| §9 | `J_K(H) ≥ Area(H)` | PASS | |
| Thm 10.1 | cell-local lifting | PASS | a full hull contains the base hull and each witness hull |
| Thm 11.1 | witness switching | PASS | the placements are independent, so min over them of a max is the max of the minima; D2 |
| §13 | lazy activation | PASS | a hull only grows |
| §14 | erosion extends to a lifted witness | PASS by cited theorem | Mishra's Lemma 21 (paper), applied to one more body |
| §15–16 | cell-switching verifier; local batches | PASS | |
| Thm 17.1 | robust transfer | PASS by cited theorem | Steiner and Round 04; loose by π (D1) |
| §18–19 | schema; the `T_1` root | PASS | W1 |
| §20–21 | the seed; the four-body optimum; the cost | PASS | W2, W4, W5, X2 |
| §22–25 | the search-only ranking; `B_7`'s status | PASS | W3; the `B_13` value is not a minimum, the ranking holds |
| §26–27 | gate R07-G1; the batch gate | PASS | equivalent to `Λ(D, B_3, B_5, B_7) ≥ 0.835`; W4 finds no counterexample |
| §28–35 | pool, policy, lineage, taxonomy, spec, formats | PASS | specifications; the spec matches the text (P1) |
| §36–38 | RCHM relation; ancestry; C07-1 … 5 | n/a | |

## The status registry

Round 07's 32 judgments are reviewed, and its 13 first-used phrases defined. Seven of
the 32 are §31's atlas-status labels, met by the census as headings and recorded as
labels, not judgments. One, conclusion G's boxed "FIRST ACTUAL 0.8350 CERTIFICATE:
COMPUTE-DEFERRED", was added by census v3 (RUN-003).

| verdict | judgments |
| --- | ---: |
| PASS | 17 |
| PASS by cited theorem | 1 |
| n/a | 14 |

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| the seed's exact area edited in the document | 1 | A0 |
| a reference's year | 1 | A1 |
| the leaf slack misquoted | 1 | X1 |
| the four-body optimum misquoted; one digit of `q†` changed | 2 | X2 |
| `f` with the arccos added; `t_n` taking the far corner; `d⋆` off in its last digit | 3 | W1 |
| the normalized angle; the headroom | 2 | W2 |
| `B_7`'s lift as 0.83813; the ranking as `7, 9, 11, 13` | 2 | W3 |
| the gate claimed at 0.8370 | 1 | W4 |
| the cost claimed as 5.0×10¹² boxes | 1 | W5 |
| `ω_T` without its π | 1 | D1 |
| the switching bound claimed additive | 1 | D2 |
| the recorded exact area; the spec's threshold | 2 | P1 |
| the package's recorded SHA-256 | 1 | P2 |
| a review dropped | 1 | R1 |

Controls: the unmodified inputs; `f` written as Round 05's `Φ_{1/2}`; `t_n` with
`R_n = 1/(2 cos(π/2n))`; the document with CRLF line endings; `ω_T` factored as
`πτ(4T + τ)`.

**20 / 20 plants, 5 / 5 controls, 330 / 330 must-stay-green assertions; no check
without a plant.** The searches are computed once and cached under the hash of their
own code and of the hull routines they call. Editing a check does not force a
recomputation; editing the search does. The cache was first written by the full
script; before the key was narrowed to the search code, it was confirmed to have come
from the unchanged search.

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

## What this round does not establish

- Gate R07-G1, or any bound above 0.8344: the four-body search is evidence, not a
  certificate, and the certificate is Round 07's deferred C07-1 … 5.
- `J_{B_n}` or `Λ(D, B_3, B_5, B_7)` themselves: every search value here is an upper
  bound.
- That atlas lifting is faster than the naive 8-D search. Round 07 says it does not
  know (§33), and nothing here measures it.