# RUN-004 — Round 01: the reduction chain holds, and the reflection branch is made explicit

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-24
**Subject:** `AMRAL_Lebesgue_Finite_Closure_Round_01_Support_ConstantWidth_v0.1.md` (AMRAL-LUC-FC-R01, dated 2026-09-18), read from the archive
**Tools:** [`run004_round01_reduction_chain.py`](../code/run004_round01_reduction_chain.py), [`registry.py`](../code/registry.py) — sympy 1.14 for the symbolic checks, numpy for the one numerical reproduction
**Logs:** [`run004-round01-reduction-chain.json`](../data/gate-logs/run004-round01-reduction-chain.json); citation snapshot [`round01-citations.json`](../data/external/round01-citations.json) (arXiv and Crossref, retrieved 2026-09-24); the [status registry](../data/STATUS_REGISTRY.v1.json), now carrying Round 01's reviews

**Verdict: PASS.** Every step of Round 01's reduction chain

`A → closed convex hull → unit constant-width body W → h_W → r_W = h_W + h_W''`

and of its placement compiler holds. Of its 40 judgments: 13 hold by argument
checked line by line here (`PASS`); 14 rest on classical theorems Round 01 applies
without naming a source (`PASS by cited theorem` — this report names verified
ones); 2 grade pre-corpus material that Round 01 does not re-prove (`UNMEASURED`);
11 are open items, deferrals or role assignments (`n/a`). Nothing fails.

- **RUN-002's `OPEN` is closed at the level of definitions.** Round 01 takes the
  orientation `Q ∈ O(2)`, splits `O(2)` into its two components, and makes the
  reflection a named discrete branch `σ ∈ {+1, −1}`. What stays open is a watch
  item: every later certificate must enumerate `σ = −1` or say why it may skip it.
- Two small observations: a branch type §22 lists is provably empty, and one
  fact §10 relies on is stated without a source (re-derived here in three lines).

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

---

## What Round 01 claims

No bound, new or old — its closing status says so twice. It claims an exact
compression of the target family and an exact containment interface:

1. **Targets.** Testing all planar sets of diameter ≤ 1 is equivalent to testing
   the unit constant-width bodies (Thm 3.1, Cor 3.2, Thms 4.1–4.2); their
   translation classes correspond one-to-one to the curvature-radius densities
   `r ∈ 𝓡` — `0 ≤ r ≤ 1`, `r(θ+π) = 1 − r(θ)`, both first moments zero (Thm 12.1);
   the centred family is compact, so a worst-case target exists (§15–17) and finite
   `ε`-nets exist (§18).
2. **Containment.** For compact convex sets, `A ⊆ U ⟺ h_A ≤ h_U` (Thm 5.1); a
   motion `x ↦ Qx + t`, `Q ∈ O(2)`, acts as `h_K(Qᵀu) + t·u` (Thm 5.2); the directed
   Hausdorff slack is `max{0, max_u (h_A − h_U)}` (§6).
3. **Placement.** For fixed `Q` the best translation exists and is witnessed by at
   most three active directions (§19–21); reflections are an explicit branch (§23).
4. **The canonical statement**: `a_Leb = inf { Area(U) : 𝔎(U) = 0 }`, with `𝔎` a
   max–min–min–max over `r`, `Q`, `t`, `θ` (§24).

## A — sources

**A0.** Every formula recomputed below was pinned to Round 01's bytes before it was
checked: 16 anchors, each found as written (whitespace ignored). An edit to any of
them in the document trips A0 before anything else.

**A1 — the references exist and say what Round 01 says they say.** Round 01 lists
eight external references; all eight were found and match in title, authors, venue,
volume, issue or article number where given, and year.

| # | Round 01 cites | found |
| ---: | --- | --- |
| 1 | Baez, Bagdasaryan, Gibbs, arXiv:1502.01251, 2015 | arXiv v1 2015-02-04 |
| 2–4 | Gibbs 2018; Mishra 2026; Zeng 2026 | as in [RUN-002](./RUN-002-ROUND00-BASELINE-AND-INTERFACE.md) |
| 5 | He, Martini, Wu, *Banach J. Math. Anal.* 17, 45, 2023 | doi:10.1007/s43037-023-00266-1 |
| 6 | Hynd, *Discrete Comput. Geom.*, 2025 | doi:10.1007/s00454-025-00779-6 — vol. 76(2), online 2025 |
| 7 | Thäle, *J. Geom.* 117, article 1, 2026 | doi:10.1007/s00022-025-00783-4 — online 2025-11, volume year 2026 |
| 8 | Martinez-Maure, *Canad. Math. Bull.* 65(3), 2022 | doi:10.4153/s0008439521000473 — online 2021-07, issue year 2022 |

