# RUN-008 — Round 05: the saturation theory holds; its sanity test could not have caught a wrong bound

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-24
**Subject:** `AMRAL_Lebesgue_Finite_Closure_Round_05_Saturation_Gate_v0.1.md` (AMRAL-LUC-FC-R05, dated 2026-09-18) and its package (`VALIDATION.json`, `State_Crystal`, `sanity.py`), read from the archive; the package's `sanity.py` was read but not run (see *Process* below)
**Tools:** [`run008_round05_saturation_gate.py`](../code/run008_round05_saturation_gate.py) — this tree's own cells, cell members and exact piecewise integrals; sympy for the derivations; the arXiv abstracts of Mishra and Zeng
**Logs:** [`run008-round05-saturation-gate.json`](../data/gate-logs/run008-round05-saturation-gate.json); citation snapshot [`round05-citations.json`](../data/external/round05-citations.json)

**Verdict: PASS.**

- Round 05 splits "saturation" in two. **Completeness in the limit** —
  `a_Leb = sup_F Λ(F) = lim λ_m` over finite witness families — is proved.
  **Exact finite saturation** — some `λ_m` already equal to `a_Leb` — is stated as a
  conjecture and left `OPEN`. On the upper side the round adds four cell-local area
  lower bounds, two prune rules and asymptotic localization. All eleven `PROVED`
  hold; seven are self-contained, four rest on classical theorems (Blaschke
  selection; Steiner's, Cauchy's and Minkowski's formulas).
- **Two proofs, read closely.** §9's continuity bound
  `4πĀε + πε²` holds but is loose by exactly π: §21's own inequality
  `Area ≥ (r/2)·Per` gives `Per(U_K) ≤ 4Ā`, hence `4Āε + πε²`, and that constant is
  essentially attained inside the class (a heptagon circumscribed about the disc has
  area `0.84276 ≤ Ā` and perimeter exactly 4 × its area). And Theorem 11.1's
  *statement* — no false permanent saturation — already follows in one line from
  §7's `λ_m → a_Leb`; what its proof adds is the mechanism, a finite batch of
  witnesses that separates the whole minimizer set, which is what §17 and Round 06
  build on.
- **The cell bounds are safe.** On 20 cells built here (five covers, four grids) no
  bound exceeds the area of any member found, including the smallest members a local
  search could reach; at the coarsest grid `LB_cell` comes within `1.3×10⁻³` of the
  smallest member. `ε_b` is 2.8 to 3.2 times tighter than Round 04's global `ε`, as
  §19 says.
- **The package's numbers reproduce, with two remarks.** Its five cells are rebuilt
  from the text's definitions to `10⁻¹²` (no rounding-guard trouble this time: at
  `M = 1024` the nearest support height sits `6×10⁻⁵` of a step from a level). But
  its `LB_env` is a 200,000-point rectangle rule, not the integral §21 defines — four
  of five recorded values *exceed* the exact integral, by up to `1.4×10⁻⁹`; harmless
  here, not certified. And its one assertion, that every bound stays below the
  candidate's area, **could not have failed** for the errors that matter: with the
  `Per·ε` term dropped from `LB_outer`, or one `R_b d_M` dropped from `ε_b`, it stays
  green. The candidate is smooth, and around a smooth body the term is never needed.
  Around straight edges it is: for the heptagon circumscribed about the disc — inside
  `C_Ā` — `LB_outer` without `Per·ε` would claim more than the heptagon's own area.
  This tree's cells catch that; nothing measured catches the other omission, only the
  derivation. Round 03's lesson again.
- **External claims hold as stated.** Mishra's abstract names the disc, the Reuleaux
  triangle and the Reuleaux pentagon and the bound 0.8344; Zeng's states
  `a_Leb = lim Λ_M`. All three of Mishra's bodies have constant width 1 and a mirror
  axis, so for this family reflections add nothing: the reflection watch item holds
  trivially.
