# RUN-011 — Round 08: the proof grammar holds, two hard leaves close at 10⁻⁴, and the verifier has no root for a mirror image

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-24
**Subject:** `AMRAL_Lebesgue_Finite_Closure_Round_08_Conditional_Lift_Certificate_v0.1.md` (AMRAL-LUC-FC-R08, dated 2026-09-18) and its package (`VALIDATION.json`, `LOCAL_COMPUTE_SPEC.json`, `CERTIFICATE_SCHEMA.json`, `State_Crystal`, `sanity.py`, `verifier_skeleton.py`), read from the archive; the two scripts read only after this tree's reconstruction, never run
**Tools:** [`run011_round08_conditional_lift.py`](../code/run011_round08_conditional_lift.py) — random boxes against the motion bound and the cores; the verifier's own inner-point bound on two live leaves, against RUN-009's exact hull; Mishra's full text (v2)
**Logs:** [`run011-round08-conditional-lift.json`](../data/gate-logs/run011-round08-conditional-lift.json); snapshot [`round08-citations.json`](../data/external/round08-citations.json)

**Verdict: PASS, with one gap in a specification.**

- Round 08 turns Round 07's lifting into a proof grammar for the first milestone,
  `T₁ = 0.835`. All five `PROVED` hold:
  - the motion bound — Mishra's Lemma 22 with any radius `R_K`;
  - the common-core theorem;
  - Mishra's erosion (Lemma 21) as its special case;
  - nested base/lift soundness (Thm 12.1);
  - the generic witness interface, within one reflection branch, where the text puts it.

  On random boxes the motion bound holds for Reuleaux polygons and for chiral Fourier
  bodies, and is attained to 95%.
- **Every constant is rebuilt:** `R_7`, `t_7⋆ = 0.196935046771`, the increment
  `2.188×10⁻⁴` and the ratio 6.83. The core thresholds `1 − R_n` match Mishra's
  Remark 24.
- **Two hard leaves, computed.** One sits at the seed with `B_7` at its best lift, the
  other at the four-body optimum. Each was bounded with the lower bound the verifier
  would use.
  - At half-width `10⁻⁴` in all eight coordinates, both leaves close: 0.8368148 and
    0.8361550. The base cores alone do not close them.
  - At `10⁻³` neither closes, which is §23's point.
  - Near the four-body optimum, leaves must be narrower than about `4×10⁻⁴`.
- **One gap (PARTIAL).** For a chiral witness — the asymmetric Fourier bodies §13 and
  §29 name as fallbacks — the root must include mirror-image placements.
  - The theorem-level text asks for that root.
  - The invariant V3, the lift stream and the package's schema have no place for it.
  - The schema also drops five of §14's eleven record fields, `reflection_symmetry`
    among them.

  `B_7` and every regular Reuleaux fallback are achiral, so the milestone path loses
  nothing.
- **The package.** Its numbers all rebuild. Its sanity body S1 is nearly round, so it
  exercises the motion bound's rotation term at about a ninth of its size. The
  verifier is a skeleton.

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

---

## What Round 08 claims

1. **The motion bound and the common core** (§1–5).
   - A placement box moves a body lying within `R_K` of its centre by at most
     `δ = √(h_x² + h_y²) + 2R_K sin(h_φ/2)`, in Hausdorff distance (§1).
   - If `h_C + δ ≤ h_{K_0}`, then `C` lies in every placement of the box (Thm 2.1).
   - There are three core providers (§3, §25):
     - Mishra's erosion `∩B(V_j, 1 − δ)`;
     - `h_K − δ`, while the curvature radius stays above `δ`;
     - any core with a finite inclusion certificate.
   - `B_3`'s orientation is the gauge, so `δ_3` has no rotation term (§5).
2. **`B_7`'s lift** (§6–9, §19).
   - The root is `φ_7 ∈ [0, 2π/7)`, `|x_7|, |y_7| ≤ t_7⋆ = 0.196935046771`.
   - The lift-box core is `C_7 = ∩B(V_j, 1 − δ_7)`.
   - Every actual hull contains `conv(D ∪ C_3 ∪ C_5 ∪ C_7)`.
   - The verifier may use inner points of the cores.
