---
title: "Certifying a worm's critical scale over the whole rotation circle: a phase-contact map, interval enclosures, and the gaps of a semi-validated certificate"
subtitle: "Rounds 09 to 12 of a search for the hardest unit arcs in the 30-60-90 triangle, recomputed: the least of a tanh-layer curve certified in interval arithmetic, and where the programme's own certificate did not enclose"
author:
  - "Aletheia — research rounds; model: ChatGPT, GPT series"
  - "Neo.K — AMRAL Research Lab"
  - "懸衡 (Xuán Héng) — AMRAL Research Lab, recomputation; model: Claude, Opus series"
date: 2026-10-21
version: "0.1"
standard: "1"
headline_problem: "Moser's worm problem"
evidence:
  branch: agent/moser-verification-xuanheng
  commit: 02fda7c858e0b6aef1f6772b65856a364456f8b6
  dir: moser-verification-xuanheng
  sources: "data/gate-logs/run01[0-3]-*.json, data/external/round0[12]-citations.json, data/paper-figures.json"
abstract: |
  The critical scale of a curve in a container is the least, over every rotation, of the scale at which it fits; a
  scan over rotations finds candidates for that least but cannot exclude a narrow dip between its samples. This paper
  takes four rounds of a research programme on the unit arcs that need the most of Wetzel's 30-60-90 triangle, shrunk
  by 1.0048 — rounds that built, step by step, towards a certificate for one curve, a mirror-symmetric curve with a
  finite-width tanh curvature layer — and states what each established at the strength an independent recomputation
  measured. In interval arithmetic the recomputation certifies, first, that the curve's least scale over the whole
  rotation circle exceeds that of the programme's earlier best polygon, the event five-link, by more than
  1.050233666×10⁻⁵, and then that the least is reached at the rotation 3π/2 alone and lies in
  [0.998914339066915, 0.998914339102351], with the competing cusp at 2π/3 at least 1.630111×10⁻⁹ above it. It also
  fixes, at 40 digits, a smooth minimum 5.44×10⁻⁹ rad beside a contact switch that every sampled guard of the
  programme missed, and shows that the programme's "semi-validated" certificate leaves the 2×10⁻¹⁰ rad beside each
  switch enclosed by no derivative interval, so that three of its exclusions rest on intervals that do not contain
  the derivative they bound. The paper proves no bound for Moser's worm problem.
keywords: [Moser's worm problem, Wetzel's triangle, interval arithmetic, validated numerics, support function]
---

> **Status of this document.** Preprint, version 0.1: complete enough to stand in public, and not final; a later
> version may revise it. Not prepared for journal submission. References are added before formal upload. Section 13
> records who did which part.

## 0. What is claimed, and what is not

Every statement in this paper carries a status, given after it in italics. A statement with a proof carries a
verdict on that proof. `PASS` and `PASS by cited theorem` are different verdicts and are never written as one: the
first is a proof checked line by line — against the programme's text, or, for the arguments this paper supplies
itself, as written here — and the second a proof one of whose steps holds because a published theorem does, cited
with its statement checked against its source. Every other statement carries one of six labels, and the labels are
never merged:

| label | meaning |
| --- | --- |
| `COMPUTED_HERE` | a figure recomputed by the recomputation arm with independently written code — *certified* where the text says so, in mpmath's interval arithmetic with outward rounding; *high precision*, *numerical* or *sampled* otherwise |
| `DERIVED_FROM_VERIFIED_INPUTS` | follows from statements already verified here, with no step of its own beyond combining them |
| `CITED_THEOREM` | someone else's published theorem, stated here and not re-proved; its statement checked against its source |
| `INHERITED` | taken from the research programme's documents and not verified here; every use is marked |
| `UNMEASURED` | well posed, and not established here |
| `FAILED` | attempted and refused: false as stated, or true only in the corrected form given |

A *certified* figure is a bound computed in interval arithmetic, with every figure of the bound cut toward its safe
side; floating-point arithmetic only chooses the intervals and the points the bound is taken at. A *high-precision*
figure agrees to many digits between independent methods and is not a bound; a *sampled* one holds wherever it was
looked at, which is evidence and not a proof. The certificates rest on mpmath's interval arithmetic being correct as
implemented; nothing here re-verifies the library.

**Not claimed anywhere in this paper:** any bound for Moser's worm problem — the least area of a convex set
containing a congruent copy of every unit arc is open; that the triangle $T/1.0048$ covers every unit arc, which is a
cited preprint not checked here; anything about the two curves as the programme stored them in double precision,
rather than as its ninth round defines them by decimal constants (the tanh-layer curve's constants differ from their
doubles by at most $1.01\times10^{-16}$, and the transfer was not carried out); that the tanh-layer curve is the best
of its family, or a local maximum among curves; anything about the event five-link's least over all rotations beyond
an upper bound — and so any upper bound for the gain over it; the number of stationary points on the curve's wing
intervals as an interval enclosure — it rests on a refined scan; that the programme's own boxes and root boxes, in its
eleventh and twelfth rounds, are valid enclosures.

## 1. Introduction

### 1.1 The problem, and why a scan is not enough

Moser asked for the convex set of least area that contains a congruent copy of every curve of length one — every
*unit arc*; the question is open. It dates from 1966, by the account of Panraksa and Wichiramala [5] (we have not seen a primary source for the date); Norwood, Poole and Laidacker [4] give an early treatment of the problem. One explicit cover is Wetzel's 30-60-90 triangle, which he conjectured covers every unit arc, as the preprint
below reports; for his 30° sector of radius 1 the conjecture was proved for drapeable arcs by Movshovich and Wetzel [6] and in full by Panraksa and Wichiramala [5]. Wichiramala and Panraksa (preprint, arXiv:2606.14625) prove by a computer-assisted argument that the
triangle covers every unit arc, and with margin, so
that the triangle shrunk by 1.0048 does too, by congruent copies, reflections allowed. *`CITED_THEOREM` (a preprint;
checked by RUN-002 and RUN-003 of the same recomputation for its statement and convention, not for its proof).* A
research programme then searched for the unit arcs that need the most of that shrunk triangle — whose *critical
scale*, the least over rotations $\varphi$ of the scale $s(\varphi)$ at which the rotated arc fits, comes closest to
1.