- **This tree's own example.** `Λ({D, RT}) = π/8 + √3/4 ≈ 0.8257118`, proved here, so
  `λ_2 ≥ 0.8257` — strictly between `λ_1 = π/4` and Mishra's `λ_3 ≥ 0.8344`.

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

---

## What Round 05 claims

Rounds 01–04 made targets, placements and covers finite. Round 05 asks when a finite
hierarchy can actually *stop*.

1. **Convergence is not attainment** (§1): `⌊nα⌋/n → α` but never equals an
   irrational `α`; a bracket with `β → 0` does not by itself give an exact finite level.
2. **The finite-witness functional** (§2–5): for a finite family `F ∋ D = B_{1/2}` of
   unit constant-width bodies, `Λ(F) = inf_{g_i ∈ E(2)} Area(conv ∪ g_i K_i)`. Then
   `Λ(F) ≤ a_Leb` (Thm 3.1), the infimum is a minimum over covers (§4), and fit sets are
   closed (Thm 5.1).
3. **Completeness** (Thm 6.1): `a_Leb = sup Λ(F)` over finite families.
4. **The ladder** (§7–10): `λ_m = sup{Λ(F) : |F| ≤ m}` increases to `a_Leb`; each
   `λ_m` is attained, by the continuity bound `|Λ(K) − Λ(L)| ≤ 4πĀε + πε²`;
   `λ_1 = π/4`; Mishra's family gives `λ_3 ≥ 0.8344`.
5. **Saturation** (§11–17): if `λ_m < a_Leb` then some `λ_{m+r} > λ_m` (Thm 11.1), so
   the ladder cannot plateau below the truth (§12); exact closure happens iff a finite
   lower witness meets a certified upper cover (Thm 14.1, §15–16).
6. **Cell bounds and prunes** (§18–28): for the quantized cell `𝔠(b)` with outer
   polygon `P_b`, `d_H(U, P_b) ≤ ε_b = q + 2R_b d_M` (§19), and four safe area lower
   bounds — `πr²`, `LB_outer`, `LB_env`, `LB_tip` (§20–23); a non-universal `P_b` or
   `LB_cell ≥ A⁺` prunes the whole cell (§24); strictly non-universal and strictly
   suboptimal limits are eventually pruned (§26–27), so surviving cells localize at
   optimal universal covers (§28) — asymptotically, not in finitely many steps.

§32 states the Finite Witness Attainment Conjecture (`∃ m⋆: λ_{m⋆} = a_Leb`) as open,
and §38 claims no new bound.

## A, X — sources

**A0.** 16 anchors pin the formulas below as written. **A1.** Round 05 cites nothing
new; its five external references were re-fetched and still match; reference 6 is the
corpus itself (RUN-001). **X1.** §10 and §31 say what two of those references prove.
Mishra's abstract (arXiv 2608.30538, v2) lists exactly the disc, the Reuleaux triangle
and the Reuleaux pentagon as its test sets and proves area at least 0.8344 for every
convex universal cover; Zeng's (2609.01284, v1) states `a_Leb = lim_{M→∞} Λ_M` for its
monotone finite-arc values. Both claims are as Round 05 reports them. Mishra's
certificate itself is not checked here — reproducing it is Round 05's deferred C05-1.

## W — the witness ladder

| check | claim | recomputed | result |
| --- | --- | --- | --- |
| W1 | `λ_1 = π/4 ≈ 0.7853981634`; gap `0.0096935944` | the disc is its own smallest cover; the decimal; the gap as exact rationals | PASS |
| W2 | *this tree's own:* `Λ({D, RT}) = π/8 + √3/4` | three ways — below | PASS |
| W3 | Mishra's three bodies are achiral | constant width 1 and a mirror axis, searched over all axes | PASS — residual `≤ 3.3×10⁻¹⁶` |