The year differences in 6–8 are online date against volume year, not errors.

**What the references do not do.** None of them is cited at a place where Round 01
applies a classical theorem. Those places say "由 … theorem" or "既有凸幾何結果"
and stop. Each is classical and each checks out, but Round 01 leaves the reader to
find the source. For the verdicts below, this tree names one — each verified to
exist (Crossref), none given with a theorem number this tree has not itself read:

| used in Round 01 | classical fact | a source |
| --- | --- | --- |
| Thm 4.1 | every planar set of diameter `d` lies in a complete set of diameter `d`; in the plane, complete ⟺ constant width | Martini, Montejano, Oliveros, *Bodies of Constant Width* (Birkhäuser 2019), ch. "Complete and Reduced Convex Bodies", doi:10.1007/978-3-030-03868-7_7; and Round 01's own ref. 5, which it does not cite there |
| Thm 5.1, §6 | a closed convex set is the intersection of its supporting halfplanes | Schneider, *Convex Bodies: The Brunn–Minkowski Theory* |
| Thm 12.1 | a periodic `h` with `h + h'' ≥ 0` is a support function | Schneider, as above |
| §15 | Arzelà–Ascoli / Blaschke selection; the Steiner point lies in the body | Schneider, as above |
| §21 | subdifferential of a maximum of affine maps; Carathéodory in ℝ² | standard convex analysis |
| §29 | extreme constant-width bodies have `r ∈ {0,1}` a.e. ("Kallay 型") | M. Kallay, *Israel J. Math.* 22 (1975) 203–207, doi:10.1007/BF02761589 — named in Round 01 without a citation; nothing rests on it |
| §10 | `0 ≤ r ≤ 1` a.e. for unit constant width | re-derived below; Round 01 gives no source |

## B — the recomputations

| check | Round 01 | recomputed | result |
| --- | --- | --- | --- |
| S1 | §9: `h(θ)+h(θ+π)=1` forces `a₀ = ½` and kills every even mode | the coefficient system for a general trigonometric polynomial of degree 8, solved | PASS — exactly that solution set; odd modes free |
| S2 | §9: Steiner point `s(W) = (a₁, b₁)` | `(1/π)∫h·u_θ dθ` for degree 5 | PASS |
| S3 | §8, §12: translation adds `t·u_θ`, which cancels antipodally and is killed by `D²+1` | symbolic | PASS |
| S4 | §11: `∫(h+h'')cos θ = ∫(h+h'')sin θ = 0` | degree-6 polynomial, symbolic | PASS |
| S5 | §13: `h = ½ + Σ (α_n cos nθ + β_n sin nθ)/(1−n²)` | `h + h'' − r ≡ 0` for odd `n ≤ 11` | PASS |
| S6 | §12: `w''+w = 1` gives `1 + A cos θ + B sin θ`; `π`-periodicity forces `A = B = 0` | `dsolve`, then the periodicity equations | PASS |
| S7 | §14: `h_a = ½ + a cos 3θ` ⟹ `r_a = ½ − 8a cos 3θ`; `0 ≤ r_a ≤ 1 ⟺ |a| ≤ 1/16`; at `a = 1/16`, `r = ½ − ½ cos 3θ` | from `h_a` directly | PASS — the range is exact |
| S8 | §30: an odd truncation keeps the width but can break convexity | a witness, exactly | PASS — see below |
| N1 | §12–13: `r` alone determines the body up to translation | the Reuleaux triangle rebuilt from its `r` | PASS — see below |

**S8 — the witness.** §30 claims only that truncation *may* violate convexity, so one
exact example settles it. The Reuleaux triangle of width 1 has `r = 1` on three arcs
of normal directions of length `π/3` and `r = 0` between them — a square wave with
Fourier series `½ + (2/π) Σ_{m odd} sin(3mθ)/m`. Cut after `n = 3`, the curvature
radius is `½ + (2/π) sin 3θ`, whose minimum is

`½ − 2/π ≈ −0.1366 < 0`   (exactly: because `π < 4`).

The width is kept — only odd modes survive — and convexity is lost. The drill
checks that the witness is not an accident of phase: the same triangle rotated by
`π/6` violates identically, and the disc, whose `r` is constant, does not.

**N1 — reproducing the construction.** Thm 12.1's surjectivity is a construction:
from `r`, solve `h'' + h = r` in the Steiner gauge and read off a body. It was run
on the Reuleaux triangle: from the square-wave `r` alone, through §13's inversion
(odd `m ≤ 4001`, tail below `10⁻⁹`), against the triangle's support function
computed from its geometry — three unit arcs about the vertices of an equilateral
triangle of side 1, centred at the centroid. Over 3,601 directions the two agree to
**4.0 × 10⁻¹¹**. That also confirms numerically that the Reuleaux triangle's Steiner
point is its centroid; otherwise a residual `a cos θ + b sin θ` would appear. This is
`NUMERICAL-EVIDENCE` for a theorem already proved; it is recorded because it
reproduces the one construction the theorem makes.