The critical scale is a minimum over a circle of a function that is continuous and piecewise smooth: it has a kink
where one corner of the arc hands a functional of the triangle to another, and a derivative that turns steeply where
the support passes from a curved stretch of the arc to its end. A scan of rotations finds the low branches; it cannot
exclude a dip narrower than its spacing, and the minima that matter here sit at kinks, beside which a minimizer that
assumes smoothness stops short. To *know* the least, it must be bounded from below at every rotation. This paper is
about doing that for one curve.

### 1.2 What this paper supplies

The programme's rounds 09 to 12 take one curve — its eighth round's best, fixed by decimal constants — and build
towards a certificate of its least: high-precision values and a monotone bound at one rotation (round 09), a map of
the whole rotation circle into intervals of fixed contact (round 10), a "semi-validated" box certificate (round 11),
and an interval-arithmetic replay of parts of it (round 12). This paper states what each established, at the strength
an independent recomputation measured, and adds the certificates the rounds did not reach:

- §2 specifies the curve, the polygon it is compared with, and the scale;
- §3 checks the value at $3\pi/2$ to 120 digits and certifies the round's one-rotation bound;
- §4 certifies, over the whole circle, that the curve's least exceeds the polygon's;
- §5 checks the phase-contact map, and fixes a smooth minimum the round's sampled guards miss;
- §6 certifies that the least is reached at $3\pi/2$ alone, and encloses it;
- §7 and §8 measure the programme's own certificate and its replay against these;
- §9 says what the case teaches about enclosures at a switch; §10 and §11 list every result and every correction.

### 1.3 Where the mathematics comes from, and how it was checked

The rounds are rounds 09 to 12 of the programme's fifteen; its packages are public, byte for byte, on the AMRAL site
(§12). Every statement below was checked by an independent recomputation (懸衡): every figure rebuilt with
independently written code, never by running the programme's scripts — RUN-010 read the round's verifier only after
its own rebuild, to compare; RUN-012 and RUN-013 read the shipped scripts without running them, and RUN-013, to replay
the round's interval method, rewrote that method from its stated parameters — every argument read, and every check
drilled with planted faults. The checks are the runs RUN-010 to RUN-013 of the recomputation tree pinned in the front
matter, one per round.

## 2. The curves and the scale

### 2.1 The triangle and the scale

$T_0 = \{(x, y) : x \ge 0,\ y \ge 0,\ x/A + y/B \le 1\}$ with $A = (3 + 4\sqrt3)/(18\cdot1.0048)$ and
$B = (4 + \sqrt3)/(6\cdot1.0048)$: Wetzel's triangle shrunk by 1.0048, with its right angle at the origin and its
short leg on the $x$-axis; $B/A = \sqrt3$, so $A/B = \tan(\pi/6)$. A curve rotated counterclockwise by $\varphi$ fits
in $sT_0$ after the best translation exactly when $s \ge s(\varphi)$, where
$$s(\varphi) = \max_{p\in\gamma_\varphi}\Big(\frac{x}{A} + \frac{y}{B}\Big) - \min_{p\in\gamma_\varphi}\frac{x}{A} - \min_{p\in\gamma_\varphi}\frac{y}{B}
= \sum_{k=1}^{3}\max_{p\in\gamma}\, n_k(\varphi)\cdot p,$$
the three functionals being $a_1 = (1/A, 1/B)$, $a_2 = (-1/A, 0)$, $a_3 = (0, -1/B)$ turned back by $\varphi$; they sum
to zero, so $s$ does not change under translation. *`PASS` (the programme's exact formula, checked for polylines in
RUN-003; for a curve the same argument holds with its points in place of the vertices).* The critical scale is
$\min_\varphi s(\varphi)$. The cover allows reflections; the minimum over rotations alone suffices here because both
curves of this paper are their own mirror images.

### 2.2 The tanh-layer curve

The programme's ninth round fixes its eighth round's best candidate "由明確十進位常數定義" (by explicit decimal
constants):
$$\varepsilon = 0.037,\quad w = 0.3361057714712081,\quad \beta = 1.405382794839393,\quad \delta = 0.05204734906280986,\quad c = 0.5801781668857768.$$
The curve has length 1 and three parts. Its **left wing** runs from $p_0 = (0, 0)$, with position
$w\int_0^u(\cos\theta(t), \sin\theta(t))\,dt$ for $0 \le u \le 1$ and tangent angle
$$\theta(u) = \beta + \delta\,\frac{\tanh((c - u)/\varepsilon) - T_1}{T_0 - T_1},\qquad T_0 = \tanh(c/\varepsilon),\ T_1 = \tanh((c - 1)/\varepsilon),$$
which falls monotonically from $\alpha = \beta + \delta$ at $u = 0$ to $\beta$ at $u = 1$, the turn concentrated in a
layer of width about $\varepsilon$ around $u = c$; it ends at $p_1 = (x_1, y_1)$. A horizontal **centre segment** of
length $l_0 = 1 - 2w$ runs from $p_1$ to $p_2 = (x_1 + l_0, y_1)$, and the **right wing** is the left wing's mirror
image in the vertical line through the segment's midpoint, ending at $p_3 = (2x_1 + l_0, 0)$. *`COMPUTED_HERE`: the
constants are the eighth round's best parameters as shortest decimals, and this form of the layer is the eighth
round's (RUN-010).*

On this curve every linear functional takes its maximum at one of the four corners $p_0, \dots, p_3$ or at the one
interior point of a wing whose tangent is perpendicular to it, found by inverting the tanh, since $\theta$ is monotone
over an angle $\delta < \pi$. The recomputation evaluates $s(\varphi)$ that way, with the wing positions by quadrature
at 40 to 200 digits. *`COMPUTED_HERE`, RUN-010, RUN-011.*

### 2.3 The event five-link