3. **Grammar and soundness** (§10–18).
   - Base leaves are `BASE-PRUNED` or `LIFT-CLOSED`; lift leaves are `PRUNED`; nothing
     may be `UNRESOLVED`.
   - A complete certificate gives `Λ(F_3 ∪ B) ≥ T_1` (Thm 12.1).
   - A failing cell is split or handed to the next witness, never lifted jointly (§13).
   - The witness record (§14); the invariants V1–V10 (§16); the stream and the package
     layout (§17–18).
4. **The milestone** (§19–27).
   - The root constants.
   - A needed increment of `2.19×10⁻⁴`, against `1.49×10⁻³` found by search: ratio
     6.83.
   - Schedulers.
   - A coarse failure is no evidence against `B_7` (§23). Only an explicit placement
     with rigorous outer area below `T_1` is (§24).
   - Acceptance with its error terms (§26).
5. **Any catalog** (§28–31).
   - The same theorem for an arbitrary witness catalog.
   - The priority `B_7, B_11, B_13, B_9`, then asymmetric Fourier bodies.
   - Certificate deduplication.
   - Six proof obligations for the implementation.
6. **Specifications** (§32–36): the compute spec, the sanity tests S1 and S2, the
   deferred runs C08-1 … 5, Round 09's topic and the checklist.

§38 claims no new bound.

## A, X — sources

**A0.** 12 anchors. **A1.** References 1, 3 and 4 were re-fetched from arXiv and
reference 5 from Crossref; all four match. Schneider is cited without edition or year,
and the record found is the second edition. Reference 2 is Mishra's repository, again
cited without a commit. Reference 6 is the AMRAL rounds themselves.

**X1 — Mishra's paper (v2).**

| Round 08 | Mishra | |
| --- | --- | --- |
| §4: the discs of radius `1 − δ` about the box-centre corners lie in every placement of the box | Lemma 21 | ✓ |
| the core is empty once `1 − δ` falls below the circumradius | the same passage | ✓ |
| §1, §5: `δ_3 = √(h_x² + h_y²)`; `δ_5` adds `2R_5 sin(h_φ/2)` | Lemma 22 | ✓ — §1 puts any `R_K` for `R_5` |
| the core empties at `δ = 1 − R_n` (W1, W3) | Remark 24: 0.422649730810 and 0.474268887881 | ✓ to `5×10⁻¹³` |
| V8: `S` trees with `L` leaves have `2L − S` nodes | §5.2, a consistency check on the search tree of Definition 30 | ✓ |
| reflections | §4.1, after Lemma 17: not needed, since `D`, `B_3` and `B_5` each have an axis of symmetry | the property a chiral witness lacks (below) |

## W — the numbers, rebuilt

| check | Round 08 | rebuilt | result |
| --- | --- | --- | --- |
| W1 | §6–7, §19–20: `R_7`, `t_7⋆`, the increment, the ratio; the core thresholds | closed forms; `t_7` by Round 07's domain rule | PASS |
| W2 | §1: the motion bound | 1,400 random placements of three Reuleaux polygons and four chiral Fourier bodies | PASS, attained to 95% |
| W3 | §2–4, §33: the cores | Reuleaux cores inside every placement of 90 random boxes; emptiness at `1 − R_n`; S1's analytic core | PASS |
| W4 | §8–9, §12: lift leaves | two hard cells at two widths, bounded by inner points | PASS — both close at `10⁻⁴`, neither at `10⁻³` |
| W5 | §16 V8: the tree identity | 200 random forests | PASS |

**W1 — the constants.** `R_7 = 1/(2 sin(3π/7)) = 1/(2 cos(π/14)) = 0.512858431636277`.
Round 07's domain rule at `T_1 = 0.835` gives `t_7 = 0.1969350467711682`; the text
has 0.196935046771. The increment `0.835 − 0.834781190917 = 0.000218809083` and the
ratio 6.8320 (text: ≈ 6.83) check. The core of a regular `B_n` empties at
`δ = 1 − R_n`: 0.422649730810, 0.474268887881 and 0.487141568364 for `n = 3, 5, 7`.
The first two are Mishra's thresholds.

**W2 — the motion bound.** Seven bodies were tested: `B_3`, `B_5`, `B_7` and four
random constant-width Fourier bodies, which are chiral. Each was placed in 40 random
boxes of half-width up to 0.02, with five placements per box.

