# RUN-013 — Round 12 (v0.12): the interval replay of the 120°/270° enclosures reproduces to 3×10⁻⁸¹ and the Newton steps hold, but one boundary ball in 19, not 19, holds Round 11's float, the root replay's positions are estimates, and "dependency inflation" explains only part of what it is used for

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-10-20
**Subject:** `Moser_Skew_Lab_v0.12.zip` (SHA-256 pinned in [`corpus.py`](../code/corpus.py)): its README, MANIFEST,
`reports/ROUND_12_REPORT.md`, `ROUND_12_IV_REPLAY_AUDIT.md`, `ROUND_13_SMOOTH_KKT_HANDOFF.md`, the two replay scripts
(read, not run), and its data (`round12_summary.json`, `special_branch_iv_certificate.json`, `exact_boundary_balls.json`,
`root_interval_newton_replay.json`, `boundary_iv_replay.json`), with Round 11's boundaries, neighbourhoods and root
boxes, Round 10's map, Round 09's constants and Round 05's event root, read from the package bytes
**Tools:** [`run013_round12_iv_replay.py`](../code/run013_round12_iv_replay.py) — this run's own replay of the round's
interval method in mpmath's interval arithmetic at 75 digits; RUN-010's to RUN-012's high-precision candidate (40 to
200 digits) for the exact values, the stationary points and the derivative beside each switch;
[`gate.py`](../code/gate.py) for the drill
**Log:** [`run013-round12-iv-replay.json`](../data/gate-logs/run013-round12-iv-replay.json)

**Verdict: PARTIAL** — in RUN-002's sense: what the round computes holds, and four things it states do not. Holding:
the s₂₇₀, s₁₂₀ − s₂₇₀ and event-branch intervals contain the exact values, s₂₇₀ 1.4174×10⁻¹⁰ and the difference
5.3711×10⁻¹¹ from either end, and this run's own interval replay of the round's method gives the two intervals to
3×10⁻⁸¹; the gain interval is their difference; each of the 19 boundary balls holds its formula's exact value; each of
the 12 root boxes holds one stationary point of its kind, its Newton image lies inside it around the root, its
second-derivative interval holds s″ at four points inside it and excludes zero, and its end signs and scale interval are
right; the five direct passes among the switches are the five between two corners, and at eleven of the other twelve the
derivative keeps, on each side, the sign Round 11 states. Not as stated: §3 says the 19 balls "全部包含第 11 輪保存的浮點值"
(all contain Round 11's saved floats), the audit note repeats its 19/19, and the statuses call the balls passed, while
the data say one does — the ball at 0 — and the summary's own all-contain is false; §7 says "所有光滑駐點" (all smooth
stationary points) were reproduced, and they are 12 of 13; the interval Newton runs on wing positions boxed by the gap
between two quadratures plus 10⁻⁵⁵ — an estimate — and on other inputs in point arithmetic, not the directed interval
arithmetic §1 names; and at the twelve switches it calls "dependency inflation, not a counterexample", Round 11's
intervals are not enclosures — even an exact enclosure could not reproduce them — at π/2 + α the derivative changes sign
on the left, at the thirteenth stationary point, and at three others no scale bound stands behind the signs. The
conclusions its figures support — s₁₂₀ above s₂₇₀, the candidate above the event five-link, the least at 3π/2 — hold, as
RUN-011 certified with bounds of its own. The drill planted 17 defects; each tripped exactly the checks named for it,
and the 4 controls disturbed nothing.

---

## What Round 12 claims

