# RUN-007 — Round 04: the cover compiler holds; its sanity polygon is not quite the one it defines

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-24
**Subject:** `AMRAL_Lebesgue_Finite_Closure_Round_04_Candidate_Cover_Compiler_v0.1.md` (AMRAL-LUC-FC-R04, dated 2026-09-18) and its package (`VALIDATION.json`, `State_Crystal`), read from the archive; the package's `sanity.py` was not run
**Tools:** [`run007_round04_cover_compiler.py`](../code/run007_round04_cover_compiler.py) — this tree's own outer polygon (halfplane clipping), exact Fourier areas, sympy for the derivation
**Logs:** [`run007-round04-cover-compiler.json`](../data/gate-logs/run007-round04-cover-compiler.json); citation snapshot [`round04-citations.json`](../data/external/round04-citations.json)

**Verdict: PASS**, with one reproduction discrepancy explained to the last digit.

- Round 04 makes the cover finite: every universal cover holds a disc of radius ½ (§2);
  anchored there, an area bound `Ā` confines it to radius `R = 2Ā` (Thm 4.1);
  upward-quantized support heights on `M` directions give an outer polygon within
  Hausdorff distance `ε = q + (R + R_P)d_M` (Thm 10.1) and area `β = 2πRε + πε²`
  (Thm 12); the finite polygon dictionary brackets `a_Leb` within `β` (Thm 15.1). All
  of it holds. Eight of its ten `PROVED` are self-contained arguments; two rest on
  Steiner's formula.
- **The bounds are safe and loose.** Measured on three covers, the outer polygon's
  actual Hausdorff excess is 13 to 136 times below `ε` as used (`R = 2Ā`), and 4 to 45
  times below `ε` with the cover's true radius. Round 04 says as much (§33).
- **§33's recorded polygon is not the polygon §7–8 define.** Built from the definition,
  the sanity polygon has area `0.8336391644` and excess `0.0006224937`; the package
  records `0.8337053574` and `0.0006459850`. The difference is exactly reproduced by
  pushing six of the eight support heights that fall *exactly* on a quantization level
  up one extra level — the package's rounding guard, `10⁻¹⁴`, is smaller than the
  floating-point overshoot at six of them. The recorded polygon is still a valid outer
  polygon and every bound still holds; it is just not the one the text defines.

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

---

## What Round 04 claims

Rounds 01–03 made the targets and the placements finite for a fixed cover. Round 04
makes the cover finite:

1. **Anchor** (§2): the disc of diameter 1 is a test set and is invariant under every
   isometry, so a universal cover can be translated to contain `B_{1/2}(0)`.
2. **Radius** (Thm 4.1): a convex set containing `B_r(0)` with area at most `A` lies in
   `B_{A/r}(0)`; with Gibbs' `Ā = 0.8440935944`, `R = 1.6881871888`.
3. **Outer polygon** (§6–10): quantize `h_U(u_j)` upward to `½ + qℤ` on `M` directions,
   intersect the halfplanes; `U ⊆ P ⊆ U + εB`.
4. **Area** (Thm 12): `Area(P) ≤ Area(U) + β`.
5. **Dictionary and bracket** (§13–16): finitely many polygons, and
   `A^poly − β ≤ a_Leb ≤ A^poly`, with `β → 0`.
6. **Certificate rules** (§17–26): `W` is 1-Lipschitz in the cover; outer
   approximation cannot create false non-universality; a non-universal dictionary
   polygon prunes its whole cell; a `γ`-inflation gives strict slack at area cost
   `2πR_Pγ + πγ²`; and the global lower rule — if every dictionary polygon of area
   below `L + β` is non-universal, then `a_Leb ≥ L`.

No bound is claimed (§37, §39), and §31–32 say plainly that this is finite-resolution
convergence, not finite exact closure, and that novelty against Zeng's hierarchy is
undecided until the two are compared in full.

## A — sources

**A0.** 12 anchors pin the formulas and the sanity instance. **A1.** Round 04 cites
nothing new; its five external references were re-fetched and still match. (The first
run of A1 failed: this tree's parser read the last four digits of `arXiv:1502.01251`
as a year. The parser now requires a year to be its own token; RUN-005's results are
unchanged by the fix.)

## C — the recomputations

| check | Round 04 | recomputed | result |
| --- | --- | --- | --- |
| C1 | Thm 4.1: the triangle `conv{x, (0,r), (0,−r)}` has area `r‖x‖`, so `‖x‖ ≤ A/r`; `R = 2Ā = 1.6881871888` | the triangle's area symbolically; the arithmetic; 200 random convex bodies holding `B_{1/2}` | PASS |
| C2 | Thm 8.1: `U ⊆ P_{M,q}(U)` | this tree's polygon on three covers — §33's, Pál's hexagon, a round cover without mirror symmetry — at `M = 128, q = 5×10⁻⁴` | PASS |
| C3 | Thm 10.1: `ε = q + (R + R_P)d_M` | the three excesses of the proof — quantization `q`, the chord `R_P d_M`, the `R`-Lipschitz support `R d_M` — summed symbolically | PASS |
| C4 | Thm 10.1, measured | the polygon's actual Hausdorff excess, against `ε` with `R = 2Ā` and with the true radius | PASS — table below |
| C5 | Thm 12 and §22 | actual area inflation against `β`; Steiner's formula for `P + γB` against the area computed from the support function | PASS — Steiner agrees to `4×10⁻⁷` |
| C6 | §7, §13: the levels reach `R + q`, so every quantized cover is in the dictionary | four `q` | PASS |
| C7 | §33 and the package's record | see below | PASS, with the pinned finding |
| C8 | the package's description of its documents | SHA-256, bytes, `$$` count | PASS |