**W2 — a second rung.** Round 05 computes `Λ` only for the disc. The next family,
`{D, RT}`, has an exact value. Place the Reuleaux triangle concentric with the disc:
its vertices sit at `1/√3` from the centre, and the arc through a vertex has its
tangent there at distance exactly ½ from the centre (`A·(A − B) = ½`), so each arc
leaves its vertex along a line tangent to the disc and then bends inside. The hull is
the disc plus three tips, each of area `Φ_{1/2}(1/√3) − π/4`:
`Area = π/4 + 3(Φ − π/4) = π/8 + √3/4 = 0.8257117836`. The hull of the sampled
bodies agrees to `8×10⁻¹¹`.

No other placement does better. Rotations are absorbed by the disc and the triangle is
achiral, so only the offset `t` matters. The hull contains the disc and the three
vertices `p_k = a_k + t`. If some `|p_k| ≥ 0.7`, the area is already
`≥ Φ(0.7) = 0.83655`, more than the value. Otherwise two vertices a width 1 apart,
both within 0.7 of the centre, are more than 90° apart as seen from it, while two tip
half-widths are at most `2 arccos(0.5/0.7) = 88.8°`; so the tips are disjoint and the
area is `π/4 + Σ tip(|p_k|)`. The tip area `Φ(s) − π/4` (zero inside the disc) is
convex and increasing (`Φ'' = r³/(s²√(s² − r²)) > 0`), and `Σ|a_k + t|` is convex and
threefold symmetric, so it is least at `t = 0`. Jensen and monotonicity then give
`Σ tip(|p_k|) ≥ 3 tip(mean |p_k|) ≥ 3 tip(1/√3)`. A grid of 96 offsets agrees: every one enlarges the
hull, the least by `1.0×10⁻⁵`.

So `λ_2 ≥ π/8 + √3/4 ≈ 0.8257`. It is this tree's example, not a Round 05 claim: it
exercises §2's definition on a family where `Λ` is exact and uses §22's `Φ` in an
independent context.

*Forward note.* Round 06 (§2) quotes the same number as Pál's classical value for the
disc and the unit equilateral triangle, and uses it as a lower bound for `Λ(D, B_3)`.
The argument above uses only the three vertices, so it proves that classical value as
well — and it shows the bound is attained: at this rung the Reuleaux triangle adds
nothing to the triangle it is built on. RUN-009 takes this up with Round 06.

## D — the formulas, derived again

| check | Round 05 | derived from | result |
| --- | --- | --- | --- |
| D1 | §19: `ε_b = q + 2R_b d_M` | the proof's two one-sided bounds, `h_P(v) ≤ b_j + R_b d_M` and `h_U(v) ≥ b_j − q − R_b d_M`, subtracted; `d_M = 2 sin(π/2M)` is the farthest any direction sits from the grid | PASS |
| D2 | §20: `LB_outer = Area(P_b) − Per(P_b)ε_b − πε_b²` | Steiner's increment `εPer(U) + πε²` with `Per(U) ≤ Per(P_b)` | PASS |
| D3 | §21: `LB_env = ¼∫ℓ_b` | Minkowski's `Area = ½∫h dS ≥ (r/2)Per` for `h ≥ r`; Cauchy's `Per = ∫h`; support functions of bodies in `B_R` are `R`-Lipschitz on the circle (random polygons) | PASS |
| D4 | §22: `Φ_r(s) = πr² + r√(s² − r²) − r² arccos(r/s)`, increasing | the disc plus two right triangles (legs `r`, `√(s² − r²)`) minus the sector of angle `2 arccos(r/s)`; `Φ' = r√(s² − r²)/s`, at 50 digits | PASS |
| D5 | §9: `|Λ(K) − Λ(L)| ≤ 4πĀε + πε²` | Steiner's increment with `Per(U_K) ≤ 2πR`, `R = 2Ā` (Round 04) | PASS |

