# RUN-005 — Round 02: the finite shape compiler holds, and its error bound is safe by a wide margin

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-24
**Subject:** `AMRAL_Lebesgue_Finite_Closure_Round_02_Finite_Compiler_v0.1.md` (AMRAL-LUC-FC-R02, dated 2026-09-18) and its package (`VALIDATION.json`, `State_Crystal`), read from the archive; the package's `sanity.py` was not run
**Tools:** [`run005_round02_finite_compiler.py`](../code/run005_round02_finite_compiler.py), [`gate.py`](../code/gate.py) — exact rational kernel coefficients, sympy for the symbolic chain, mpmath at 40 digits
**Logs:** [`run005-round02-finite-compiler.json`](../data/gate-logs/run005-round02-finite-compiler.json); citation snapshot [`round02-citations.json`](../data/external/round02-citations.json) (retrieved 2026-09-24)

**Verdict: PASS**, with one displayed digit wrong.

- Every step of the compiler holds: squared-Fejér smoothing `𝒥_N` keeps a body legal
  (Thm 4.1), the explicit error `E_N = π²(4N+1) / (2(2N²+4N+3)(N+1))` is derived
  correctly (§5–9), interiorization and quantization keep legality with
  `A_N = (4/3)(N−1)N(N+1)` (§12–17), and the finite dictionary exists with error
  `E_N + δ/2 + (N−1)q` (Thm 20.1).
- **`E_N` is valid and conservative.** The exact second moment of the kernel, computed
  from its rational Fourier coefficients, gives a bound `μ₂,N/2` that is 29% of
  `E_N` at `N = 1` and 15% at `N = 256`. On the Reuleaux triangle — the least smooth
  constant-width body — the actual smoothing error is about 9% of `E_N`.
- **Every number in the sanity example (§32) reproduces** from exact kernel multipliers
  (`140/163`, `108/163`), within `10⁻⁹` of the package's values and on the side grid
  sampling predicts. **One displayed digit is wrong:** the quantized curvature maximum
  is shown as `0.77710000…`; it is `0.7771000125…`. No consequence.

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

---

## What Round 02 claims

Round 01 left the target family as an infinite-dimensional domain `𝓡`. Round 02
claims a **finite legal dictionary**: for every resolution `ε` there is a finite,
explicitly enumerable set of genuine centred unit constant-width bodies, every
target within `ε` of one of them in Hausdorff distance. Three layers:

1. **smoothing** `h ↦ 𝒥_N h = J_N * h` by the squared-Fejér kernel `J_N = F_N²/S_N`,
   which keeps width, convexity, the Steiner gauge and `0 ≤ r ≤ 1` exactly (Thm 4.1),
   with `‖𝒥_N h − h‖∞ ≤ E_N` (§9);
2. **interiorization** `h ↦ (1−δ)𝒥_N h + δ/2`, pushing `r` into `[δ/2, 1−δ/2]` at a
   cost of `δ/2` (§12–13);
3. **quantization** of the `2(N−1)` odd coefficients to a grid of spacing `q`, legal
   when `qA_N ≤ δ/2` (§16–17), at a cost of `(N−1)q` (§18).

Then a sandwich (§25) turns the dictionary into two finite certificate rules for a
fixed candidate cover: all dictionary shapes fit with slack `ε` ⟹ universal (Rule A);
one dictionary shape does not fit ⟹ not universal (Rule B). No bound on `a_Leb` is
claimed, and §27 and §36 say plainly that placements remain continuous.

## A — sources

**A0.** The formulas recomputed below are pinned to the document: 12 anchors.

**A1.** Round 02 cites four works beyond those already verified:

| # | Round 02 cites | found |
| ---: | --- | --- |
| 5 | Bari, *A Treatise on Trigonometric Series*, Pergamon, 1964 | doi:10.1016/c2013-0-08001-2 (Elsevier, the Pergamon imprint's owner; the record lists no authors — title and year compared) |
| 6 | Zygmund, *Trigonometric Series*, Cambridge University Press | doi:10.1017/CBO9781316036587, the 2003 Cambridge edition, whose record also credits C. Fefferman (its foreword) |
| 7 | Shah, Urschel, West, *What is Jackson's constant?*, arXiv:2607.23375, 2026 | arXiv v1 2026-07-25 |
| 8 | Schneider, *Convex Bodies: The Brunn–Minkowski Theory*, Cambridge University Press | doi:10.1017/CBO9781139003858 |

§9 calls `E_N` "本輪自行推導" (derived in this round). It is a Jackson-type estimate of
a standard shape; nothing in Round 02 depends on its being new, and B below
re-derives it rather than trusting either the derivation or the literature.

## B — the kernel error `E_N`

| check | Round 02 | recomputed | result |
| --- | --- | --- | --- |
| K1 | §5: `F_N(t) = Σ_{|k|≤N} (1 − |k|/(N+1)) e^{ikt}` | both sides at `2N+3` points, 40 digits, `N = 1..16` — two trigonometric polynomials of degree `N` agreeing at `2N+1` points are equal | PASS |
| K2 | §6: `S_N = (2N²+4N+3)/(3(N+1))` | the Parseval sum, symbolically in `N` | PASS |
| K3 | §9: `∫₀^{t₀} t²(N+1)² = π³/(3(N+1))`, `∫_{t₀}^{π} π⁴/((N+1)²t²) = π³N/(N+1)²`, their sum over `πS_N`, and `E_N` as half of it | symbolically in `N` | PASS |
| K4 | §9: `F_N(t) ≤ N+1` and `F_N(t) ≤ π²/((N+1)t²)` on `(0, π]` | grid, `N = 1..64` (evidence; the proof is `sin(t/2) ≥ t/π` by concavity) | PASS — equality at `t = π` for even `N` |
| K5 | the bound is valid: `μ₂,N/2 ≤ E_N` | the **exact** `μ₂,N = π²/3 + 4 Σ_{k=1}^{2N} c_k (−1)^k/k²` from the rational coefficients `c_k` of `J_N`, `N = 1..64, 128, 256` | PASS — ratio below |
| K6 | §22's table of `E_N` for `N = 8 … 256` | `E_N` rounded to 10 decimals | PASS — all six entries |
| K12 | "for every centred unit constant-width body" | the Reuleaux triangle: its exact Fourier series through the exact multipliers of `J_N` | PASS — below |

How much room the bound leaves:

| `N` | exact `μ₂,N / 2` | `E_N` | ratio | Reuleaux triangle, actual `‖𝒥_N h − h‖∞` |
| ---: | ---: | ---: | ---: | ---: |
| 1 | 0.3949 | 1.3708 | 0.288 | |
| 2 | 0.1837 | 0.7792 | 0.236 | 0.0606 |
| 8 | 0.01932 | 0.1110 | 0.174 | 0.00965 |
| 64 | 3.574 × 10⁻⁴ | 2.309 × 10⁻³ | 0.155 | 2.02 × 10⁻⁴ |
| 256 | 2.275 × 10⁻⁵ | 1.490 × 10⁻⁴ | 0.153 | |

Two losses make `E_N` about 6.5 times the exact moment bound for large `N`: §9
bounds `F_N²` by `(N+1)²` on the whole of `[0, π/(N+1)]` and by the Jordan tail
beyond, and `‖h''‖∞ ≤ 1` is used although a constant-width body's `h''` can be
smaller (the Reuleaux triangle's is `1/√3`). Neither is an error — §22 itself calls
these "proof-level coarse bounds" with "很大常數優化空間". It matters only for size:
the dictionary grows like `(⌈4/q⌉+1)^{2(N−1)}` with `q ≲ δ/A_N`, so a bound 6.5
times too large means a larger `N` for the same `ε`. That is a question for the
deferred census C02-1, not for correctness.

## C — quantization and the dictionary

| check | Round 02 | recomputed | result |
| --- | --- | --- | --- |
| K7 | §16: `Σ_{j=1}^{N−1} ((2j+1)² − 1) = (4/3)(N−1)N(N+1)`; §35's `q ≤ 3δ/(8(N−1)N(N+1))` is `qA_N ≤ δ/2`; §21's choices give `5ε/6` | symbolically | PASS |
| K8 | §19: coefficients may be boxed in `[−2, 2]`; `|𝒟| ≤ (⌈4/q⌉+1)^{2(N−1)}` | for `0 ≤ h ≤ 1`, `|a_j| ≤ (1/π)∫|cos| = 4/π`; rounding with `q ≤ ½` adds at most `¼`, so every coefficient stays within `1.53`; the grid `qℤ ∩ [−2,2]` has `2⌊2/q⌋+1 ≤ ⌈4/q⌉+1` points | PASS — with room: `4/π` is sharper than §19's `2` |

## D — the sanity example

§32 runs the compiler once, on `r = ½ + 0.25 cos 3θ + 0.15 sin 5θ` with `N = 8`,
`δ = 0.1`. It does not state `q`; the package's `VALIDATION.json` does:
`q = 0.025/672`, so that `qA₈ = 0.025` — half the margin `δ/2`. With that `q`, every
number was recomputed from the exact multipliers of `J₈` at the two modes present,
`ĵ(3) = 140/163` and `ĵ(5) = 108/163`, and extremes found as roots of the derivative
(K9):

| quantity | §32 shows | the package records | recomputed |
| --- | --- | --- | --- |
| `min r`, `max r` | `0.1076858…`, `0.8923141…` | 0.10768588783870783, 0.8923141121612922 | 0.10768588783870782, 0.89231411216129218 |
| smoothing error | `0.006394669…` | 0.006394669208304116 | 0.00639466922143404 |
| `E₈` | `0.111007820…` | 0.11100782046215024 | 0.11100782046215025 |
| interiorized `r` range | — | 0.2226468354…, 0.7773531646… | 0.22264683443315808, 0.77735316556684192 |
| quantized `r̂` range | `0.22289999…`, **`0.77710000…`** | 0.2228999876…, 0.7771000124… | 0.22289998745740615, **0.77710001254259385** |
| total support error | `0.00946175…` | 0.009461749658347007 | 0.0094617496713189537 |
| theorem bound `E₈ + δ/2 + 7q` | — | 0.1612682371288169 | 0.16126823712881692 |

The package's values sit within `10⁻⁹` of the exact ones, and always on the inside —
its minima above the true minima, its maxima and errors below the true ones. That
is the signature of a maximum taken over grid points, and the check (K9) requires
it: a recorded extreme outside the true one would be an error, not sampling.

**The display slip (K10).** §32 shows the quantized maximum as `0.77710000…`. The
value is `0.7771000125…`: by the package's own record, by exact recomputation, and by
symmetry, since `r̂(θ+π) = 1 − r̂(θ)` makes the maximum `1 − 0.2228999875… =
0.7771000125…`. Whether §32's `…` means truncation or rounding — it uses both
elsewhere — the eighth decimal is `1`. As a stated number at its stated precision
this is `FAIL`; it changes nothing, since the legality margin it illustrates is
`0.2229` wide on each side. K10 pins it as a known slip: it passes while exactly
this slip is present, and fails on any other wrong display or if this one is
corrected, so the record cannot drift.

**The package's description of itself (K11).** `VALIDATION.json` records the SHA-256,
byte count and `$$` count of the Round 02 document and its state crystal. All match
the archive: the package validated exactly this text.

## E — the theorems, read

| Round 02 | statement | verdict | note |
| --- | --- | --- | --- |
| §1–2 | the curvature measure of any unit constant-width body is `r dθ` with `0 ≤ r ≤ 1` | PASS by cited theorem | `h + h''` is a nonnegative measure for a convex body; closes the gap RUN-004 noted in Round 01 §10 |
| Thm 4.1 | a nonnegative normalized even kernel keeps a body legal | PASS by cited theorem | width by linearity, `K * r ≥ 0` then the support-function criterion, the upper bound by averaging, the gauge by the Fourier multiplier; evenness keeps reflections commuting with smoothing |
| §5–6 | Fejér and squared-Fejér kernels | PASS | K1, K2 |
| §7 | `0 ≤ h ≤ 1`, `‖h''‖∞ ≤ 1` | PASS by cited theorem | `0 ∈ K` because the Steiner point lies in the body |
| §8–9 | second-difference bound; `E_N` | PASS | K3–K6, K12 |
| §10 | `E_N = O(N⁻²)` is not Zeng's `CM⁻²` | PASS | the disclaimer is correct: one bounds shape approximation, the other the constant's hierarchy |
| §11–15 | finite-dimensional is not finite; interiorization; odd form up to frequency `2N−1`, `2(N−1)` coefficients | PASS | |
| §16–18 | quantization error in `r` and in `h` | PASS | K7 |
| §19, Thm 20.1, §21 | the finite dictionary and its parameters | PASS by cited theorem | K7, K8; inherits §7's citation. §21 omits `q ≤ ½` but it is implied: `A_N ≥ 8` and `ε < 1` give `q ≤ ε/48` |
| §23–24 | signed margin `M_U`, 1-Lipschitz in the shape | PASS | `Q` ranges over `O(2)` — reflections included |
| §25 | sandwich; Rules A and B | PASS | the left inequality needs every dictionary body to be legal, which §17 provides |
| §26–28, §36 | what closed and what did not | PASS | no over-claim |

**The reflection watch item** (from RUN-002 and RUN-004): Round 02 enumerates shapes,
not placements, so there is nothing to enumerate; its signed margin takes `Q ∈ O(2)`.
Round 03, which builds the placement certificate, lists "reflection 作兩個 discrete
branches" among its tasks — that is where the watch item is next checked.

## The status registry

Round 02's 18 judgments are reviewed and its 8 first-used phrases defined. This is the
first round carrying `PROVED`, and the classification RUN-003 set up is now used:

| Round 02 label | subject | how it is known | verdict |
| --- | --- | --- | --- |
| `PROVED` | positive-kernel legality | analytic | PASS by cited theorem |
| `PROVED` | explicit kernel error | analytic | PASS by cited theorem |
| `PROVED` | legal coefficient quantization | analytic | PASS |
| `PROVED IN MEASURE FORM` | non-smooth constant-width inclusion | analytic | PASS by cited theorem |
| `PROVED CONSTRUCTIVELY` | finite dictionary existence | analytic | PASS by cited theorem |

Every `PROVED` in Round 02 is an analytic proof; none is a computation passed off as
one. Four of the five lean on classical facts they do not cite.

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

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| Fejér coefficient `1 − k/N` | 1 | K1 |
| `S_N` with denominator `3N` | 1 | K2 + K3 |
| first integral `π³/(3N)` | 1 | K3 |
| `E_N` 0.1% too small | 1 | K3 + K6 + K9 |
| `E_N` ten times too strong | 1 | K3 + K5 + K6 + K9 + K12 |
| Jordan bound `π²/((N+1)²t²)` | 1 | K4 |
| `A_N` halved | 1 | K7 + K9 |
| §21 total `2ε/3` | 1 | K7 |
| coefficient box `1`; lattice bound `⌈2/q⌉+1` | 2 | K8 |
| recorded smoothing error `+10⁻⁶`; recorded minimum `10⁻⁹` outside the true one | 2 | K9 |
| Fejér kernel in place of `J_N` | 1 | K9 + K12 |
| a table entry edited | 1 | K6 |
| a display edited; the known slip corrected; the slip unpinned | 3 | K10 |
| `A_N`'s formula edited in the document | 1 | A0 |
| the package's recorded SHA-256; its `$$` count | 2 | K11 |
| a reference's year; a title | 2 | A1 |
| a review dropped; a definition dropped | 2 | R1 |

Controls: the unmodified inputs; `S_N` written `1 + N(2N+1)/(3(N+1))`; `E_N` written
`(π²/2)(4N+1)/((N+1)(2N²+4N+3))`; the Fejér coefficient written `(N+1−k)/(N+1)`; the
document with CRLF line endings; a recorded value moved by `10⁻¹³`.

**24 / 24 plants, 6 / 6 controls, 417 / 417 must-stay-green assertions.** From this
round on, a plant that changes nothing is flagged rather than counted — the first
version of the document-edit plant replaced a string that occurs in the document only
with line breaks inside it, and was vacuous; the drill reported it uncaught, and the
guard now names such a case for what it is.

| check blinded | cases reported blind | plants naming it |
| --- | ---: | ---: |
| A0 | 1 | 1 |
| A1 | 2 | 2 |
| K1 | 1 | 1 |
| K2 | 1 | 1 |
| K3 | 4 | 4 |
| K4 | 1 | 1 |
| K5 | 1 | 1 |
| K6 | 3 | 3 |
| K7 | 2 | 2 |
| K8 | 2 | 2 |
| K9 | 6 | 6 |
| K10 | 3 | 3 |
| K11 | 2 | 2 |
| K12 | 2 | 2 |
| R1 | 2 | 2 |

## What this round does not establish

- Anything about placements. The dictionary is a shape compiler; Round 03 is the
  placement certificate.
- The deferred computations C02-1..3 — the dictionary's actual size, the compiler on
  adversarial shapes, pruning — which Round 02 marks `COMPUTE-DEFERRED`.
- That `E_N`, or anything built on it, is sharp. It is valid; it is not tight.