## C — the theorems, read

| Round 01 | statement | verdict | note |
| --- | --- | --- | --- |
| Thm 3.1 | closed convex hull keeps the diameter | PASS | the convex-combination estimate is complete |
| Cor 3.2 | universality may be tested on compact convex targets | PASS | |
| Thm 4.1 | a compact convex set of diameter ≤ 1 lies in a unit constant-width body | PASS by cited theorem | completion + complete ⟺ constant width (cited); the dilation for `0 < d < 1` re-derived — `c + d(x − c) ∈ C_d` by convexity — and the point case |
| Thm 4.2 | testing ⟺ testing `𝒲₁` | PASS | given Thm 4.1; independent of the placement group |
| Thm 5.1 | `A ⊆ U ⟺ h_A ≤ h_U` | PASS by cited theorem | halfspace representation |
| Thm 5.2 | `h_{gK}(u) = h_K(Qᵀu) + t·u`, `Q ∈ O(2)` | PASS | one line; covers both components (cf. RUN-002 B1–B2) |
| §6 | directed Hausdorff slack formula | PASS by cited theorem | via Thm 5.1 applied to `U + εB` |
| §7, §20 | the placement infimum is a minimum | PASS | `Q` ranges over a compact group; `F_Q(t) ≥ ‖t‖ − ‖a_Q‖∞` makes `t` coercive |
| §8–9, §11 | antipodal width, Fourier parity, Steiner gauge, moments | PASS | S1–S4 |
| §10 | `0 ≤ r ≤ 1` a.e. | PASS | re-derived below; Round 01 cites nothing |
| Thm 12.1 | translation classes of `𝒲₁` ↔ `𝓡` | PASS by cited theorem | all four parts re-derived; rests on the support-function criterion. A classical correspondence, new only as this programme's variable, which is how Round 01 words it |
| §13–14 | inversion; the sanity family | PASS | S5, S7 |
| §15, §17–18 | compactness; the worst case is attained; finite `ε`-nets | PASS by cited theorem | Arzelà–Ascoli / Blaschke; the net is existence only, which §18 says itself |
| Thm 16.1 | `Ψ_U` is 1-Lipschitz in the target | PASS | |
| §21 | at most three active directions | PASS by cited theorem | see observation 1 |
| §23 | reflections as an explicit branch | PASS | see below |
| §24 | canonical max–min–min–max statement | PASS | assembled from the above |
| §29 | extreme-only testing is *not* established | PASS | the caution is right: `∀K ∃g_K` does not pass through a Minkowski combination, since `g₀ ≠ g₁` is allowed |
| §30 | odd truncation can break convexity | PASS | S8 |

## Two observations

**1. §22 lists a branch type that cannot occur.** §21 shows that at a best
translation `t*` for fixed `Q`, `0 ∈ conv 𝒜_Q`, where `𝒜_Q ⊂ S¹` is the active set.
§22 then says future branch types are restricted to "one-active degeneracy;
two-active balance; three-active balance". The first is empty: a single unit vector
`u` has `conv{u} = {u} ∌ 0`, so every minimiser has at least two active directions —
an antipodal pair or a balanced triple. Harmless, since nothing is built on it; but
it makes a prediction. When the deferred active-direction census (C02) is run, a
"one-active" count at a genuine minimiser would signal a numerical artefact, not
geometry.

*Added on reading Round 03:* the corpus makes this same correction itself. Round 03
§8, "Round 01 correction ledger", records it as `R01-CORRECTION-001` — "one-active
branch impossible"; the classification is "2-active antipodal or 3-active
origin-enclosing" — and notes, as here, that the at-most-three theorem is unaffected.
This tree reached it independently, two rounds earlier in reading order.

**2. §10 states `0 ≤ r ≤ 1` without a source.** It re-derives in three lines. Unit
constant width says `h(θ) + h(θ+π) = 1`, that is `h_W + h_{−W} = 1`, so `W + (−W)`
is the unit disc. In the plane `h + h''` is the body's length measure, nonnegative
and additive under Minkowski sums; the unit disc's is `dθ`. Hence
`S_W(dθ) + S_W(dθ + π) = dθ` with `S_W ≥ 0`, which forces `S_W = r dθ` with
`0 ≤ r ≤ 1` and `r(θ) + r(θ+π) = 1` almost everywhere.