§21 writes `ℓ_b` with a radius `R` it does not fix. Any `R` with `U ⊆ B_R` works; the
package takes `R_b` from §19, which is valid, since every member of the cell lies in
`P_b ⊆ B_{R_b}`. N3 measures both `R_b` and Round 04's `R = 2Ā`.

## N — the cell bounds, measured

The cells are built here from five covers holding `B_{1/2}(0)` — Round 04's §33
candidate `h = 0.515 + 0.01 cos 2θ`, a cover without mirror symmetry, the hull of the
disc and the Reuleaux triangle, the regular heptagon circumscribed about the disc
(area `7 tan(π/7)/4 = 0.842756`, inside `C_Ā`; six of its seven edges are normal to no
grid direction used here), and
Pál's hexagon — at `(M, q) = (8, 1/64)`, `(16, 1/256)`, `(32, 1/1024)`, `(64, 1/4096)`.
The hexagon (area `√3/2`) lies outside `C_Ā`; none of the bounds' proofs use the area
constraint, so it stays as a second straight-edged test.

A cell's members are made as `conv(B_{1/2} ∪ {x_j})` with `x_j` in the slab
`{x ∈ P_b : x·u_j ≥ b̲_j}`: the member closest to the disc (`x_j` nearest the origin),
eight random members, and — at `M ≤ 16` — the result of a 300-step descent on area.
Each member's area and perimeter are computed exactly from its support function,
integrated in closed form between the angles where the maximum changes hands (checked
against sampled hulls to `10⁻⁸`).

| check | Round 05 | measured | result |
| --- | --- | --- | --- |
| N1 | §18–19: each cover lies in the cell of its own quantized supports, inside `P_b`; every member within `ε_b` of `P_b` | 20 cells; Hausdorff distance sampled at 2¹⁶ angles plus the Lipschitz half-step | PASS |
| N2 | §22: `Φ_r(s)` is the hull area of a disc and a point | hulls of a 400,000-point disc and a point, `s` from ½ to `2Ā` | PASS — agreement `≤ 3.3×10⁻¹¹` |
| N3 | §20–23: every bound is safe | each bound against the smallest member of each cell; `ℓ_b` integrated exactly, with `R_b` and with `2Ā` | PASS — table below |
| N4 | §9 and §21: `Per ≤ 2πR ≤ 4πĀ`; `Area ≥ (r/2)Per`; the bound's Steiner increment | 60 bodies of `C_Ā`: tangential polygons, the disc, random hulls | PASS |

N1 in numbers: 230 members over the 20 cells, every one inside `ε_b` — the farthest at
5 to 24 % of it, so `ε_b` is safe and 4 to 20 times loose. `ε_b` is 2.8 to 3.2 times
smaller than Round 04's global `ε_{M,q}` on every cell.

N3, at the coarsest and finest grid of each cover (all 20 cells are in the log):

| cover | `M` | `LB_outer` | `LB_env` | `LB_tip` | `LB_cell` | smallest member found | margin |
| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: |
| §33 candidate | 8 | −1.3423 | 0.7856 | 0.7867 | 0.7867 | 0.7880 (closest) | 0.0013 |
| §33 candidate | 64 | 0.6575 | 0.7937 | 0.7880 | 0.7937 | 0.8314 (random) | 0.0377 |
| no mirror symmetry | 8 | −1.3800 | 0.7859 | 0.7867 | 0.7867 | 0.7918 (closest) | 0.0051 |
| no mirror symmetry | 64 | 0.6619 | 0.7952 | 0.7885 | 0.7952 | 0.8377 (random) | 0.0425 |
| disc + Reuleaux triangle | 8 | −1.4827 | 0.7889 | 0.7953 | 0.7953 | 0.8242 (descent) | 0.0289 |
| disc + Reuleaux triangle | 64 | 0.6317 | 0.8157 | 0.7988 | 0.8157 | 0.8257 (the cover) | 0.0100 |
| heptagon | 8 | −1.5463 | 0.7891 | 0.7919 | 0.7919 | 0.8168 (closest) | 0.0249 |
| heptagon | 64 | 0.6620 | 0.8236 | 0.7936 | 0.8236 | 0.8428 (the cover) | 0.0191 |
| hexagon | 8 | −1.5978 | 0.7921 | 0.7953 | 0.7953 | 0.8462 (descent) | 0.0510 |
| hexagon | 64 | 0.6732 | 0.8460 | 0.7988 | 0.8460 | 0.8660 (the cover) | 0.0200 |

