# moser-verification-xuanheng — the Moser worm problem, recomputed

The second layer for the AMRAL case *Moser's worm problem*: find the least area of a planar convex set that
contains, after a rigid motion, every curve of length 1. The first layer (`/moser/` on the AMRAL site) holds the
programme's fifteen round packages, v0.1 to v0.15, "semi-autonomous research (led by Neo.K)". Fourteen of the
fifteen READMEs say the round does not constitute a new upper or lower bound for the problem; round 12's says
nothing about bounds, and nor does anything else in its package (RUN-001). This layer measures what each round does
establish, and at what strength.

This tree is 懸衡's (Xuán Héng's), the recomputation arm that recomputed the Lebesgue case
(`lebesgue-verification-xuanheng`). It works the same way.

## What a run does

One run per round, in the programme's own order (RUN-001 is the corpus). A run

- recomputes every finite claim of the round with independently written code — never by running the round's
  scripts, which are read only after the rebuild, to compare;
- reproduces every construction the round reports (curves, containers, critical scales, contact ledgers);
- reads every theorem-level step against its source, and says which steps rest on a cited theorem;
- states each result at the strength it was measured: exact or interval-certified, numerical, cited, or not
  established — never stronger than the evidence;
- ends in a gate log (`data/gate-logs/`) and a report (`reports/`), with a mutation drill: planted faults that
  must each be caught by the check named for them, controls that must disturb nothing. A run is recorded only
  when a cold re-run reproduces its gate log byte for byte.

## The corpus

The fifteen packages are the original zips the first layer publishes, pinned in `code/corpus.py` by size and
SHA-256 from the site's own manifest (site revision `d7a8e7a4`). `python code/fetch_source.py` downloads them
from their public URLs into `data/source/` and keeps nothing that fails a pin; they are read in memory and
never extracted. 15 packages, 12,039,698 bytes, 282 files.

| round | package | files |
| --- | --- | ---: |
| v0.1 | `Moser_Skew_Lab_v0.1.zip` | 13 |
| v0.2.2 | `Moser_Skew_Lab_v0.2.2.zip` | 29 |
| v0.3 | `Moser_Skew_Lab_v0.3.zip` | 13 |
| v0.4.1 | `Moser_Skew_Lab_v0.4.1.zip` | 16 |
| v0.5 | `Moser_Skew_Lab_v0.5.zip` | 17 |
| v0.6.1 | `Moser_Skew_Lab_v0.6.1.zip` | 18 |
| v0.7 | `Moser_Skew_Lab_v0.7.zip` | 21 |
| v0.8.3 | `Moser_Skew_Lab_v0.8.3.zip` | 30 |
| v0.9 | `Moser_Skew_Lab_v0.9.zip` | 16 |
| v0.10 | `Moser_Skew_Lab_v0.10.zip` | 14 |
| v0.11 | `Moser_Skew_Lab_v0.11.zip` | 19 |
| v0.12 | `Moser_Skew_Lab_v0.12.zip` | 15 |
| v0.13 | `Moser_Skew_Lab_v0.13.zip` | 18 |
| v0.14 | `Moser_Skew_Lab_v0.14.zip` | 21 |
| v0.15 | `Moser_Skew_Lab_v0.15.zip` | 22 |

## Status