What the bounds leave:

| cover | actual excess | `ε` with `R = 2Ā` | `ε` with the true `R` | actual inflation |
| --- | ---: | ---: | ---: | ---: |
| §33: `h = 0.515 + 0.01 cos 2θ` | 0.00062 | 0.0834 | 0.0263 | 0.00088 |
| Pál's hexagon (width 1) | 0.00663 | 0.0834 | 0.0289 | 0.00805 |
| round, no mirror symmetry | 0.00061 | 0.0834 | 0.0273 | 0.00090 |

The hexagon is the tightest case, as its corners should make it: 13 times below the
bound as used, 4.4 times with the true radius. `β` as used is `0.906` — larger than
the area of any cover in the class.

**What measurement cannot see.** C4 compares a measured excess with `ε`; with `ε`
this loose, it cannot detect an error in `ε`'s formula. The drill shows it: with the
`R d_M` term dropped from `ε`, or with `q` dropped, C4 and C5 stay green and only the
symbolic derivation (C3) and the comparison with the recorded numbers (C7) catch it.
This is the same lesson as Round 03's sanity example, in a milder form: §33 can catch
a wrong construction — quantizing downward breaks containment, and C2 catches that —
but not a wrong bound.

## §33 — the recorded polygon

§33 builds the outer polygon of `h_U = 0.515 + 0.01 cos 2θ` at `M = 128`, `q = 5×10⁻⁴`
and asserts containment, excess below `ε` and inflation below `β`. All three hold. The
package records the numbers; this tree reproduces some exactly and not others:

| | recorded | from the definition |
| --- | ---: | ---: |
| `Area(U)` (exact Fourier formula) | 0.8327576726503144 | 0.8327576726503144 |
| `ε` with `R = 2Ā`; `β` | 0.08339137281575232; 0.9063953966591665 | identical |
| the convergence table (`M = 64 … 1024`, `q = M⁻²`) | | identical |
| polygon area | **0.8337053574119659** | **0.8336391643823979** |
| Hausdorff excess | **0.0006459849700081** | **0.0006224936758761** |

Why they differ. On the 128 directions, eight support heights fall exactly on a
quantization level: `h = 0.525` at `θ = 0, π`, `h = 0.505` at `θ = π/2, 3π/2`, and
`h = 0.515` at the four diagonals. There §7's `½ + q⌈(h − ½)/q⌉` should leave the
height where it is. Searching all 2⁸ ways of pushing some of those eight heights up one
level, exactly one reproduces the recorded area to `10⁻¹²`: the six at `h = 0.525` and
`h = 0.515` pushed, the two at `h = 0.505` not. That polygon's excess matches the record
to the last digit as well.

The mechanism was found afterwards, by reading — not running — the package's script.
It quantizes with `⌈(h − ½)/q − 10⁻¹⁴⌉`, a guard meant to absorb rounding error. In
floating point the quotient overshoots its integer by `4 × 10⁻¹⁴` at `h = 0.525`
(`50.00000000000004`), by `2.5 × 10⁻¹⁴` at `h = 0.515`, and by `9 × 10⁻¹⁵` at
`h = 0.505`. The guard absorbs only the last; at the other six the ceiling lands one
level up. Exactly the six the search found.

So the recorded sanity polygon is the definition's polygon with six edges moved out
by one extra level. It is still an outer polygon of `U`, and every assertion §33 makes
still holds for it. The finding is about reproduction, not correctness: anyone
building §33's polygon from the text gets different numbers from the package's, and
re-running the package's own script would never have shown it. C7 pins it — it
rebuilds the recorded polygon from the definition plus the six pinned levels and
requires both recorded numbers to `10⁻¹²`, so the explanation cannot drift.

*Correction, made before this round was reported:* the version of this paragraph first
committed said the quotient at `h = 0.505` "falls just below its integer" and gave the
quotient at `0.525` as `50.000000000000044`. Both were written without being computed.
The quotient at `0.505` is above its integer; it is the guard that falls below the
overshoot there, not the quotient below the integer.

## The theorems, read