At coarse grids `LB_outer` is negative — `ε_b` is then of the order of the cover itself —
and `LB_tip` or `LB_env` carries the bound; by `M = 64` `LB_env` leads everywhere. The
closest approach, `1.3×10⁻³`, is at `M = 8` on the §33 candidate, whose cell's
smallest member is almost the disc. `LB_env` with Round 04's `R = 2Ā` is never larger
than with `R_b`, as it should be.

N4's largest perimeter is `0.9984 × 4Ā`, reached by the heptagon circumscribed about
the disc (`Per = 4·Area` exactly, area `0.84276`) — the `4Ā` of the sharper §9 bound,
not the `4πĀ` Round 05 uses.

## P — the package

**P1.** The package's `VALIDATION.json` records the cells of Round 04's §33 candidate at
`M = 64 … 1024`, `q = M⁻²`. From the text's definitions this tree rebuilds every
recorded number — vertex count, area, perimeter, `R_b`, `ε_b`, `LB_outer`, `LB_env`,
`LB_combined`, the candidate's area `0.8327576726503144`, `λ_1`, the anchors and the
gap — to `10⁻¹²`. Three remarks:

1. *Rounding.* Round 04's package pushed six on-level heights one level too far
   (RUN-007). Here no height is near a level: the closest, at `M = 1024`, is `6×10⁻⁵`
   of a step away. The definition reproduces the record directly.
2. *`LB_combined` omits `LB_tip`.* §23 allows enabling only a cheaper subset in
   practice, and on these cells `LB_tip ≈ 0.788` never exceeds the others, so the full
   §23 bound would differ only through the quadrature below.
3. *`LB_env` is a quadrature.* §21 defines an integral; the package records a
   200,000-point rectangle rule. Integrated exactly:

   | `M` | recorded `LB_env` | exact `¼∫ℓ_b` | recorded − exact |
   | ---: | ---: | ---: | ---: |
   | 64 | 0.7936755224944383 | 0.7936755210933901 | +1.40×10⁻⁹ |
   | 128 | 0.7996297467317487 | 0.7996297463977708 | +3.34×10⁻¹⁰ |
   | 256 | 0.8039144600812937 | 0.8039144597314679 | +3.50×10⁻¹⁰ |
   | 512 | 0.8064287142947868 | 0.8064287143856450 | −9.09×10⁻¹¹ |
   | 1024 | 0.8076952824221812 | 0.8076952822898363 | +1.32×10⁻¹⁰ |

   The exact integral is taken piece by piece in closed form between the angles where
   the envelope changes hands. It is checked twice: against a closed form (one tent,
   to every digit), and against a 2²²-point rectangle rule on the `M = 64` cell (to
   `1.3×10⁻¹¹`, with rectangle rules of growing size converging onto it like `n⁻²`).

   Four of five recorded values lie above the exact integral, so they are not what §21
   proves: §21 proves `¼∫ℓ_b`, and these exceed it. Here the margins to the candidate's
   area are at least ten million times larger and nothing changes; a certificate built
   this way would need the exact integral or a quadrature error bound.

**What the package's assertion could see.** Its only test is that every `LB_combined`
stays below the candidate's own area. Run on its five cells with deliberately wrong
formulas:

| wrong formula | largest bound on the five cells | the package's assertion |
| --- | ---: | --- |
| `LB_outer` without its `Per·ε` term | 0.83273 | green — the candidate's area is 0.83276 |
| `ε_b` with one `R_b d_M` instead of two | 0.82754 | green |
| `LB_env` with factor ½ instead of ¼ | 1.61539 | trips |
| `LB_outer = Area(P_b)` | 0.83387 | trips |

A bound too large by a factor, or one that ignores the polygon's excess altogether, is
caught; a bound missing one of its correction terms is not. The reason is the
candidate's shape. Around this smooth, nearly round body the outer polygon's excess is
second order in the grid spacing (with `q = M⁻²`, as here), and `πε_b²` alone already
exceeds it — 7.6 times over at `M = 64` — so for this candidate the `Per·ε` term is not
needed, and a test built on it cannot show that it is.

It is needed around straight edges. Where an edge of the cover is not normal to a grid
direction, the outer polygon leaves a thin roof over it, first order in the spacing.
For the heptagon circumscribed about the disc at `M = 64`, `P_b` exceeds the heptagon by
`0.01333` while `πε_b² = 0.00941`, so `LB_outer` without its `Per·ε` term would claim
`0.84667` for a cover of area `0.84276` inside `C_Ā`. N3 catches that plant on exactly
two of its 20 cells, the heptagon's and the hexagon's at `M = 64`; the hull of the disc
and the Reuleaux triangle has straight edges too, but short ones, and does not show it.
The error grows with refinement: the roof is first order in the spacing, `πε_b²` second,
so the finer the grid, the surer a straight edge exposes it. The other
omission — one `R_b d_M` dropped from `ε_b` — is caught by nothing measured, here or in
the package; only the derivation (D1) and the exact reproduction (P1) see it.

It is Round 03's lesson (RUN-006) once more: the package's sanity example could not
have failed for the error that matters most for straight-edged covers — and Pál's
hexagon, where the known covers start, is all straight edges.

**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 05 | statement | verdict | note |
| --- | --- | --- | --- |
| §1 | convergence ≠ attainment | PASS | |
| §2 | `Λ(F)`; the disc may be fixed | PASS | one isometry applied to the whole configuration |
| Thm 3.1 | `Λ(F) ≤ a_Leb` | PASS | a cover holds every placed hull |
| §4 | the infimum is a minimum over covers | PASS by cited theorem | `C_Ā` compact (Round 04 §5: Blaschke selection); fit sets closed; area continuous. Needs `D ∈ F` to anchor |
| Thm 5.1 | fit sets closed | PASS | `O(2)` compact, translations bounded, a convergent subsequence |
| Thm 6.1 | `a_Leb = sup Λ(F)` | PASS by cited theorem | `Λ ≤ A` gives a cover of area `≤ A` only because §4's minimum is attained; FIP in the compact `C_A`; Round 01's reduction makes the common cover universal. `E(2)` here matches Round 01's definition |
| §7 | `λ_m ↑ a_Leb` | PASS | immediate from Thm 6.1 |
| §8–9 | `λ_m` attained; continuity bound | PASS by cited theorem | Steiner; the tuple fixes `K_1 = L_1 = D`, so both covers anchor and the swap is legitimate. Bound loose by π (D5, N4) |
| §10 | `λ_1 = π/4`; `λ_3 ≥ 0.8344` | PASS (`λ_1`); PASS by cited theorem (`λ_3`) | W1, X1. Mishra bounds the hull of copies of the three bodies, which is exactly `Λ({D, RT, R5}) ≥ 0.8344`; the certificate itself is outside the corpus |
| Thm 11.1 | `λ_m < a_Leb ⟹ λ_{m+r} > λ_m` | PASS | `M_m`, taken anchored in `C_Ā`, is compact; the non-fit sets are open; a finite subcover gives the batch. The statement alone follows from §7 |
| §12–13 | no false plateau; the dichotomy | PASS | |
| Thm 14.1, §15–16 | exact closure iff lower = upper; `Γ ≥ 0`; the squeeze | PASS | |
| §17 | one violated target need not raise `Λ`; a separating batch is needed | PASS | the reading of Thm 11.1's proof |
| §18–19 | the cell; `U ⊆ P_b`; `d_H ≤ ε_b` | PASS | `b̲_j ≥ b_j − q` is exactly the bound the proof uses (D1, N1) |
| §20 | `LB_outer` | PASS by cited theorem | Steiner; perimeter monotone under inclusion (D2, N3) |
| §21 | `LB_env` | PASS by cited theorem | Cauchy and Minkowski (D3, N3); `R` unspecified — any valid radius |
| §22 | `Φ_r`; `LB_tip` | PASS | D4, N2 |
| §23 | `LB_cell`, safe | PASS | N3 |
| §24–25 | prunes P1, P2; active cells | PASS | P1 by Round 04 Cor 8.2 |
| §26 | strictly non-universal limits are pruned eventually | PASS | Round 04 Thm 17.1; needs Round 03's certificates to exist for `W(P_n) > δ/2`, not their size |
| §27 | strictly suboptimal limits are pruned eventually | PASS | `LB_outer → Area(U)` |
| §28 | surviving cells localize at optimal universal covers | PASS | uses: `W(U_∞) ≤ 0` means universal (margins attained, Round 01 compactness), and `A_n⁺ ≥ a_Leb`. Asymptotic only, as the section says |
| §29–30 | stopping criterion; architecture | PASS | organizational |
| §31 | Mishra and Zeng as interfaces; `CROSS-MAP: OPEN` | PASS | X1 |
| §32–33 | the attainment conjecture, and its branch-type fallback | n/a | conjectures, stated as such |