The corpus closes this itself, one round later: Round 02 §1–2 opens with "a
necessary strengthening of Round 01" and gives the same argument — `D² + 1` applied
to the width identity yields `μ_h + τ_π μ_h = dθ` for the curvature measure — so that
non-smooth bodies such as the Reuleaux triangle are covered. The gap in Round 01 is
real but was not left open.

The same kind of one-line argument settles the one pre-corpus item Round 01 grades
`PASS` without proof here, Q1 — as Round 01 uses it, `Ψ` is 1-Lipschitz in the
*cover*: `d₊(gK, U) ≤ d₊(gK, V) + d₊(V, U)`, so `|Ψ_U(K) − Ψ_V(K)| ≤ d_H(U, V)`.
The two it grades that are not re-proved anywhere in Round 01 — Q4's angular
sampling (`PASS-WITH-SCOPE`) and Q6's removable-region criterion
(`FINITE-FAMILY-PASS`) — are `UNMEASURED` here: the drafts they grade are outside
this corpus.

## The reflection branch — RUN-002's `OPEN`

RUN-002 found Round 00 writing the placement group as `E(2)` while describing and
parametrising only rotations and translations — immaterial for mirror-symmetric test
bodies, material for chiral ones. Round 01 settles the definition:

- §2 defines universality with `g ∈ E(2)`, and Thm 5.2 takes `Q ∈ O(2)`;
- §23 states that the problem uses congruent (isometric) copies, so `Q ∈ O(2)`, not
  `SO(2)`; writes `O(2) = SO(2) ∪ R_ref SO(2)`; and turns the reflection into an
  explicit discrete branch `σ ∈ {+1, −1}` beside the continuous `φ ∈ S¹`;
- its reproducibility checklist records "Reflection audit: PASS".

So the convention is now fixed and correct. What cannot be settled in Round 01 is
whether the certificates built later honour it. **Watch item, carried forward:** in
every round that enumerates placements, check that `σ = −1` is enumerated, or that
the round says why it may be skipped — for instance because the test body, or the
candidate cover, is mirror-symmetric.

## The status registry

Round 01's 40 judgments now each carry a review in the registry — how it is known
and this tree's verdict — and the 13 status phrases Round 01 is the first to use each
carry a definition record: 6 defined in line where they are used, 3 inherited from
Round 00 §2, 3 used without definition (meaning taken from context), and 1 that is not
a status at all but a lemma's name the census picked up. A check (R1) requires the
reviews to cover the census exactly — one per judgment, none extra — and every
first-used phrase to be defined.

| verdict | judgments |
| --- | ---: |
| PASS | 13 |
| PASS by cited theorem | 14 |
| UNMEASURED | 2 |
| n/a | 11 |

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| a formula edited in the document (`1/16` → `1/8`; `1−n²` → `1+n²`) | 2 | A0 |
| a reference's title, volume, article number, author or year altered; an arXiv year altered | 6 | A1 |
| odd instead of even modes claimed to vanish | 1 | S1 |
| Steiner point doubled | 1 | S2 |
| antipodal translation sign flipped | 1 | S3 |
| moment taken against `cos 2θ` | 1 | S4 |
| inversion factor `1/(1+n²)`; inversion factor `1/(n²−1)` | 2 | S5 + N1 |
| width ODE kernel replaced by `cos 2θ, sin 2θ` | 1 | S6 |
| sanity curvature sign flipped; bound claimed `1/8` | 2 | S7 |
| truncation witness replaced by the disc | 1 | S8 |
| geometry replaced by the plain triangle | 1 | N1 |
| a review dropped; duplicated; added for no judgment; a definition dropped; a verdict outside the vocabulary | 5 | R1 |

Controls — nothing may trip: the unmodified inputs; the inversion written
`−1/(n²−1)`; the sanity curvature written `(1 − 16a cos 3θ)/2`; the truncation
witness rotated by `π/6`; a reference's venue with its HTML entity unescaped; the
document with CRLF line endings.

**24 / 24 plants, 6 / 6 controls, 334 / 334 must-stay-green assertions.**

| check blinded | cases reported blind | plants naming it |
| --- | ---: | ---: |
| A0 | 2 | 2 |
| A1 | 6 | 6 |
| S1 | 1 | 1 |
| S2 | 1 | 1 |
| S3 | 1 | 1 |
| S4 | 1 | 1 |
| S5 | 2 | 2 |
| S6 | 1 | 1 |
| S7 | 2 | 2 |
| S8 | 1 | 1 |
| N1 | 3 | 3 |
| R1 | 5 | 5 |

## What this round does not establish

- The classical theorems themselves — cited, and now with sources, not re-proved.
- Anything computed: Round 01 defers C01–C03 and makes no computational claim.
- Whether later rounds enumerate the reflection branch. That is the watch item.