Round 12 finds no `python-flint`, Arb or Sage in its environment and uses mpmath's `iv`, "directed interval
arithmetic", as an independent fallback. It encloses s₂₇₀ in [0.99891433894289…, 0.99891433922637…] and s₁₂₀ − s₂₇₀ in
[1.5846×10⁻⁹, 1.6920×10⁻⁹] — "下界仍嚴格為正" (the lower bound is still strictly positive) — and the candidate's margin over
the event control's first branch in [1.0581810×10⁻⁵, 1.0582094×10⁻⁵], "同樣保持嚴格正下界" (likewise keeping a strictly
positive lower bound). It recomputes the 19 boundary formulas as balls, and §3 reports 19/19, "全部包含第 11 輪保存的浮點值". It
runs an interval Newton step on each of Round 11's 12 root boxes: 12/12 "個根盒滿足 interval Newton 包含條件；端點導數符號也全部符合極小／極大分類" (root boxes satisfy the interval Newton inclusion condition; the end-point derivative signs also all fit
the minimum/maximum classification). Of the 17 switches' sides it resolves 5 directly; of the rest, "這是 **dependency inflation**，不是發現反例。第 11 輪的解析誤差界與尺度排除仍保留，但未被本輪後備函式庫獨立重播" (this is dependency inflation, not a
counterexample found; Round 11's analytic error bounds and scale exclusions stand, but were not independently replayed by
this round's fallback library). It does not finish the 579 leaf boxes, and concludes that "最重要的低值競爭與所有光滑駐點，均被另一套區間運算重現" (the most important low-value competition and all smooth stationary points are reproduced by another
interval arithmetic) — support, not a full Arb certificate.

## The checks

| id | guards | result |
| --- | --- | --- |
| W1 | the s₂₇₀, s₁₂₀ − s₂₇₀ and event-branch intervals contain the exact values; the gain is the s₂₇₀ interval less the event interval; this run's own interval replay of the method (65,536 parts, 75 digits) gives the two intervals, to 10⁻⁷⁰ | **PASS** |
| W2 | 19 balls with Round 11's formulas, each holding the formula's exact value and narrower than 10⁻⁶⁹; the containment flags are what the balls hold; the summary's all-contain is their conjunction | **PASS** |
| W3 | each root box holds one exact stationary point of its kind and is Round 11's; its Newton image lies inside it around the root; its second-derivative interval holds s″ at four points inside it (60 digits, to 10⁻¹⁰) and excludes 0; its end signs; its scale interval holds s at the root; the margins; the boxes are all the stationary points | **FAIL** |
| W4 | 17 boundaries with Round 11's formulas and flags; the direct passes are the five switches between corners; at the other twelve, wherever Round 11 states a sign, the derivative keeps it on each side (60 digits) | **PASS** |
| W5 | the summary holds the data files' records and counts; the leaf replay is not completed; the environment | **PASS** |
| W6 | the report's intervals (§2) and tables (§4, §5), its counts, statuses, the README, the audit note, the manifest and the handoff; their account of the boundary balls against the data | **FAIL** |
| W7 | the replay scripts' constants are Round 09's decimals and their methods are those stated | **PASS** |

## Findings

### 1. What holds

The special intervals contain the exact values: s₂₇₀ lies 1.4174×10⁻¹⁰ inside each end of its interval, and s₁₂₀ − s₂₇₀
5.3711×10⁻¹¹ inside each end of its own (`s270_inside_interval_by`, `difference_inside_interval_by`); the event branch's
interval holds Round 09's B1, and the gain interval is the s₂₇₀ interval less it (W1). This run's own replay of the
method — midpoint sums of sin θ, cos θ and q(θ) over 65,536 parts in interval arithmetic at 75 digits, plus the analytic
midpoint error M/(24N²), written anew and not running the round's script — gives the stated intervals to 3×10⁻⁸¹ at
either end (`replay_minus_stated`): the round computed what it says. The 19 balls each hold their formula's exact value,
at most 2.2×10⁻⁷⁰ wide (W2). Each root box holds one stationary point of its kind, the Newton image lies inside it and
holds the root, and the second-derivative test (at four points of the box), the end signs and the scale interval hold
(W3). The five direct passes among the switches are π/2, 2π/3, π, 3π/2 and 5π/3, the five between two corners (W4).

### 2. The boundary balls: one in 19