The Hausdorff distance between two placements of one convex body is the largest
difference of their support functions, measured here in 8,192 directions. It never
exceeded `δ`, and it reached 95% of it, so the bound is close to attained.

**W3 — the cores.** For each of `B_3`, `B_5` and `B_7`, 30 random boxes of half-width up
to 0.03 were tested. Every point of the eroded core `∩B(V_j, 1 − δ)`:

- lies within `1 − δ` of every box-centre corner, so `C + δB ⊆ K_0`;
- lies within 1 of every corner of five random placements in the box.

At the regular placement, the core is nonempty at `1 − δ = R_n + 10⁻⁹` and empty at
`R_n − 10⁻⁹`.

For S1's analytic body, `R_K = 0.52`. Over 300 random boxes of half-width up to 0.003,
the core `h_{K_0} − δ` stays inside every placement, by at least `1.7×10⁻⁴`.

**W4 — two hard leaves.** A lift leaf is a product box: a base cell of half-width `h` in
all five base coordinates, times a `B_7` box of half-width `h` in `(φ_7, x_7, y_7)`. Its
lower bound is the verifier's own (§9): the hull of a 20,000-gon inscribed in the disc
and of inner points of the three eroded cores.

Two leaves were computed, each at two widths:

- the seed `q†` with `B_7` at its best lift (RUN-010), where the base family is at its
  minimum;
- the four-body optimum (RUN-010), the lowest known point of the whole family.

| leaf | `h` | base cores alone | with `C_7` | least of 120 exact hulls in the box | at 0.835 |
| --- | ---: | ---: | ---: | ---: | --- |
| seed, `B_7` at its best lift | `10⁻⁴` | 0.8345408 | **0.8368148** | 0.8371307 | `LIFT-CLOSED` |
| | `10⁻³` | 0.8325519 | 0.8342258 | 0.8371444 | unresolved |
| four-body optimum | `10⁻⁴` | 0.8347583 | **0.8361550** | 0.8364992 | `LIFT-CLOSED` |
| | `10⁻³` | 0.8326700 | 0.8337170 | 0.8365888 | unresolved |

- **At `10⁻⁴` both leaves close**, and the base cores alone would not: `B_7` does the
  work, as the grammar intends.
- **At `10⁻³` neither closes.** This is §23's point: a coarse failure says nothing
  against `B_7`.
- **The bound is sound in every leaf:** it stays below each of the 120 exact hulls
  sampled in the box.
- **How narrow the leaves must be.** The bound loses 2.9–3.4 per unit of half-width.
  The four-body optimum lies `1.49×10⁻³` above the target. So near it, leaves must be
  narrower than about `4×10⁻⁴` in each of eight coordinates. That is a local estimate
  from two widths, not a count.

**W5 — V8.** 200 random forests were grown, each from 1–5 seeds by up to 60 splits;
every one has `N = 2L − S` nodes. V8's single-root form, `N = 2L − 1`, is the case
`S = 1`.

## The gap: a chiral witness has no mirror branch

`Λ` places every body by a rigid motion, and mirror images count as placements. For
`D`, `B_3`, `B_5`, `B_7` they cost nothing, and likewise for every regular Reuleaux
polygon in §29's pool. Each has an axis of symmetry, so a mirrored placement is a
rotated one. Mishra skips reflections for exactly that reason.

Round 08 also invites chiral witnesses:

- 結論 C and §25 connect Round 02's Fourier dictionary;
- §13 and §29 list asymmetric Fourier bodies as fallbacks;
- W2's four Fourier bodies are chiral, and the motion bound holds for them.

For a chiral witness `K`, a lift tree over proper placements proves only
`J⁺_K(H(q)) ≥ T_1`. The mirror placements of `K` over `q` are its proper placements
over the mirrored base configuration `σq`, which in general lies in another base cell.
Suppose that cell is closed by a different witness `K′`. A full placement with `K`
mirrored and `K′` proper then lies in neither tree, and the certificate says nothing
about it.

The theorem-level text asks for the right thing:

- Thm 12.1's hypothesis 4 and §28's item 2 want the witness's "full relevant placement
  root";
- §31's `root_domain(K, T)` wants every placement that could bring the area below `T`.

The machinery that would carry it is missing:

- §1 and 結論 A work inside one reflection branch, and say so;
- §13 asks for a witness's complete 3-D root, but a chiral witness's root has two
  3-D components;
- V3 states only `B_7`'s root;
- the lift stream (§17) splits one `(φ, x, y)` box;
- §14's record carries `reflection_symmetry`, but the package's schema does not
  require it.

The fix is small. A witness with `reflection_symmetry = false` gets a two-component
root, or a branch as its first split, and V3 and the schema say so. Until then the
verifier invariants are PARTIAL. They are complete for the `B_7` milestone and for
every Reuleaux fallback, and incomplete for the Fourier fallback. Every theorem stands.

## P — the package

**P1.** `VALIDATION.json`'s sanity block rebuilds:

- `B_7`'s root: `R_7`, `t_7(0.835) = 0.19693504677116785` and the period `2π/7`;
- the headroom figures, `0.00021880908299998225` and `0.0014949010000000484`;
- S1's core: curvature minimum `0.33489722931226573 = 0.34 − δ`, with
  `δ = 0.005102770687734223`, and no violation in 300 placements.

The compute spec agrees with the text on:

- the target;
- `B_7`'s rotation radius `R_7`, its translation radius `t_7⋆` and its period;
- `t_3` and `t_5` at 0.835;
- the core provider;
- §29's fallback order `B_11, B_13, B_9`.

The schema's magic is §17's `LUCFC08`, and its core providers are §14's three.

The schema requires six fields of a witness record:

- `witness_id`, `representation_type`, `diameter`, `symmetry_period`;
- `core_provider_type`;
- `root_domain`, an object with no constraint.

`geometry_hash` is optional. §14 lists eleven fields, and five have no counterpart in
the schema. The verifier needs each of them:

| field | the verifier needs it for |
| --- | --- |
| `constant_width_status` | legality |
| `centering_gauge` | the centre, hence `δ` |
| `rotation_radius_bound` | `R_K`, hence `δ` |
| `translation_domain_rule` | the root |
| `reflection_symmetry` | the root's mirror branch |

**S1 tests the rotation term weakly.** Its body `h = ½ + 0.02 cos 3θ` is nearly round.
Turning it by `h_φ` moves its support by at most `0.06 h_φ`, while the motion bound
allows `2R_K sin(h_φ/2) ≈ 0.52 h_φ`.

S1's box has half-widths `0.0015`, `0.0010` and `0.006`; with the script's
`R_K = 0.55` they reproduce the recorded `δ` exactly. Suppose the rotation term is
dropped from the motion bound. In that box, 37 of 2,000 random placements then show a
deficit, of at most `3.6×10⁻⁴`. With the term in place, the recorded worst gap is
`3.1×10⁻³`.

So 300 placements would very likely catch the defect. But it would show in under 2% of
the samples, at about a tenth of the test's normal margin. W2 and W3 use Reuleaux
polygons, whose corners move by the full rotation term; the drill's plant M7 trips
both.

**P2.** The package's description of its two documents matches the archive: SHA-256,
bytes, `$$` count and parity, and the two flags. Its digests of the schema, the compute
spec and the skeleton match too.

The scripts, read after the reconstruction:

- `sanity.py` sets `R_K = 0.55` for S1's body; the true value is 0.52 (W3). A larger
  `R_K` only enlarges `δ`, so S1 stays valid.
- In `verifier_skeleton.py`, every `verify_*` function raises `NotImplementedError`.
  Its `motion_delta` and its tree identity (`nodes == 2·leaves − roots`) match the
  text.

## The theorems, read