| run | subject | result |
| --- | --- | --- |
| [RUN-001](reports/RUN-001-CORPUS-IDENTITY.md) | corpus identity: the first layer's pages against these packages | packages PASS; pages FAIL 5 of 7 checks, all presentation |
| [RUN-002](reports/RUN-002-ROUND01-SUPPORT-SKEW-LP.md) | Round 01 (v0.1): support-skew linear programs, the curve library, the first adversarial search | PARTIAL — reproduces; the maxima are a grid's, the records a local search's, the candidate's scale one handedness's (mirror: 0.8945); 34 curves, not 35 |
| [RUN-003](reports/RUN-003-ROUND02-PHASE-SCAN-CHIRALITY.md) | Round 02 (v0.2.2): the contact ledger, phase scans, the exact formula, the chirality correction | PARTIAL — reproduces; the main report's numbers are the 256-grid's (its own addendum corrects them); two stated scales 3–7×10⁻⁹ above their minima; the three-link family reaches 0.998697792, above the corrected 0.998573795; two arcs undefined, the U surface only partly |
| [RUN-004](reports/RUN-004-ROUND03-SYMMETRIC-LINKS.md) | Round 03 (v0.3): mirror-symmetric five- and seven-link families on the exact formula | PARTIAL — reproduces to 1.4×10⁻¹³; the seven-link family holds every five-link curve, so its lower optimum (8.0×10⁻⁵ below) is the search's, not the family's; against the three-link family's best the five-link gains 5.66×10⁻⁵, not 1.80×10⁻⁴; both endpoints on the hypotenuse is the imposed symmetry at φ = 2π/3 |
| [RUN-005](reports/RUN-005-ROUND04-BRANCH-EQUALIZATION.md) | Round 04 (v0.4.1): the phase-branch ledger and the four-branch equalization of the five-link | PARTIAL — reproduces (0.998903750476 at φ = 3π/2, nine minima, ledgers); the four branches level to 2.7×10⁻¹² are the tracker's (true spread 1.30×10⁻⁸, as its own audit says); the sensitivity matrix holds to 2.3×10⁻⁵–1.5×10⁻⁴, not to its printed eight decimals; the four branch minima sit at exact phases, where re-equalized they level to 10⁻¹⁵ at 0.998903757133, the next round's value |
| [RUN-006](reports/RUN-006-ROUND05-CONTACT-EVENTS.md) | Round 05 (v0.5): the contact-event equations and the nonsmooth KKT system | PARTIAL — the closed forms, the nine equations, the Jacobian's rank, the 40 trials and the audit reproduce; the one-sided derivatives and σ_min, κ are not right to their printed digits; the root 0.998903757132509 satisfies the second-order sufficient condition (curvature −0.123): a strict local maximum of the four-branch model, and by continuity of the curve's least scale on a neighbourhood of unestablished size |
| [RUN-007](reports/RUN-007-ROUND06-CHIRALITY-ESCAPE.md) | Round 06 (v0.6.1): chirality escape, the eight-parameter five-link search, the census, the local stability draft | PARTIAL — the modes, escape, census, audit and draft reproduce; the modes' chirality gaps are grid-sample differences (off by up to 3.7×10⁻⁴); the search's best is 3.47×10⁻⁴ below the root it contains and did not re-converge to mirror symmetry; the four branches' antisymmetric gradients are nonsingular, so the root is a strict local maximum of the congruent least scale among nearby five-links (neighbourhood unsized) |
| [RUN-008](reports/RUN-008-ROUND07-CURVATURE-WINGS.md) | Round 07 (v0.7): segmented curvature wings and the constant-curvature arc wing against the event five-link | PARTIAL — the control, the segmented candidates (their rule inferred from the curves), both arcs and the sample reproduce; the arc's 4.14×10⁻⁵ deficit stands at a local maximum of the arc family; every segmented family reaches the event five-link in the limit, so their deficits are the search's; the m = 6 signature is Round 05's B2 event, not another mechanism |
| [RUN-009](reports/RUN-009-ROUND08-SMOOTH-LAYER.md) | Round 08 (v0.8.3): the finite-width tanh curvature layer against the event five-link | PARTIAL — the headline reproduces in independent code and at the least phase in 40-digit arithmetic: least scale 0.998914339084632, 1.0581952124×10⁻⁵ above the event five-link; the best candidate's curve file is not the candidate (centre cut short, right wing off-step, endpoint missing: as a curve 0.998794830, below the five-link); the printed curvature digits, an audit's "約 $10^{-6}$" and a cloud note's "method difference" do not hold as stated; the event five-link is not a local maximum among curves |
| [RUN-010](reports/RUN-010-ROUND09-PRECISION-CUSP.md) | Round 09 (v0.9): the 270° cusp in arbitrary precision, the monotone Darboux enclosure, the branch audit | PARTIAL — s₂₇₀ holds to the summary's 120 digits, and the event control and the difference reproduce; the Darboux bound is sound, and certified here in interval arithmetic; the 80-digit s₂₇₀ and s₀ of the README and the report hold to 72 and 71 decimals, the branch audit's 75-digit values to 70, §8's derivatives (h = 10⁻⁹ quotients) to 9; certified over the whole phase circle, the candidate's least scale exceeds the event five-link's by more than 1.050×10⁻⁵ |
| [RUN-011](reports/RUN-011-ROUND10-PHASE-MAP.md) | Round 10 (v0.10): the full phase-contact map, the stationary points and the global numerical exclusion | PARTIAL — the 18 intervals, the 17 switches (to 10⁻¹³) and the 12 stated stationary points reproduce; at the 12 switches where a wing's interior support meets a corner s is continuously differentiable, but two different one-sided derivatives are stated; the cusp minimum at 3.028 rad is a smooth minimum 5.4×10⁻⁹ rad before it, which the lists, guards and ledger miss (13 stationary points); certified in interval arithmetic: the least is at 3π/2 alone, s(3π/2) in [0.998914339066915, 0.998914339102351] |
| [RUN-012](reports/RUN-012-ROUND11-BOX-CERTIFICATE.md) | Round 11 (v0.11): exact contact boundaries, derivative boxes, root boxes, switch neighbourhoods and the 120°/270° enclosures — a semi-validated certificate | PARTIAL — the 19 boundary formulas are exact, the special enclosures contain the exact values, the 579 derivative boxes and 12 root boxes hold where sampled; the neighbourhoods' one-sided derivative intervals leave out the 2×10⁻¹⁰ rad beside each switch and miss the derivative there at 14 of 17 switches (by up to 0.157 at the wing switches), and three exclusions rest on them; 13 stationary points, not 12; the qualitative conclusions hold, certified by RUN-011 with its own bounds |
| [RUN-013](reports/RUN-013-ROUND12-IV-REPLAY.md) | Round 12 (v0.12): the mpmath.iv replay — special enclosures, boundary balls, interval Newton on the root boxes, the switches' sides | PARTIAL — the special intervals contain the exact values and an independent replay gives them to 3×10⁻⁸¹; the balls and Newton steps hold; but §3 says 19/19 balls hold Round 11's floats where the data say 1/19, 'all' stationary points are 12 of 13, the Newton positions rest on estimated quadrature errors, and 'dependency inflation' does not explain intervals that do not enclose |
| [RUN-014](reports/RUN-014-ROUND13-SMOOTH-KKT.md) | Round 13 (v0.13): the five-parameter smooth event-KKT system — the four branches, gradients, pressures, the 12×12 Jacobian, restarts, curvature ledger, full phase audit | PARTIAL — the branches, gradients (to 1.6×10⁻⁷), residual, restarts' records and ledger hold; this run's own solution of the twelve equations lies 6×10⁻⁸ from the stated point and is a strict local maximum on an unsized neighbourhood; the least is certified at s₁₃ − 1.5×10⁻¹⁰ or above, a gain over Round 08 of 4.0451–4.2486×10⁻⁹; but the stated singular values are not the Jacobian's (condition 2.1×10³, not 3.8×10⁷: not 'highly ill-conditioned'), §7's projection is not reproduced, three of the four other minima are not the curve's, and the pressures are printed past their digits |
| [RUN-015](reports/RUN-015-ROUND14-DOUBLE-PEAK.md) | Round 14 (v0.14): double-peak curvature, chirality breaking and the single peak's local stability | PARTIAL — the curve files, the high-resolution cusps, the profile's cusps and the chirality data hold, and the mirror symmetry is a strict local maximum of the congruent scale; but the single peak is a saddle against splitting (the Lagrangian's curvature along the separation +1.587×10⁻⁴): split into two halves with its five parameters re-solved, the curve's least is certified 1.1924×10⁻⁷ above Round 13's at separation 0.03, inside the family the round searched; its profile holds the parameters fixed, its search's low branches run 10⁻⁸ low, from d = 0.028 its profile phases are interval ends, one fit is not the shipped data's, and its minima lists are phase samples |
| [RUN-016](reports/RUN-016-ROUND15-FUNCTIONAL-MODES.md) | Round 15 (v0.15): curvature function modes, the pressure-projected Hessian, the branch-opening window and the eight-mode candidate | PARTIAL — the candidate stands: at 40 digits its branches hold to 2×10⁻¹⁴ (least 0.99891448071696448, latent margin 3.0046×10⁻⁹, nine minima), and its least is certified 1.3725–1.3758×10⁻⁷ above Round 13's; the curve file, mode gradients, Hessian, profiles and Newton line are their data's; but Round 13's point is not stationary in the modes (P4 gradient −1.98×10⁻⁶), so the Hessian decides nothing there, the base's low-branch gradients are off by 10⁻⁵ and its four-way tie is the evaluator's, the ledger's takeover opens and closes before the stated window, and the headline figures are printed past their digits |

RUN-001's consequences for every later run: read the package bytes, never the site's served copies. Five package
documents (rounds 4, 8, 12) carry TeX whose backslash escapes became control characters when they were written;
restore them with `restore_escapes` in `code/run001_corpus_identity.py` before reading their TeX.

RUN-002's, for the rounds after it: a grid scale program is a relaxation, so a container's true value must be
computed apart from its grid value; the round's triangle has its short leg on the x-axis; a chiral curve has two
critical scales, one per handedness. Round 01's package ships no program, and a curve or a setting a round's
documents do not define is not rebuilt.

RUN-003's: for the triangle, the exact three-normal formula replaces any direction grid; a minimum over phases is
refined by golden section, which cannot stall at a kink as a parabolic step can; Round 02's three-link baseline is
not the family's best (this tree's search reaches 0.998697792 against the 0.998574374711 Round 03 uses).