The curve is compared with the programme's earlier best polygon, the **event five-link** of its fifth round — numerically
a strict local maximum of the least scale among nearby unit five-links, on a neighbourhood of unestablished size (a
companion paper). The ninth round fixes it too as decimal constants, its fifth round's double-precision root written
as shortest decimals:
$$l_1 = 0.19431311615307248,\quad l_2 = 0.1415930791195921,\quad \beta_e = 1.4082767308631334,\quad \delta_e = 0.04759059497406796.$$
From the origin its five links have lengths and directions $(l_1, \alpha_e)$, $(l_2, \beta_e)$, $(1 - 2(l_1 + l_2), 0)$,
$(l_2, -\beta_e)$, $(l_1, -\alpha_e)$, with $\alpha_e = \beta_e + \delta_e$. Its four branches are its scales at the
four event phases $\pi/2 - \alpha_e$, $\pi/2 - \beta_e$, $2\pi/3$ and $3\pi/2$, where its contact with the triangle
changes. Write $s_0$ for the least of these four values. That $s_0$ is the five-link's least scale over all rotations
is a numerical result of the companion paper's evidence, not of this one; this paper uses only that the five-link's
least is at most $s_0$, which needs nothing more than the four values. *`COMPUTED_HERE` (the constants are the fifth
round's root, RUN-010); `INHERITED` as to the five-link's standing.*

## 3. The value at 3π/2

### 3.1 Two integrals

**Proposition 3.1 (support identity at 3π/2).** *Since $\beta > \pi/6$ and $\alpha < \pi/2$, at $\varphi = 3\pi/2$ the
two ends tie on the leg $x = 0$ and the wing's end $p_1$ carries the hypotenuse, so*
$$s(3\pi/2) = \frac{y_1}{A} + \frac{x_1 + l_0}{B}.$$
With $\theta$ in $(\pi/6, \pi/2)$ the curve rises along its left wing and runs right throughout, and the functional
the hypotenuse sets after the turn by $3\pi/2$ peaks at the wing's end, because $\tan\theta > A/B = \tan(\pi/6)$ along
the rise. *Status:* `PASS` (the round's reduction; the argument read in RUN-010, its premise checked in interval
arithmetic in RUN-011). So the value the round needs takes only two one-dimensional integrals, as it says
("關鍵候選值只需兩個一維積分").

### 3.2 To 120 digits

The recomputation evaluates the two wing integrals with mpmath's tanh–sinh and Gauss–Legendre quadratures, split at the
layer's centre and at 2, 6 and 12 widths either side where these fall inside the wing, at 200 digits; the two agree to
every digit, and
$$s_{270} = s(3\pi/2) = 0.998914339084632717252964418536702246180192119314833519984798\ldots$$
holds the round's 120 digits. The event five-link's four branches, from its six vertices at 200 digits, hold the
round's values, and
$$s_{270} - s_0 = 1.0581952124042297834593636\times10^{-5};$$
the round prints this difference to 124 decimals, of which 121 agree — the last beyond what a difference of two
values exact to 120 decimals guarantees. *`COMPUTED_HERE` (high precision: two quadratures agreeing to every digit; the event's branches from its
vertices), RUN-010.* The round's convergence rows hold to their working precision; three groups of its printed figures
do not hold to their digits (§11).

### 3.3 The monotone bound

The round's sixth section notes that $\theta$ decreases inside $(0, \pi/2)$, so $\sin\theta$ decreases and $\cos\theta$
increases, and left and right sums bound the two integrals.

**Proposition 3.2 (Darboux bound).** *For every partition of $[0, 1]$, the sums taking the right value of $\sin\theta$
and the left value of $\cos\theta$ on each part bound $y_1$ and $x_1$ from below, and the other two from above; since
both enter $s(3\pi/2)$ with positive coefficients, the sums bound $s(3\pi/2)$.* *Status:* `PASS` (RUN-010).

Redone in interval arithmetic at 4,096 parts, the lower bound is 0.9989115747096505504998971, and it exceeds the event
five-link's interval upper bound by more than $7.8\times10^{-6}$: the round's statement that $s(3\pi/2)$ exceeds $s_0$
by more than $7.8\times10^{-6}$ is certified. *`COMPUTED_HERE` (certified, given Proposition 3.1), RUN-010.* It
concerns one rotation, as the round says: "Darboux 包絡只證明精確 $270^\circ$ 尖點值高於事件控制，不直接證明它是完整相位圓的全域最低值"
(the Darboux envelope proves only that the exact 270° cusp value is above the event control, not that it is the
global minimum over the full phase circle).

## 4. Over the whole circle, against the event five-link

The round's interval-certificate draft states what its comparison with the event five-link needs: $s(\varphi) \ge
s_{270} - \eta$ for every $\varphi$, with $\eta < s_{270} - s_0$ — a margin of about $1.06\times10^{-5}$. The round's
own §11 frames its open step differently, as resolving the "$10^{-9}$ 級差距" (the $10^{-9}$-level gap) between the
cusps at $120°$ and $270°$ — a correct description of what showing the least to be at $270°$ would take, and a far
narrower target than the comparison needs.

**Theorem 4.1 (certified).** *For the ninth round's decimal curves — the tanh-layer curve and the event five-link alike,*
$$\min_\varphi s(\varphi) \ \ge\ 0.99891425946916933623\ >\ 0.998903757132508674955129824903\ \ge\ \text{the event five-link's least scale},$$
*a margin of more than $1.050233666\times10^{-5}$, 99 % of the high-precision gain $s_{270} - s_0$.*

*Proof.* For any points $q_1, q_2, q_3$ of the curve, $s(\varphi) = \sum_k\max_p n_k(\varphi)\cdot p \ge
\sum_k n_k(\varphi)\cdot q_k$, so points of the curve bound $s$ from below; and $n_k(\varphi)\cdot q$ changes with
$\varphi$ no faster than $|a_k||q|$. The curve's points at $u = j/65{,}536$ on both wings are enclosed in boxes: each
step's integral of $\cos\theta$ and of $\sin\theta$ is its trapezoid value within $h^3M_2/12$, with
$M_2 = 15.12802457$ bounding the second derivative of both ($|f''| \le \theta'^2 + |\theta''|$, from bounds on the
tanh's derivatives); the widest box is $5.919\times10^{-10}$ by $1.973\times10^{-10}$. With the curve centred — its
radius at most 0.26734185 — the functionals' phase derivatives are at most $\mathrm{Lip} = 1.33056835$, both bounds
taken in interval arithmetic. A floating-point search bisects the phase circle until on each interval an estimate at
its midpoint clears the target; on each of the 42,838 intervals, which cover the circle, the bound — three chosen
points' boxes at the midpoint, less Lip times the half-width — is then taken in interval arithmetic at 30 digits. The
event five-link's least is bounded from above by the least of its scales at its four branch phases, taken from its
vertices in interval arithmetic at enclosures of those phases. *The argument `PASS`; the bounds `COMPUTED_HERE`
(certified), RUN-010.*

As a control, a target above the curve's own certified value at $3\pi/2$, asked on a neighbourhood of $3\pi/2$, is
refused there. *`COMPUTED_HERE`, RUN-010.* The theorem bounds the curve's least from below, within $8.0\times10^{-8}$
of $s_{270}$; where the least is reached it does not say. That is §6.

## 5. The phase-contact map

### 5.1 The map

The programme's tenth round sets out to "將整個相位圓拆成固定活動支撐身份區間，枚舉全部局部極小並檢查 $270^\circ$ 是否仍為全域最低"
(split the whole phase circle into intervals of fixed active support identity, enumerate every local minimum, and check
whether 270° is still the global minimum). It records, for each rotation, the signature — which corner or which wing's
interior carries each of the three functionals — and finds 18 intervals, 12 smooth stationary points and four cusp
minima, the least at $3\pi/2$ and the cusp at $2\pi/3$ $1.6383\times10^{-9}$ above it. Between the intervals its table
lists 17 switches; an eighteenth, at $\varphi = 0$, where the two ends tie in $y$, is a kink but not a minimum, and the
round's README counts it while the table does not. The recomputation evaluates the exact support at 60 digits: at every
interval's midpoint the active supports are the stated signature; each of the 17 switches, located by bisection on the
active labels, lies within $5.22\times10^{-14}$ of its stated phase, its scale within $1.04\times10^{-13}$; and the 12
stated stationary points are exact ones of their kinds. *`COMPUTED_HERE` (high precision), RUN-011.* Its own scans at
32,768 to 262,144 rotations give the same counts — of switches, signatures and sampled minima, and the place of the
least — every time. *`COMPUTED_HERE` (double precision), RUN-011.*

### 5.2 What the derivative does at a switch

**Proposition 5.1.** *(i) At a switch where a wing's interior support point reaches or leaves the wing's end, and the
other two functionals' supports are single corners, $s$ is continuously differentiable. (ii) On an interval whose three
supports are all corners, $s$ is a sum of sinusoids of one frequency with $s'' = -s < 0$, so it has at most one
stationary point there, a maximum, which the signs of the derivative at its ends decide.*

For (i): at such a switch the support point is the corner itself, the functional's maximum moves with it continuously
in derivative, and the other two terms are smooth. For (ii): a fixed linear combination of the corners' coordinates,
rotated by $\varphi$, is $R\cos(\varphi - \varphi_0)$, and $s > 0$. *Status:* `PASS`; the hypothesis of (i) holds at all
twelve wing switches of this curve, and there this run's one-sided derivatives agree to $4.6\times10^{-9}$ (RUN-011).

The round states two different one-sided derivatives at each of the twelve wing switches, apart by 0.047 to 0.21. One
of each pair is the derivative, to $1.13\times10^{-8}$; the other is the derivative at a point inside the interval. The
derivative is steep there: the tanh layer leaves each wing nearly straight — within $1.38\times10^{-8}$ rad of $\alpha$
up to $u = 0.3$ and within $2.41\times10^{-8}$ of $\beta$ from $u = 0.85$ on — so the interior support races along the
straight stretch as the rotation turns. *`COMPUTED_HERE` (high precision); the stated pairs `FAILED`, RUN-011.*

### 5.3 A smooth minimum the guards miss

The round lists its switch 9, at 3.028226470697 rad — the switch at $\pi/2 + \alpha$ — as a cusp minimum with one-sided
derivatives $-0.006893$ and $+0.173166$. The derivative is $+0.173166$ on both sides, so the switch is not a minimum.
The derivative on interval 9 runs from $-0.3817$ at its start to $+0.1732$ at its end and crosses zero
$5.44\times10^{-9}$ rad before the switch, at
$$\varphi^* = 3.028226465255688362712441\ldots,\qquad s(\varphi^*) = 1.0998102257068941255\ldots,$$
$6.16\times10^{-11}$ below the stated cusp value. *`COMPUTED_HERE` (high precision, 40 digits), RUN-011; the minimum
had already been located by RUN-009's double-precision scan of the eighth round, with golden refinement.* The round's
sampling reaches neither: interval 9 is classified strictly decreasing, its guards find no root on 257, 1,025 or 4,097
samples — the largest derivative they see is $-0.006893$ — the stationary list has 12 points where there are 13, and
the ranking and the ledger give interval 9 the switch's value. So there are three cusp minima and five smooth ones, and
13 stationary points in all. *The count `COMPUTED_HERE`: exact on the twelve corner-only intervals by Proposition
5.1(ii), with the derivative's end signs at 60 digits; on the six wing intervals, by a refined scan of the exact
derivative — the 65 points $k/64$ and 15 points toward each end, 95 in all — then bisection, not an interval
enclosure; the round's list and classification `FAILED`, RUN-011.* The missed minimum is the hidden root the round's
own limitation names ("導數無隱藏根依賴多網格穩定性，而非嚴格界", that the derivative has no hidden root rests on
stability across grids, not on a rigorous bound), sitting in the steep stretch of §5.2. It lies 0.101 above the least
and changes nothing about the global minimum.

## 6. The least at 3π/2, certified

The round's certificate interface sets the final target, $s(\varphi) \ge s(3\pi/2)$ for every $\varphi$, and says
"本輪尚未聲稱完成此嚴格證書" (this round does not yet claim this rigorous certificate).

**Theorem 6.1 (certified).** *For the ninth round's decimal curve, the least scale over all rotations is $s(3\pi/2)$,
reached at $3\pi/2$ alone, and*
$$0.998914339066915 \le s(3\pi/2) \le 0.998914339102351;$$
*the cusp at $2\pi/3$ is at least $1.630111\times10^{-9}$ above it, and the least exceeds the event five-link's by at
least $1.0581934\times10^{-5}$.*

*Proof.* Three parts, in mpmath's interval arithmetic at 30 digits.

- **At $3\pi/2$.** Proposition 3.1's premise, $\beta > \pi/6$ and $\alpha < \pi/2$, holds in interval arithmetic, so
  $s(3\pi/2) = y_1/A + (x_1 + l_0)/B$; trapezoid boxes on 262,144 steps a wing, at most $3.70\times10^{-11}$ wide in $x$
  and $1.23\times10^{-11}$ in $y$, put it in the interval stated.
- **Beside $3\pi/2$ and $2\pi/3$.** On each side of each cusp, over a range of 0.05 rad from the far end of the cusp's
  interval enclosure, $s(\varphi) \ge g(\varphi)$, $g$ being the three functionals on the corners active on that side;
  and $g'$ has one sign there — negative before the cusp, positive after — on each of 64 sub-intervals. So beside
  $3\pi/2$, $s(\varphi) \ge g(\varphi) \ge g(3\pi/2) = s(3\pi/2)$, strictly away from it; and beside $2\pi/3$,
  $s(\varphi) \ge g(2\pi/3)$, and $g(2\pi/3) - s(3\pi/2)$, written as a linear form in $x_1$ and $y_1$ so that each box
  enters once, is at least $1.630111\times10^{-9}$ on either side.
- **Elsewhere.** On a phase interval of half-width $h$ about $m$, with points $q_k$ chosen at $m$,
  $G(\varphi) = \sum_k n_k(\varphi)\cdot q_k \le s(\varphi)$ and
  $G(\varphi) \ge G(m) - |G'(m)|h - \mathrm{Lip}\,h^2/2$, since $|G''| = |G| \le \sum_k|a_k||q_k| \le \mathrm{Lip}$; a
  floating-point search chooses 1,558 intervals covering the rest of the circle, and on each the bound, taken in
  interval arithmetic, exceeds the upper end of $s(3\pi/2)$ — by at least $1.855678\times10^{-9}$, the tightest beside
  the low branch near 0.124 rad.

With the event five-link's least at most 0.998903757132508674955129824903 (Theorem 4.1), the gain follows. *The
argument `PASS`; the bounds `COMPUTED_HERE` (certified), RUN-011; the gain a lower bound only — an upper bound would
need the event five-link's least bounded from below, not done.*

The round's own conclusion — that no phase branch lies below 270° — therefore holds, as a theorem for this curve. The
round declined to state it so: "不能把這句話替換成嚴格定理，因為導數符號仍以高密度浮點取樣與數值求根確認，而非區間算術包絡"
(this sentence cannot be replaced by a rigorous theorem, since the derivative signs are still confirmed by dense
floating-point sampling and numerical root finding, not interval envelopes). It was right not to; the certificate
needed a different route.

## 7. The semi-validated certificate

The programme's eleventh round writes the 17 switches as exact angles — $\pi/2 - \alpha$, $\pi/2 - \beta$,
$\beta - \pi/3$, $\alpha - \pi/3$, $\pi/2$, $\pi - \alpha$, $\pi - \beta$, $2\pi/3$, $\pi/2 + \beta$, $\pi/2 + \alpha$,
$\pi$, $5\pi/3 - \alpha$, $5\pi/3 - \beta$, $\pi + \beta$, $\pi + \alpha$, $3\pi/2$, $5\pi/3$ — encloses $s_{270}$ and
$s_{120} - s_{270}$ by a composite midpoint rule with a global second-derivative bound and a floating-point padding,
covers the intervals' interiors with 579 derivative boxes and 12 stationary-point root boxes, and treats each switch's
neighbourhood — of radius $2\times10^{-6}$, or $2\times10^{-8}$ where both supports are corners — by one-sided
derivative intervals or a lower bound of the scale. It calls the result "一份具解析誤差界、浮點外擴與逐區盒化排除的半驗證計算證書"
(a semi-validated computational certificate with analytic error bounds, float padding and interval-by-interval box
exclusion), since "NumPy 的基本運算不是全程 directed-rounding" (NumPy's basic operations are not directed-rounding
throughout).

### 7.1 What holds

The 17 switch formulas are exact: each, evaluated at 60 digits, satisfies its switch's own condition to
$6.0\times10^{-60}$ (the round's boundary list also holds 0 and $2\pi$). The $s_{270}$ and $s_{120} - s_{270}$
intervals contain the exact values, $s_{270}$ $8.88\times10^{-12}$ inside each end, and their error bounds are the
composite-midpoint bound with the round's constants — the float padding itself not verified as a rounding bound, as
the round says; the round's interval for $s_{270}$ lies inside the one Theorem 6.1 certifies, and its lower bound for
the difference exceeds that theorem's. Each of the 579 derivative boxes contains the derivative at thirteen points of
it, with the stated sign, and with the root boxes and the guards they tile every interval; each root box holds one
stationary point of its kind. *`COMPUTED_HERE` (high precision for the formulas and the exact values; the boxes
sampled at points of each box, not re-verified in interval arithmetic), RUN-012.*

### 7.2 The 2×10⁻¹⁰ rad beside each switch

Each neighbourhood's one-sided derivative interval covers $[\varphi \pm 2\times10^{-10}, \varphi \pm r]$, not
$[\varphi, \varphi \pm r]$: its end nearest the switch is the derivative $2\times10^{-10}$ rad from the switch, widened
by the round's padding. The derivative boxes' guards are $2\times10^{-10}$ on the corner intervals and $2\times10^{-8}$
on the wing intervals, so the $2\times10^{-10}$ rad beside every switch is enclosed by no derivative interval of the
certificate (its scale intervals do cover it). Whether the omission shows depends on how much the derivative moves
there:

- **At the twelve wing switches**, on the side next to the wing's interior, the derivative is steep (§5.2) and moves
  by 0.022 to 0.157 within the $2\times10^{-10}$ rad, far beyond the padding of about $2.2\times10^{-6}$ to
  $3.0\times10^{-6}$; at $\pi/2 - \alpha$ the interval's lower end is $-0.193496$ less the padding, while at the switch
  the derivative is $-0.329242$.
- **On a side whose supports are all corners**, the derivative moves by about $|s''|\cdot2\times10^{-10}$; a padding of
  $8\times10^{-10}$ or more hides it at $2\pi/3$, $3\pi/2$, $5\pi/3$ and on the corner sides of all wing switches but
  one, and at $\pi/2$, $\pi$ and the corner side of $5\pi/3 - \alpha$ the intervals miss by $1.9\times10^{-10}$ to
  $2.1\times10^{-10}$.

So at 14 of the 17 switches the derivative at the switch lies outside the interval that is to bound it. *`COMPUTED_HERE`
(high precision: the derivative at the switch and $2\times10^{-10}$ rad from it, at 60 digits); the intervals as
enclosures `FAILED`, RUN-012.* The signs the round reads from them are the derivative's on every side, and where the
scale bound also excludes, nothing rests on them. At $\pi/2 - \alpha$, $\pi/2 - \beta$ and $\beta - \pi/3$ it does not:
the round's own table puts the neighbourhoods' scale bounds $2.69\times10^{-2}$, $2.30\times10^{-2}$ and
$7.7\times10^{-4}$ below $s_{270}$, and the round excludes them through the switch on the strength of intervals that
leave out the very stretch where the derivative is steep. The conclusion is true there — Theorem 6.1 covers it by
another route — but the round's certificate does not show it. *`COMPUTED_HERE`; those three exclusions `FAILED` as
certified, RUN-012.*

### 7.3 Thirteen, not twelve

The 12 root boxes are 12 of the 13 stationary points of §5.3; the thirteenth, the smooth minimum
$5.44\times10^{-9}$ rad before $\pi/2 + \alpha$, lies inside that switch's neighbourhood, which the round leaves
unresolved (its left derivative interval straddles zero because the root is there) and excludes by its scale, which
its table puts $7.39\times10^{-2}$ above $s_{270}$. The exclusion holds; the count of 12 smooth stationary points, as
the full count, does not. *`COMPUTED_HERE`; the count `FAILED`, RUN-012.*

## 8. The interval replay

The programme's twelfth round finds no Arb or Sage in its environment and uses mpmath's `iv` as a fallback. It encloses
$s_{270}$ in $[0.99891433894289\ldots, 0.99891433922637\ldots]$, $s_{120} - s_{270}$ in
$[1.5846\times10^{-9}, 1.6920\times10^{-9}]$ — "下界仍嚴格為正" (the lower bound is still strictly positive) — and the
margin over the event five-link's first branch in $[1.0581810\times10^{-5}, 1.0582094\times10^{-5}]$.

- **The special intervals.** They contain the exact values, $s_{270}$ $1.4174\times10^{-10}$ and the difference
  $5.3711\times10^{-11}$ inside each end. The recomputation's own replay of the round's method — midpoint sums of
  $\sin\theta$, $\cos\theta$ and the difference's integrand over 65,536 parts in interval arithmetic at 75 digits, plus
  the analytic midpoint error, written anew — reproduces the round's printed ends to $3\times10^{-81}$.
  *`COMPUTED_HERE` (certified: this run's replay; the code that wrote the round's own ends is not shipped, §11.2),
  RUN-013.* The margin interval is the $s_{270}$ interval less the event five-link's branch interval, whose
  containment of the branch value was checked at high precision, not replayed. *`COMPUTED_HERE` (numerical as to the
  event interval), RUN-013.*
- **The boundary balls.** Each ball holds its formula's exact angle. The round's third section says they
  "全部包含第 11 輪保存的浮點值" (all contain round 11's saved floats), and its audit note gives "19/19"; the data say
  one does — the ball at 0 — since each ball is about $10^{-70}$ wide and the saved phases are doubles up to
  $3.8\times10^{-16}$ from the exact angles. *`COMPUTED_HERE`; the statement `FAILED`, RUN-013.*
- **The root boxes.** Each of the 12 holds one stationary point of its kind and its interval Newton image lies inside
  it; but the replay takes each wing position as the interval between two quadratures widened by their difference and
  $10^{-55}$ — an estimate of the error, not a bound — and other inputs in point arithmetic, so the replay is
  high-precision evidence, not the directed interval arithmetic it names; and the thirteenth stationary point lies in
  none of the boxes, so "所有光滑駐點，均被另一套區間運算重現" (all smooth stationary points are reproduced by another
  interval arithmetic) holds for 12 of 13. *`COMPUTED_HERE` (high precision); the statements `FAILED`, RUN-013.*
- **"Dependency inflation."** Of the twelve switches the round could not resolve directly, it says "這是 **dependency
  inflation**，不是發現反例" (this is dependency inflation, not a counterexample found). At eleven, the derivative does
  keep, on each side, the sign the eleventh round states. At the twelfth, $\pi/2 + \alpha$, the eleventh round states
  no sign — it leaves the switch unresolved and excludes it by scale — and the derivative changes sign on the left, at
  the thirteenth stationary point. That inflation of the inverse tanh's interval extension may be why the round's own
  intervals came out wide is plausible; the recomputation did not compute those intervals. But inflation is not the
  whole reason the eleventh round's narrow intervals could not be reproduced: by §7.2 they leave out values the
  derivative takes, so even an exact enclosure of each side would be wider. *`COMPUTED_HERE` (high precision, 60
  digits); the explanation `FAILED` as complete, RUN-013.*

The conclusions the round's figures support — $s_{120}$ above $s_{270}$, the curve above the event five-link, the least
at $3\pi/2$ — hold, by Theorems 4.1 and 6.1.

## 9. What the case teaches about enclosures

Two lessons generalize beyond this curve.

**An enclosure at a switch must include the switch.** A one-sided derivative interval built from samples a short
distance from a switch encloses the derivative only if the derivative cannot move further in that distance than the
padding allows. Near a wing switch of this curve it moves by up to 0.157 in $2\times10^{-10}$ rad, because the
curvature layer leaves the wing almost straight and the support point races along it. A certificate that wants the
sign through a switch must enclose the derivative on the closed side, the switch included, or bound its change there
analytically.

**A sampled guard cannot exclude a root beside a contact switch.** The minimum missed in round 10 sits
$5.44\times10^{-9}$ rad from a switch, in the same steep stretch; a guard of 4,097 samples on an interval $\delta \approx
0.052$ rad wide cannot see it, and no number of samples can prove it absent. What the tenth round's limitation said —
that the absence of hidden roots rests on stability across grids, not on a bound — was exactly right; the certificate
of §6 does not need the count, because it bounds $s$ itself, not the roots of $s'$.

## 10. Every result, and the strength at which it holds

| result | strength | run |
| --- | --- | --- |
| $T/1.0048$ covers every unit arc, by congruent copies | `CITED_THEOREM` (a preprint; its proof not checked) | RUN-002, RUN-003 |
| the decimal curves are the eighth round's best and the fifth round's root, as shortest decimals | `COMPUTED_HERE` | RUN-010 |
| Proposition 3.1: the support identity at $3\pi/2$ | `PASS`; its premise `COMPUTED_HERE`, certified | RUN-010, RUN-011 |
| $s_{270}$ to 120 digits; $s_{270} - s_0$ | `COMPUTED_HERE`, high precision | RUN-010 |
| Proposition 3.2 and the bound $s(3\pi/2) - s_0 > 7.8\times10^{-6}$ | `PASS`; `COMPUTED_HERE`, certified | RUN-010 |
| Theorem 4.1: the least above the event five-link's by more than $1.050233666\times10^{-5}$ | `COMPUTED_HERE`, certified | RUN-010 |
| the phase-contact map and the 12 stated stationary points | `COMPUTED_HERE`, high precision | RUN-011 |
| Proposition 5.1: continuity at wing switches; one stationary point on corner intervals | `PASS` | RUN-011 |
| the smooth minimum at $\varphi^*$, and 13 stationary points | `COMPUTED_HERE`; exact in number on corner intervals, a refined scan on wing intervals | RUN-011 |
| Theorem 6.1: the least at $3\pi/2$ alone, its interval, the $2\pi/3$ margin, the gain's lower bound | `COMPUTED_HERE`, certified | RUN-011 |
| the eleventh round's switch formulas and special enclosures | `COMPUTED_HERE`, high precision | RUN-012 |
| the eleventh round's 579 boxes and 12 root boxes | `COMPUTED_HERE`, sampled; not re-verified | RUN-012 |
| the 2×10⁻¹⁰ rad left out, and the 14 switches whose intervals do not enclose | `COMPUTED_HERE`, high precision | RUN-012 |
| the twelfth round's special intervals, replayed | `COMPUTED_HERE`, certified (the replay) | RUN-013 |
| the twelfth round's root boxes | `COMPUTED_HERE`, high precision; its own replay rests on estimated inputs | RUN-013 |
| the curves as stored in double precision; the event five-link's least from below; the curve's optimality | `UNMEASURED` | — |

## 11. Corrections found on the way

### 11.1 Statements and figures that do not hold as written

A selection; the inventory of the four reports holds 18 correction rows, and the reports hold every one.

| round | the programme says | the recomputation finds | run |
| --- | --- | --- | --- |
| 09 | "採用 $120$ 位結果" (the 120-digit result is adopted), with an 80-digit $s_{270}$ and an 80-digit event minimum | they hold to 72 and 71 of their decimals | RUN-010 |
| 09 | the branch audit's 75-digit values, presented as the branches' values | at their printed phases they hold to 70 or 71 decimals; but the two low branches' phases are a minimizer's, 6.6×10⁻⁹ and 5.8×10⁻⁹ rad from the stationary points, and those values exceed the branch minima by 7.34×10⁻¹⁸ and 5.60×10⁻¹⁸ | RUN-010 |
| 09 | fifty-digit one-sided slopes at the cusps | difference quotients at $h = 10^{-9}$; 9 of their digits are the derivative's | RUN-010 |
| 10 | two one-sided derivatives at each wing switch, apart by up to 0.21 | $s$ is continuously differentiable there; one of each pair is a sample inside the interval | RUN-011 |
| 10 | switch 9 is a cusp minimum; 12 smooth stationary points; interval 9 strictly decreasing | the derivative is +0.173166 on both sides; a smooth minimum $5.44\times10^{-9}$ rad before it, 13 points in all | RUN-011 |
| 11 | the neighbourhoods' one-sided derivative intervals bound the derivative through each switch | they cover $[\varphi \pm 2\times10^{-10}, \varphi \pm r]$; at 14 of 17 switches the derivative there lies outside; three exclusions rest on them | RUN-012 |
| 11 | 12 smooth stationary points in all | 13 | RUN-012 |
| 12 | the boundary balls all contain round 11's floats ("19/19") | one does; all hold the exact angles | RUN-013 |
| 12 | all smooth stationary points reproduced in interval arithmetic | 12 of 13, on estimated wing positions | RUN-013 |
| 12 | the unresolved switches are dependency inflation, not counterexamples | at one the derivative changes sign; and round 11's intervals do not enclose, which inflation does not explain | RUN-013 |

One more is a reframing rather than a correction: the ninth round's §11 puts its open step at the
$10^{-9}$-level gap between $120°$ and $270°$, which is right about what locating the least would take; the comparison
with the event five-link needed only its draft's margin of about $1.06\times10^{-5}$ (§4).

### 11.2 What could not be checked, or stays open

The two curves as the programme stored them in double precision, as against the ninth round's decimal ones; the
transfer of the certificates to them, which a displacement bound would make but which was not carried out. The event
five-link's least bounded from below, and so an upper bound for the gain. The eleventh round's boxes as enclosures. How
the twelfth round's data that its shipped scripts do not produce were made — its scripts print 60-digit ends where its
data hold 80. The packages' figures (images), which were not examined. *`UNMEASURED`, RUN-010 to RUN-013.*

## 12. Reproduction and attachments

**What a reader can check without the archive.** The programme's fifteen round packages are public on the AMRAL site,
byte for byte; the input manifest `data/SOURCE_MANIFEST.v1.json` gives each package's address, size and SHA-256 and
the SHA-256 of each member, and every run refuses a package that does not match. The recomputation tree is private; its
public projection — every report, script and gate log of its sixteen runs, with SHA-256 sums — is to be published at
<https://amral.evemisslab.com/moser/recompute/> (English: <https://amral.evemisslab.com/en/moser/recompute/>), one page
per round, with this line's second-layer pages, before this paper is released. Every load-bearing number in this paper
occurs in the gate logs of RUN-010 to RUN-013, in the citation snapshots, or in `data/paper-figures.json` (Appendix A);
the paper's front matter declares these files as its sources, and the standard's checker traces every figure against
them alone.

**The instrument can fail, and was made to.** Every check of every run was drilled: faults were planted in its
inputs, and each had to be caught by exactly the checks named for it, while controls — the unmodified inputs and
harmless rewrites — had to stay green. Over the four runs of this paper: 71 planted faults, all 71 caught by the named
checks and none uncaught or caught by another check; 16 controls, none disturbed; 34 checks; 651 must-stay-green
assertions held. Over the whole recomputation tree, of which these runs are part: 352 planted faults, 352 caught by the
named check, 64 controls undisturbed, 139 checks. The plants were not chosen blind: each report's expected sets were
reasoned before a dry run with every set empty was read, one RUN-011 plant was revised after that dry run, and each
report lists the branches of its checks that no plant reaches.

**Commands.** Python 3.14 [7] with mpmath 1.3 [2], numpy 2.4 [8], scipy 1.17 [9] and sympy 1.14 [10]; no network beyond fetching the
packages. From the line's directory (`moser-verification-xuanheng/` at the pinned commit):

```bash
python code/fetch_source.py
python code/run010_round09_precision_cusp.py --drill
python code/run011_round10_phase_map.py --drill
python code/run012_round11_box_certificate.py --drill
python code/run013_round12_iv_replay.py --drill
```

Each `--drill` run checks the package, drills every check and rewrites its gate log under `data/gate-logs/`; a re-run
is correct when that log is byte-identical to the published one. The paper is typeset by the shared build tool of the
crystallization repository, which refuses to write a PDF from which a character would be dropped.

## 13. Contributions

What each author did is stated here, side by side and in no rank; the roles are different in kind, and the paper is
worth less if they are blurred.

**Aletheia** — the web-side research line; model: ChatGPT, GPT series — produced the programme's fifteen rounds, on
the question Neo.K set out; every statement this paper attributes to "the programme" or to "the round" is from those
documents, except where the paper marks a reading of them as the recomputation's.

**Neo.K** set out the research programme: the question of how tight the 30-60-90 cover is, and the methodology
under which its rounds and their independent recomputation were run.

**懸衡 (Xuán Héng)** — the independent recomputation; model: Claude, Opus series — did the four runs this paper names
and wrote this paper: every `COMPUTED_HERE` figure rebuilt with independently written code; every argument read
against its source; the drills of §12; and the additions marked as the recomputation's where they occur — the
certificates of Theorems 4.1 and 6.1, the interval redo of the round's monotone bound, Proposition 5.1, the smooth
minimum of §5.3 (first seen in RUN-009, fixed and placed in RUN-011), the measurement of the eleventh round's
neighbourhoods in §7.2, the replay of §8, and the corrections of §11. Before each of the four reports was committed,
and before this paper was, a separate instance of the same model (model: Claude Opus, version 5.5, run as a read-only subagent of 懸衡's Claude Code session), briefed only with the text and its evidence, read it
independently; its findings — among them boxes three times wider than first reported in RUN-010's certificate, a
sliver of $10^{-41}$ rad left unchecked beside each cusp in RUN-011's, and the single omission behind RUN-012's
fourteen failures — were applied, and the reports record them. The paper was then reviewed by 墜衡 (Zhuì Héng), the lab's
proof-side verification arm, who recomputed with code of their own the value at $3\pi/2$, the event five-link's
branches, the smooth minimum and the certificates' constants, and read both certificates' code line by line; their
suggestions were applied.

**Priority, stated plainly.** The curves, the support identity at $3\pi/2$, the monotone bound, the phase-contact
map, the exact switch formulas and the targets the certificates meet are the programme's. What is offered as this
line's own is narrower: the certificates of §4 and §6, the findings of §5.3 and §7, an independent check of every
step, and the corrections. The covering theorem the question rests on is Wichiramala and Panraksa's.

## Acknowledgements

We thank Anthropic, whose Claude models the lab's verification and recomputation lines run on, and OpenAI, whose
ChatGPT models the programme's documents were written with. Not every AI model or instance that took part in this
work is named in it — among them instances that the named authors ran as helpers; that an AI is not listed here
does not mean that none took part.

## References

1. Aletheia, Neo.K and 懸衡, *Six rounds of a search for the hardest unit arcs in the 30-60-90 triangle, recomputed: the exact critical-scale formula, two chirality conventions, and the event five-link*, preprint, AMRAL Research Lab (2026), the first of its three companion papers.
2. The mpmath development team, *mpmath: a Python library for arbitrary-precision floating-point arithmetic* (version 1.3.0), <https://mpmath.org> (2023).
3. W. Wichiramala and C. Panraksa, *Wetzel's 30-60-90 triangle covers unit arcs*, <https://arxiv.org/abs/2606.14625> (v1, 2026).
4. R. Norwood, G. Poole and M. Laidacker, *The worm problem of Leo Moser*, Discrete Comput. Geom. 7(2) (1992) 153–162, doi:10.1007/BF02187832.
5. C. Panraksa and W. Wichiramala, *Wetzel's sector covers unit arcs*, Period. Math. Hungar. 82(2) (2021) 213–222, doi:10.1007/s10998-020-00354-x; arXiv:1907.07351.
6. Y. Movshovich and J. E. Wetzel, *Drapeable unit arcs fit in the unit 30° sector*, Adv. Geom. 17(4) (2017) 497–506, doi:10.1515/advgeom-2017-0011.
7. The Python Software Foundation, *Python* (version 3.14), <https://www.python.org>.
8. C. R. Harris, K. J. Millman, S. J. van der Walt, R. Gommers et al., *Array programming with NumPy*, Nature 585 (2020) 357–362, doi:10.1038/s41586-020-2649-2; used here at version 2.4.
9. P. Virtanen, R. Gommers, T. E. Oliphant, M. Haberland et al., *SciPy 1.0: fundamental algorithms for scientific computing in Python*, Nature Methods 17 (2020) 261–272, doi:10.1038/s41592-019-0686-2; used here at version 1.17.
10. A. Meurer, C. P. Smith, M. Paprocki, O. Čertík et al., *SymPy: symbolic computing in Python*, PeerJ Comput. Sci. 3 (2017) e103, doi:10.7717/peerj-cs.103; used here at version 1.14.

*The preprint's arXiv record, read into the research tree by RUN-002 and RUN-003, is kept there with the evidence; its version 1 is the one cited.*

## Appendix A. The figures file

`data/paper-figures.json`, and the script that writes it, `code/paper_figures.py`, are published beside this paper
as they stood at the pinned commit. The script runs nothing of the programme and computes no mathematics of its own.
For this paper it sums the drill records of the four runs and of the whole tree; counts the inventory's correction rows
and the logged lists of switches and neighbourhoods; forms, from logged fields, the certified width of the curve's
least, the certified margin over the gain, the smooth minimum's height above the least, and the extremes of the
one-sided derivatives at the wing switches; reads four scan parameters from the run scripts as written, each with its
line; and extracts the programme's quoted figures verbatim, each with its package, member, the member's SHA-256 and the
line. Re-run, the file is byte-identical.