**Placements and reflections.** `Λ` is defined over `E(2)` (§2), reflections included,
which matches Round 01. The only concrete family in the round is Mishra's, and all
three of its bodies are achiral (W3), so the reflection branch changes nothing for it.
The watch item stays open for later rounds: any chiral witness must enumerate `σ = −1`.

## Process

This tree's rule is to reconstruct first and read an author's script only afterwards,
forensically. In this round the package's `sanity.py` was opened in the same step that
listed the round's registry entries — before the reconstruction. What it contributed:
that `LB_env` was taken as a 200,000-point rectangle rule with `R = R_b`. Everything else
here — cells, members, exact integrals, derivations — is built from the text, and the
verdict on `LB_env` rests on the exact integral, not on the script. The slip is recorded
so that the independence of this round is not overstated.

## The status registry

Round 05's 18 judgments are reviewed, and its two first-used phrases defined:
`FORMALIZED` (the theory is written out as definitions and proved statements; nothing is
computed, and finite attainment stays `OPEN`) and `FALSE-POSITIVE` — not a status at all
but one of §35's five witness-ancestry labels for Round 06.

| verdict | judgments |
| --- | ---: |
| PASS | 10 |
| PASS by cited theorem | 4 |
| n/a | 4 |

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| `ε_b`'s formula edited in the document | 1 | A0 |
| a reference's year | 1 | A1 |
| Mishra's bound edited in the abstract; the family misnamed | 2 | X1 |
| `λ_1`'s decimal; the gap's last digit | 2 | W1 |
| a chiral body in place of the Reuleaux pentagon | 1 | W3 |
| `Φ`'s sector added instead of subtracted | 1 | D4 + N2 + N3 + W2 |
| `Φ` without its protrusion (`πr²` alone) | 1 | D4 + N2 + W2 (**not** N3: a bound too small is still safe) |
| `ε_b` with one `R_b d_M` | 1 | D1 + P1 (**not** N1, N3) |
| `ε_b` claimed to be `10⁻⁹` | 1 | D1 + N1 + N3 + P1 |
| `LB_outer` without `Per·ε` | 1 | D2 + N3 + P1 (N3 through the two straight-edged cells only) |
| `LB_outer = Area(P_b)` | 1 | D2 + N3 + P1 |
| `LB_env` with factor ½ | 1 | D3 + N3 + P1 |
| §9's bound with `Per ≤ πĀ` | 1 | D5 + N4 |
| §9's bound without `πε²` | 1 | D5 (**not** N4: `Per ≤ 4Ā` leaves the room) |
| the cell's lower edge set to its upper edge | 1 | N1 + P1 |
| quantization downward | 1 | N1 + P1 |
| the recorded `LB_env` moved by `10⁻⁹` | 1 | P1 |
| the package's recorded SHA-256 | 1 | P2 |
| a review dropped | 1 | R1 |