RUN-004's: before a larger family's lower optimum is read as "more parameters do not help", the families it contains
are written into it and evaluated — a family's optimum is at least every contained curve's; a summary's "metrics" are
a phase grid's samples, not minima; for a curve symmetric about the y-axis whose endpoints decide the minimum, the
minimizing phase is 2π/3 and the endpoints' tie on the hypotenuse is the symmetry's.

RUN-005's: a branch minimum at a phase where a contact identity switches — a link parallel to a leg, a
symmetry tie — is a closed form in the curve's parameters, smooth where a one-dimensional minimizer over phases stalls;
a resolution table whose grids all contain the minimizing phase shows nothing about resolution. RUN-006's: at a max-min root with every multiplier positive, the critical cone is the gradients' null space — a
line when they have rank 3 — and the Lagrangian's curvature along it decides between a maximum and a saddle; complex-step derivatives make the closed forms'
gradients exact to rounding. RUN-007's: a one-parameter scan of an antisymmetric mode peaks at the symmetric point by symmetry alone; local
stability against chirality breaking is the nonsingularity of the branches' antisymmetric gradients, which reduces
the general problem's critical cone to the symmetric one's. RUN-008's: before a smoothing is said to lose to a polyline, check whether its family reaches the polyline in a
limit; a contact signature is read against the events already named before it is called a new mechanism. RUN-009's: a curve file is read as a curve before it is published as the candidate; a local maximum within a polyline family is not one among curves when a smoothing family contains it as a limit; a "difference between methods" is taken at one phase on both sides. RUN-010's: a comparison of two least scales needs only its own margin — a lower bound for one, from points of the curve in interval boxes and a Lipschitz cover of the phases, against any one phase's value for the other — not where either least lies; a figure printed past the precision it was computed at holds only to that precision; a bound is printed cut toward its safe side. RUN-011's: where a smooth layer leaves a wing nearly straight, the derivative is continuous but steep beside a switch, and a sampled guard sees neither the slope nor a root there; a least's location needs a bound beside each cusp — the active corners' sum moving away from its value — and a second-order cover elsewhere. RUN-012's: an interval in a certificate is checked at its box's own ends, the switch included, in a precision that resolves them — double precision cannot place a point within an ulp of a switch; a sign read from an interval that does not enclose is not shown, even when it is right. RUN-013's: a replay is checked by computing it again, at full precision; a status line is read against the record it summarizes; an error estimate inside interval arithmetic is still an estimate. RUN-014's: a Jacobian's spectrum is checked by building it at the system's solution from derivatives accurate far past its smallest singular value, with two steps that agree — a system whose entries are of order one has no singular value of 10⁸; at a max-min solution with every multiplier positive, five parameters and gradients of rank 3, the critical directions are a plane, and the reduced Hessian there decides between a maximum and a saddle; a listed minimum is the derivative's zero, not a sampled phase near it; a gain between two least scales is bounded below by a lower bound on the new least, set just below its tie, less an upper bound on the old, and above by an upper bound on the new less a lower bound on the old. RUN-015's: when a family is widened by a direction the old optimum is symmetric in — the exchange of two identical halves — the first-order test passes by symmetry and says nothing; the Lagrangian's curvature along that direction decides, and a profile with the other parameters held fixed measures the wrong thing; a cusp is taken where its two sides tie, which moves once the symmetry that pinned it breaks; an ascent found by second-order theory is certified on the curve itself, over the whole phase circle. RUN-016's: before a Hessian is read, the first-order test in the new directions — a point stationary in its own parameters is not therefore stationary in a wider family, and where a pressure-weighted gradient is not zero the second-order signs decide nothing; a curve defined by an integral of a density is certified by enclosing the integral itself, with a rule of high enough order and derivative bounds from interval Taylor arithmetic; a ledger of re-solved points is read row by row, since a window can open and close before it opens for good; a two-sided gain needs a certified lower bound on the old least, not on one of its branches. With RUN-016 the fifteen rounds are recomputed;
the Moser papers come next. The related worm-problem lines on the site — the skew field and
WSFC — are outside this tree for now.

The papers are measured first: [`crystal/`](crystal/README.md) holds the inventory — 403 items, each round's claims
at the strength the runs measured, every one quoted from its report — from which the crystallization census counts.

## Re-running

Python 3.14, no network beyond `fetch_source.py`. From this directory: `python code/fetch_source.py`, then each
`python code/runNNN_*.py` (and `--drill`). A run rewrites its gate log; it is correct when the log is
byte-identical to the committed one. `python -X utf8 code/check_inventory.py` checks the inventory against the
reports.