| Round 08 | statement | verdict | note |
| --- | --- | --- | --- |
| §1 | the motion bound | PASS | a point at distance `r ≤ R_K` from the centre moves by at most `|Δt| + 2r sin(Δφ/2)`; Mishra's Lemma 22 with `R_K` for `R_5`; W2 |
| Thm 2.1 | the common core | PASS | `h_{K_g} ≥ h_{K_0} − δ ≥ h_C` in every direction; W3 |
| §3, §25 | three core providers | PASS | `h_K − δ` stays a support function while the curvature radius exceeds `δ`; the certified core is Round 03's finite-direction certificate |
| §4 | Reuleaux erosion | PASS | a point within `1 − δ` of every old corner is within 1 of every new one; Mishra's Lemma 21 |
| §5 | base-cell cores | PASS | `B_3`'s orientation is the gauge, so `δ_3` has no rotation term |
| §6–7, §19 | `B_7`'s root and lift-box core | PASS | W1; `B_7` is achiral, so `[0, 2π/7)` covers its mirror placements |
| §8–9 | the core hull; inner points | PASS | subsets of every actual hull; W4 |
| §10–11 | base and lift grammar | PASS | |
| Thm 12.1 | nested soundness | PASS | hypothesis 4 must cover every placement that could bring the area below `T_1`; for `B_7`, Round 07's a-priori domain does |
| §13 | fallback without a joint lift | PASS | each leaf needs one witness (Round 07, Thm 11.1); a chiral witness's complete root has two components |
| §14 | the witness record | PASS | the list is complete; the schema drops five of its fields (P1) |
| §15–16 | emitter and verifier; V1–V10 | **PARTIAL** | V3 gives `B_7`'s root only; nothing specifies a mirror branch |
| §17–18 | stream; package layout | PASS | a mirror branch would need its own split axis |
| §20 | the headroom | PASS | W1; with RUN-010's four-body value 0.8364914 the ratio is 6.82 |
| §21–23 | schedulers; a coarse failure is no evidence | PASS | W4 shows it: both leaves fail at `10⁻³` and close at `10⁻⁴` |
| §24 | a certified negative result | PASS | only an explicit placement with rigorous outer area below `T_1` counts |
| §26–27 | safety margins; a weaker verifier | PASS | inner points need no geometric margin, only a floating one |
| §28–29 | any catalog; `B_7` first, then Fourier | PASS | item 2, the "full relevant placement root", is where a chiral witness's mirror branch belongs |
| §30–31 | deduplication; proof obligations | PASS | `root_domain(K, T)`: every placement that could bring the area below `T` |
| §32–33 | compute spec; S1, S2 | PASS | P1 |
| §34–35, §37–38 | deferred runs; Round 09; handoff; declaration | n/a | |

## The status registry

Round 08's 29 judgments are reviewed, and its 13 first-used phrases defined. Sixteen of
the 29 are grammar tokens and labels, recorded as such rather than as judgments:
`LIFT-CLOSED`, `BASE-PRUNED`, `SPLIT`, `PRUNED`, `UNRESOLVED`, the three core
providers, §24's two witness labels and `NOT PROOF PATH`.

| verdict | judgments |
| --- | ---: |
| PASS | 10 |
| PARTIAL | 1 |
| n/a | 18 |

The PARTIAL is §36's `SPECIFIED` for the independent verifier invariants.

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| the document's `t_7⋆` edited | 1 | A0 |
| a reference's year | 1 | A1 |
| Mishra's `B_3` threshold misquoted | 1 | X1 |
| `R_7` or `t_7` off in the last digit; the ratio as 6.93 | 3 | W1 |
| the motion bound without its rotation term | 1 | W2, W3 |
| the core eroded by `δ/2` | 1 | W3 |
| the coarse seed leaf claimed closed; the four-body cell claimed base-pruned | 2 | W4 |
| the tree identity for one root | 1 | W5 |
| the spec's `t_7`; `reflection_symmetry` assumed in the schema; S1's `δ` shifted | 3 | P1 |
| the schema's recorded digest | 1 | P2 |
| a review dropped | 1 | R1 |

Four controls:

- the unmodified inputs;
- the motion bound's `2 sin(x/2)` written as `4 sin(x/4) cos(x/4)`;
- the document with CRLF line endings;
- the tree identity written `L + (L − S)`.

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

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

## What this round does not establish

- **`Λ(D, B_3, B_5, B_7) ≥ 0.835`, or any bound above 0.8344.** Two leaves are two
  cells of an atlas nobody has built. Their closing shows the mechanism works where the
  margin is thinnest; it does not show that the atlas closes.
- **A rigorous leaf.** The inner hulls here are computed in floating point, with no
  error term. Their margins, `1.2×10⁻³` and `1.8×10⁻³`, dwarf rounding, but a
  certificate needs §26's `e_fp`.
- **That the atlas is affordable** at leaf widths near `4×10⁻⁴` in eight coordinates.
  That is Round 09's subject.
- **That any verifier works:** the package's verifier is a skeleton.