Controls: the unmodified inputs; `ε_b` written `q + 4R_b sin(π/2M)`; `Φ` with
`arctan(√(s² − r²)/r)` in place of `arccos(r/s)`; the document with CRLF line endings;
§9's bound factored as `πε(4Ā + ε)`; `LB_outer` factored as `A − ε(Per + πε)`.

**21 / 21 plants, 6 / 6 controls, 447 / 447 must-stay-green assertions; no check
without a plant.** The first run of this drill had one failure, and it was the
expectation that was wrong. It had been set from the smooth candidate: that no
measurement could see `LB_outer` lose its `Per·ε` term. N3 tripped, on the hexagon's
`M = 64` cell. Finding out why led to the straight-edge mechanism and to the heptagon
inside `C_Ā` (P above); the heptagon was added as a fifth cover and the expectation
set to what the cells show.

| check blinded | cases reported blind | plants naming it |
| --- | ---: | ---: |
| A0 | 1 | 1 |
| A1 | 1 | 1 |
| X1 | 2 | 2 |
| W1 | 2 | 2 |
| W2 | 2 | 2 |
| W3 | 1 | 1 |
| D1 | 2 | 2 |
| D2 | 2 | 2 |
| D3 | 1 | 1 |
| D4 | 2 | 2 |
| D5 | 2 | 2 |
| N1 | 3 | 3 |
| N2 | 2 | 2 |
| N3 | 5 | 5 |
| N4 | 1 | 1 |
| P1 | 8 | 8 |
| P2 | 1 | 1 |
| R1 | 1 | 1 |

## Correction — the envelope routine

*Made during RUN-009, the same day.* The exact envelope routine behind every hull area,
perimeter and `∫ℓ_b` in this round compared two pieces by the sign change of their
difference. When a crossing fell exactly on a grid angle the difference vanished there,
and the cut went one grid step early. RUN-009 found it when its optimizer settled on
such a placement — two vertices tying at the grid angle 89.296875° — and the "exact"
hull came out `4.4×10⁻⁵` below a sampled hull of the same points.

The routine now locates every hand-over by bisection on the maximizing piece and
follows every hand-over inside a grid step. It takes angles mod 2π, and raises an
error on a chain that does not close. Its first rewrite still mishandled a hand-over
lying exactly at angle 0; this round's own drill caught that, when the plant that sets
each cell's lower edge to its upper edge produced a member of area 0.744 — less than
`π/4`, which no body holding the disc can have. With the corrected routine the whole
round was run again. Every check passes, and every logged number is unchanged to
`2×10⁻¹⁵`. The drill is again 21 / 21, 6 / 6, 447 / 447. The blind table depends only
on which plants name which checks, so it is unchanged.

## What this round does not establish

- Anything about the value of `a_Leb`, or any new bound: Round 05 claims none (§38).
- Mishra's `0.8344`: only its abstract's statement is checked. Reproducing the
  certificate is Round 05's own deferred C05-1.
- That the Finite Witness Attainment Conjecture is true or false.
- That the branch-and-bound terminates: §26–28 are asymptotic, and nothing here runs a
  search.
- `λ_2`: W2 gives `λ_2 ≥ π/8 + √3/4` from one family; whether the Reuleaux triangle
  maximizes `Λ({D, K})` is not examined.