| Round 04 | statement | verdict | note |
| --- | --- | --- | --- |
| §2 | a universal cover holds `B_{1/2}` after translation | PASS | the disc is fixed by rotations and reflections |
| Thm 4.1, Cor 4.2 | `U ⊆ B_{A/r}`; `R = 2Ā` | PASS | C1 |
| §5 | the anchored, area-bounded class is compact | PASS by cited theorem | Blaschke selection; area continuous |
| Thm 8.1, Cor 8.2 | `U ⊆ P`; universality is inherited by `P` | PASS | C2 |
| §9 | `P ⊆ B_{R_P}`, `R_P = (R+q)/cos Δ` | PASS | |
| Thm 10.1 | `P ⊆ U + εB` | PASS | C3, C4 |
| Thm 12 | `Area(P) ≤ Area(U) + β` | PASS by cited theorem | Steiner's formula; perimeter monotone under inclusion; C5 |
| §13–14 | the finite dictionary; every anchored cover has a representative | PASS | C6 |
| Thm 15.1, §16 | `A^poly − β ≤ a_Leb ≤ A^poly`; convergence | PASS by cited theorem | inherits `β` |
| Thm 17.1, §18 | `W` 1-Lipschitz in the cover; outer approximation lowers `W` by at most `ε` | PASS | |
| Thm 19.1 | a non-universal dictionary polygon prunes its cell | PASS | |
| §20–22 | `γ`-inflation: `W(P^γ) = W(P) − γ`, area cost `2πR_Pγ + πγ²` | PASS by cited theorem | Steiner; C5 |
| §23–24 | every true universal (non-universal) dictionary polygon is eventually certified | PASS | existence of finite certificates, not their size |
| §25 | global lower rule: all dictionary polygons of area below `L + β` non-universal ⟹ `a_Leb ≥ L` | PASS | the proof by contradiction is sound; this is the rule a lower-bound certificate would have to instantiate |
| §28 | certificate-safe boundary surgery | PASS | a schema: search proposes, the independent certificate decides |
| §31–32 | not exact closure; novelty against Zeng undecided | PASS | stated as it should be |

**Placements and reflections.** Round 04 enumerates covers, not placements; every
universality decision it makes is delegated to Round 03's certificate, which
enumerates both reflection branches (RUN-006). The watch item has nothing new to
check here.

## Not read in this round, on purpose

The archive holds a second AI's audit of Round 04 — a "lagged" verification and four
deep-audit passes — in the DLMVC methodology track, including a sharper radius bound
than Thm 4.1's. This round was done without reading them, so that the two audits stay
independent. They are compared when this tree reaches DLMVC.

## The status registry

Round 04's 19 judgments are reviewed; its two first-used phrases defined
(`ESTABLISHED`; `PROOF SCHEMA ESTABLISHED`). Of its ten `PROVED`, eight are
self-contained arguments (`PASS`) and two rest on Steiner's formula (`PASS by cited
theorem`).

| verdict | judgments |
| --- | ---: |
| PASS | 12 |
| PASS by cited theorem | 5 |
| n/a | 2 |

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| the triangle's area doubled; `2Ā` mis-added | 2 | C1 |
| quantization downward | 1 | C2 |
| `ε` without its `R d_M` term; without `q` | 2 | C3 + C7 (**not** C4, C5) |
| `ε` claimed to be `10⁻⁶` | 1 | C3 + C4 + C5 + C7 |
| `β` without `πε²` | 1 | C7 |
| the `γ`-inflation overhead claimed zero | 1 | C5 |
| `K_q` two levels short | 1 | C6 |
| the recorded polygon area moved by `10⁻⁹`; the pinned levels removed | 2 | C7 |
| `ε`'s formula edited in the document | 1 | A0 |
| the package's recorded SHA-256 | 1 | C8 |
| a reference's year | 1 | A1 |
| a review dropped | 1 | R1 |

Controls: the unmodified inputs; `ε` written `q + 2(R + R_P) sin(Δ/2)`; quantization
by `⌊·⌋ + 1` instead of `⌈·⌉` (it differs only on exact levels, and stays outward); the
document with CRLF line endings.

**15 / 15 plants, 4 / 4 controls, 189 / 189 must-stay-green assertions.** The first
version of this drill had no plant naming C4 — found by counting plants per check,
after the same gap in RUN-006 (see there) — and the `ε = 10⁻⁶` plant was added.

| check blinded | cases reported blind | plants naming it |
| --- | ---: | ---: |
| A0 | 1 | 1 |
| A1 | 1 | 1 |
| C1 | 2 | 2 |
| C2 | 1 | 1 |
| C3 | 3 | 3 |
| C4 | 1 | 1 |
| C5 | 2 | 2 |
| C6 | 1 | 1 |
| C7 | 6 | 6 |
| C8 | 1 | 1 |
| R1 | 1 | 1 |

## What this round does not establish

- That any real cover — Pál's, Gibbs' — is universal, or any bound: Round 04 builds the
  compiler; running it is its deferred C04-1..4.
- That the polygon dictionary can be searched in practice. It is finite; the count
  `(K_q + 1)^M` is astronomically large, and Round 04 does not claim otherwise.
- Anything about the lagged audit of Round 04, deliberately unread here.