Each ball is the exact angle, about 10⁻⁷⁰ wide; Round 11's saved phases are doubles from a double-precision evaluation of
the formulas, up to 3.8×10⁻¹⁶ from the exact angles (`round11_float_minus_exact_largest`) — eight of them not the double
nearest the angle. So no ball but the one at 0 can hold its double, and the data's flags say exactly that: one ball of 19
holds Round 11's float, and the summary's `all_contain` is false (`balls_containing_round11_float`). The report's §3
nevertheless boxes 19/19 and says "全部包含第 11 輪保存的浮點值", the audit note repeats "解析邊界：19/19", and the summary's and
the manifest's statuses call the balls passed — which the balls are, as enclosures of the exact angles, but not by §3's
own criterion, which the same summary's `all_contain: false` contradicts (W6).

### 3. Twelve stationary points of thirteen

The 12 root boxes are Round 11's, and the thirteenth stationary point, the smooth minimum 5.44×10⁻⁹ rad before π/2 + α
(RUN-011, RUN-012), is in none of them (W3's failure; 13 points in all, `stationary_count`): it lies inside the
neighbourhood of that switch, which Round 11 excludes by its scale. So "所有光滑駐點，均被另一套區間運算重現" is not so; 12 of 13
are, on estimated positions (§4 below).

### 4. The root replay's inputs are estimates

The interval Newton step runs in interval arithmetic, but its inputs are not enclosed by it. The replay script takes
each wing position as the interval between two quadratures — mpmath's tanh–sinh and Gauss–Legendre, split at the layer's
centre — widened by their difference and 10⁻⁵⁵, an estimate of the error, not a bound on it (W7 reads the line); it
computes the inverse of the tangent angle, the bounds on θ′ and the support's phase constant in point arithmetic; and it
enters A and B through their decimal strings. At 80 digits the two quadratures agree exactly at the wing's end
(`quad_minus_quadgl_at_wing_end`, with this run's split; the round's split agrees too), so the estimate is ±10⁻⁵⁵ there,
and every Newton inclusion this run checks holds. The result is high-precision evidence, not the directed interval
arithmetic §1 names for the replay.

### 5. "Dependency inflation, not a counterexample"

At eleven of the twelve switches the round could not resolve directly, there is indeed no counterexample: the derivative
keeps, on each side, the sign Round 11 states, the switch included (W4, at 60 digits). At the twelfth, π/2 + α, Round 11
states no sign — it leaves the switch unresolved and excludes it by its scale, 7.39×10⁻² above s₂₇₀ — and the derivative
does change sign on the left, at the thirteenth stationary point. That a natural interval extension through the inverse
tanh near atanh(±1) is wide may well be why the round's own intervals could not fix the signs; this run did not compute
those intervals. But it is not the whole reason Round 11's narrow boxes could not be reproduced: RUN-012 found that at
every one of these twelve switches Round 11's one-sided interval leaves out the 2×10⁻¹⁰ rad beside the switch, where the
derivative moves by 0.022 to 0.157, so the interval misses values the derivative takes
(`inflation_boundaries_round11_shortfall`); even an exact enclosure over the side would be wider. And at three of the
twelve — π/2 − α, π/2 − β, β − π/3 — Round 11 has no scale exclusion, so "第 11 輪的解析誤差界與尺度排除仍保留" leaves those three
resting on intervals that do not enclose. The conclusion there is true — RUN-011 certified the least at 3π/2 by another
route — but neither round's certificate shows it.

### 6. The scripts do not make all the data

The shipped special-branch script prints 60-digit ends and no event interval, where the data hold 80-digit ends and the
event interval; the root script prints the second derivative, the Newton image and its inclusion, where the data also
hold end signs and scale intervals; and no script makes the balls or the side replay. W7 checks the fragments the
scripts do contain; the rest of the data comes from code the package does not ship.

## At what strength each result stands

| result | strength |
| --- | --- |
| the special intervals contain the exact values; the replay gives them | interval arithmetic, this run's and the round's alike, with the analytic midpoint error; the exact values at 100 to 200 digits |
| the balls hold the exact angles; one holds its double | high precision (the formulas at 90 digits) |
| the Newton steps, second derivatives (at four points), end signs and scales of the 12 root boxes | high precision at 60 digits; the round's own replay rests on estimated positions |
| 13 stationary points | RUN-011: exact in number on the corner-only intervals, a refined scan on the wing intervals |
| the signs beside eleven unresolved switches; the sign change beside π/2 + α | high precision: the derivative at the switch and beside it, at 60 digits; not an interval enclosure |
| the conclusions the round's figures support | certified by RUN-011 with its own bounds |

## The drill

| | |
| --- | ---: |
| planted defects | 17 |
| tripping exactly the checks named for them | **17** |
| controls (the package unmodified, the report with CRLF endings, the README with trailing spaces, the root records copied) | 4 |
| controls that disturbed nothing | **4** |
| must-stay-green assertions held | **129/129** |

Plants include a triangle leg, the event-branch interval, a ball's ends and another's containment flag, a Newton image,
a second-derivative interval, a root margin, a switch's direct pass and another's formula, two summary records, a §4
distance, a README count, a manifest status, the handoff's unknowns, a replay constant and the root replay's error
line. The expected sets were reasoned before the dry run with every set empty was read, and it tripped exactly them; so
17 of 17 says the reasoning matched the harness, not that the plants were chosen blind. Where a plant moves a figure the
checks compare elsewhere — a data record and the summary's copy of it, a switch's pass with its counts, §5's cell, §5's
count and the README's — the restatements are planted alike, so that only the comparison can see the plant. W3 and W6
fail on the package with fixed-text messages, so their plants trip them through a figure that holds. The triangle leg
alone reaches W1's containment tests (s₂₇₀, the difference, the event branch) and its two replay tests, and W3's
one-stationary-point and scale tests; no plant reaches W1's flags, W2's formula and count tests and its all-contain,
W3's box-is-Round-11's and end-sign tests, W4's count and sign-kept tests, W5's record identities and boundary counts,
most of W6's patterns, or W7's other fragments. Of the four controls, the unmodified package exercises nothing by
construction; the report with CRLF endings re-runs W6, the README W6, the copied root records W3, W5 and W6. Each check,
replaced in turn by one that always passes, was reported blind in exactly as many cases as plants name it — W1 2, W2 2,
W3 4, W4 2, W5 2, W6 4, W7 2 — which by construction shows only that the harness counts as described (seven runs; a
blind run writes no log). Two runs of the drill made side by side wrote gate logs with the same SHA-256.

The instrument was wrong before it was right, in ways worth recording. The first ball test asked for widths below
10⁻⁷⁰, where the round's 70-digit balls run to 2.2×10⁻⁷⁰. The first replay differed from the round's ends by up to
2×10⁻²⁷, which this run did not trace (a replay run in a 30-digit interval context differs by about that much); rewritten
to read every end at full precision, it agrees to 3×10⁻⁸¹, and the tolerance is now 10⁻⁷⁰, the replay's own rounding,
not one fitted to the difference. An independent reading of this report before it was committed confirmed the replay,
the Newton images and s″ with code of its own, and found the sign test claimed for twelve switches where it covers
eleven, the audit note credited with §3's sentence, the doubles described as nearest roundings, a wrong account of the
first replay's difference, the unplanted branches misstated, the round's conclusions endorsed beyond the figures, and
the scripts' gaps unmentioned; all are corrected here.

## What this run does not establish

That the round's root boxes or Round 11's boxes are certified: their inputs rest on estimates, and this run's checks of
them are high-precision samples. How the data the scripts do not make were made. A repair of the exclusions at π/2 − α,
π/2 − β and β − π/3 inside either round's scheme: RUN-011's certificate covers them by another route. Any bound for
Moser's problem. Nor the package's three figures, which were not examined.

## Re-running

```
python code/fetch_source.py
python code/run013_round12_iv_replay.py --drill
```

The run is correct when the gate log is byte-identical to the committed one.