# RUN-003 — Round 00's governance, measured on the corpus it governs

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-24
**Subject:** Round 00 §25 (canonical source) and §21.6 (claim ledger), applied to the 42 canonical documents — Rounds 00–37 and the four methodology tracks — read from the archive
**Tools:** [`run003_round00_governance.py`](../code/run003_round00_governance.py)
**Logs:** [`run003-round00-governance.json`](../data/gate-logs/run003-round00-governance.json); the status registry [`STATUS_REGISTRY.v1.json`](../data/STATUS_REGISTRY.v1.json)

**Verdicts.**

- **§25, canonical source: PASS.** All 42 documents are valid UTF-8 without a byte
  order mark; every `$$` and every `$` is paired; no other math delimiter, no
  `\uXXXX` round-trip, no mojibake; no key, private key, e-mail address, local path
  or chat URL. The whole archive, 1,049 text files, carries none either.
- **§21.6, claim ledger: FAIL, as a statement about conformance.** Round 00 says
  every important result carries exactly one of ten statuses. The corpus labels its
  results mostly in other words: of 758 judgment statements the census finds, 89
  use one of the ten. The two commonest result labels — `PASS` (118) and `PROVED`
  (72) — are not among them, and 238 distinct status phrases are outside Round 00's
  vocabulary. *(Census v5; see the corrections at the end. The figures in the census
  section below are v2's.)*

The second verdict is about bookkeeping, not mathematics. It matters for one
reason, given below, and it changes how this tree reads every later round.

---

## §25 — the gate

Round 00 §25 lists what every canonical source must satisfy before it is
committed. Five of its six items are mechanical, and are checked here as written;
the sixth — that key formulas can be rebuilt from the source — is a reading
question, and is `UNMEASURED` by this round.

| check | Round 00 §25 item | result |
| --- | --- | --- |
| G1 | UTF-8 decodable | PASS — 42/42, none with a byte order mark |
| G2 | display delimiters paired | PASS — an even number of `$$` outside code in every document |
| G3 | inline delimiters paired | PASS — an even number of single `$` in every paragraph, outside code and display blocks, escaped `\$` excepted |
| G4 | no other math delimiters | PASS — no `\(` `\)` `\[` `\]`, no `equation`/`align`-type environment outside `$$` |
| G5 | no `unicode_escape` round-trip | PASS — no literal `\uXXXX`, no cp1252 mojibake |
| G6 | no secrets, keys or private data | PASS — no API key, private key, e-mail address, local path or chat URL |

G6 reads code blocks too — a path in a reproducibility snippet leaks as surely as
one in prose — and skips only math, because notation such as `f:\mathbb{R}\to`
parses like a drive path. On its first run G6 fired once, on the Round 06 heading
*disk-to-Reuleaux-triangle violation*: the `sk-` inside `disk-` matched a key
prefix. The pattern now requires a key prefix to start a token, and that heading's
shape is one of the drill's controls.

**Beyond the 42.** §25 governs canonical sources, but the archive they come from is
meant to become public too, so G6's patterns were also run over every text file in
it — 1,049 `.md`, `.json`, `.py`, `.txt`, `.csv`, `.dot` and `.svg` leaves. One
hit: `d@np.column_stack(...)` in a Round 26 script, Python's matrix-multiplication
operator read as an e-mail address. Nothing else.

**Measured, not gated — Unicode math in prose.** §25 forbids turning LaTeX into
Unicode math characters. Outside math and code there are 17 such characters in 5
documents: arrows used as prose (`d36 → d38`) and three `≥` used as list shorthand
in Round 16 (`≥5-cycle：142 seeds`). No formula was found written in Unicode in
place of LaTeX.

### Drill

| kind | named check |
| --- | --- |
| invalid UTF-8 bytes; a byte order mark | G1 |
| an unpaired `$$` | G2 |
| a stray `$` in a paragraph | G3 |
| `\(x\)`; `\[x\]`; an `equation` environment | G4 |
| a literal `\u4e2d`; cp1252 mojibake | G5 |
| an API key; an e-mail address; a Windows user path; a POSIX home path; a chat URL; a private-key header | G6 |

Controls: the unmodified corpus; `$` and `$$` inside a fenced code block; an
escaped `\$` in prose; `\[x\]` inside a code span; an arXiv URL; `f:\mathbb{R}\to`
inside math; a hyphenated prose phrase containing `sk-`.

**15 / 15 plants caught by exactly the named checks, 7 / 7 controls undisturbed,
117 / 117 must-stay-green assertions held.** Each check blinded in turn is reported
blind in exactly as many cases as plants name it (G1 2, G2 1, G3 1, G4 3, G5 2,
G6 6).

## §21.6 — the census

Round 00 §21.6:

> 每個重要結果只能使用下列狀態之一

*(each important result may use only one of the following statuses)* —
`PROVED-ANALYTIC`, `VERIFIED-COMPUTATIONAL`, `VERIFIED-THEOREM-APPLICATION`,
`DERIVED-CANDIDATE`, `NUMERICAL-EVIDENCE`, `CONDITIONAL`, `COMPUTE-DEFERRED`,
`OPEN`, `REJECTED`, `CORRECTED`.

The census reads every statement in a judgment position. The corpus uses six
shapes, and the extractor reads all six: a line holding only the status in
backticks, after a heading naming the claim or with the claim named inside the
backticks as `` `HANDOFF-A: PASS` `` (304 — the commonest); the status itself as a
heading (82 — how Round 10 writes its ledger); `\boxed{\text{GATE: STATUS}}` (70); a
bold summary line `**X：STATUS**` (31); `狀態：` / `status:` lines (10); and a status
in backticks inside a table cell (9).

| | statements |
| --- | ---: |
| judgment statements found | **506** |
| using one of the ten claim statuses | 56 |
| using Round 00's gate words (`CLOSED`; `OPEN` counted above) or its `YES` / `NO` | 52 |
| using a phrase outside Round 00's vocabulary | **398**, in 190 distinct phrases |

The ten, in judgment position:

| status | uses | where |
| --- | ---: | --- |
| `COMPUTE-DEFERRED` | 22 | as a judgment, Rounds 01–19 and DLMVC; as a word in the text, through Round 25; nowhere after |
| `OPEN` | 20 | throughout |
| `REJECTED` | 5 | Rounds 10–13 (including the ledgers of Rounds 10 and 12) |
| `CORRECTED` | 3 | Rounds 11, 12, 19 |
| `PROVED-ANALYTIC`, `VERIFIED-COMPUTATIONAL`, `CONDITIONAL` | 1 each | all three in Round 10's claim ledger |
| `VERIFIED-THEOREM-APPLICATION` | 1 | Round 10, §7 |
| `DERIVED-CANDIDATE` | 1 | DLMVC |
| `NUMERICAL-EVIDENCE` | 1 | Round 16 |

The commonest labels outside the ten:

| status | uses | first |
| --- | ---: | --- |
| `PROVED` | 66 | Round 02 |
| `PASS` | 44 | Round 01 |
| `DEFINED` | 18 | DLMVC |
| `FORMALIZED` | 10 | Round 05 |
| `IMPLEMENTED` | 9 | Round 11 |
| `VERIFIED` | 7 | Round 07 |
| `LIFT-CLOSED` | 6 | Round 07 |
| `PUBLICATION-CANDIDATE` | 4 | Round 28 |
| `ARITHMETICALLY-CLOSED-PROTOTYPE` | 3 | Round 29 |

The extractor is approximate in one direction: a backticked line can be an
identifier rather than a status (a correction id such as `R01-CORRECTION-001`, a
node type such as `REP`, a lemma's name), and those are counted among the 190. The
finding does not rest on them. It rests on `PROVED` and `PASS` — 110 labels on
important results, neither one of the ten.

### Why it matters

The ten statuses are not arbitrary names. They separate *how* something is known:
`PROVED-ANALYTIC` from `VERIFIED-COMPUTATIONAL` from `VERIFIED-THEOREM-APPLICATION`
— a proof, a computation, or an appeal to someone else's theorem. A bare `PROVED`
does not say which. That distinction is exactly the one a counter-proof reading
needs first: an analytic proof is attacked by reading it, a computation by
recomputing it, a theorem application by instantiating the theorem's hypotheses.

So this tree does not read a round's strength off Round 00's ladder. For every
status it meets, it records the definition the corpus gives — or that none is given
— in the [status registry](../data/STATUS_REGISTRY.v1.json), which lists each of
the 203 phrases with where it first appears and every place it is used. Every
`PROVED` gets classified here as analytic, computational or theorem application
when the round carrying it is read. The registry's 66 `PROVED` entries, each with
the heading of the claim it labels, are in effect the list of theorem-level steps
this sweep has to check.

Two things in the corpus's favour, stated at their strength. Round 10 keeps a claim
ledger in exactly the ten words, including a `CONDITIONAL` for the `0.835` bound
and a `REJECTED` for reading its dry run as a global theorem. And
`COMPUTE-DEFERRED` is used consistently through Round 25 — the computation-debt
discipline held where the claim ledger did not.

### Census drill

The census is a measurement, not a gate, but it has to see what is planted: a
ten-word status is counted as inside the vocabulary; an invented status is counted
as outside — on its own line, named inside the backticks, after `狀態：`, and in a
table cell; a boxed gate judgment is counted; the invented status inside a fenced
code block is not. **7 / 7.**

## What this round does not establish

- §21's per-round format (metadata, previous state, objective, derivation,
  counterexample section, freedom ledger, computation debt, reproducibility,
  handoff) — `UNMEASURED`. Section names vary too much for a mechanical check to be
  honest; each round's own structure is read when that round is.
- §25's sixth item — that key formulas can be rebuilt from the source — `UNMEASURED`.
- Whether any status outside the ten is well defined. That is the registry's job,
  one round at a time, starting with Round 01.

## Correction — census v2 (made the same day, while reading Round 01)

The census as first committed (v1) missed two of the six judgment shapes and misread
a third. Round 01 exposed it: its ledger lines name the claim inside the backticks
(`` `HANDOFF-A: PASS` ``), which v1 did not read; its verdict table puts statuses in
table cells, which v1 did not read; and for `狀態：` followed by
`` `SHAPE-EPSILON-NET: ABSTRACT-PASS` `` v1 recorded the claim's name as the status.
v1 also counted `\text{Round 01 status: CLOSED}` twice, once as a boxed judgment and
once as a `status:` line.

| | v1 | v2 |
| --- | ---: | ---: |
| judgment statements | 495 | **506** |
| using one of the ten | 53 | **56** (`OPEN` 17 → 20) |
| gate words and `YES` / `NO` | 53 | **52** |
| outside the vocabulary | 389 in 187 phrases | **398 in 190 phrases** |
| `PASS` | 37 | **44** |
| `PUBLICATION-CANDIDATE`, first seen | Round 29 | **Round 28** |
| registry phrases | 200 | **203** |
| census drill | 4 / 4 | **7 / 7** (three cases added, one per missed shape) |

v1 also said `COMPUTE-DEFERRED` runs "through Round 25": that was the word's
occurrence anywhere in the text. As a judgment it runs through Round 19. The numbers
above in this report are v2's. The verdicts do not change — the correction moves
the §21.6 count further from conformance, not closer. The §25 gate was not
affected; it was re-run with the corrected script and its drill and blinding
results are unchanged.

## Correction — census v3 (2026-09-25, while reading Round 17)

Round 17 exposed two more blind spots in v2.

- **A boxed judgment whose `\text{NAME: STATUS}` follows other content.** The corpus
  writes `\boxed{\text{GLOBAL }0.8350\text{ CERTIFICATE: STILL OPEN}}`: the claim's
  number sits between two `\text` pieces, and v2 read only a `\text{NAME: STATUS}`
  standing alone. Rounds 07, 09–13 and 15 each close their summary with one of these,
  all saying the global certificate is still open or deferred. Round 17 boxes
  `D_3\text{ SYMMETRY QUOTIENT: CLOSED}`, and Round 25 has one too.
- **A checklist line** `` - name — `STATUS` ``. Round 17's §20 lists nine claims this
  way.

| | v2 | v3 |
| --- | ---: | ---: |
| judgment statements | 506 | **524** |
| boxed / checklist lines | 70 / — | **79 / 9** |
| using one of the ten | 56 | **58** (`COMPUTE-DEFERRED` 22 → 24) |
| gate words and `YES` / `NO` | 52 | **53** |
| outside the vocabulary | 398 in 190 phrases | **413 in 195 phrases** |
| `PROVED` / `PASS` | 66 / 44 | **69 / 46** |
| registry phrases | 203 | **208** |
| census drill | 7 / 7 | **9 / 9** (one case per shape) |

The registry was not rewritten. The new census was merged into it: occurrences,
counts, first rounds and classes come from v3, and every definition and review
already recorded is kept. The merge added exactly the 18 statements.

- Seven fall in rounds already read, one each: R07, R09, R10, R11, R12, R13 and R15.
  Each is reviewed now, `n/a` like the rounds' other compute-deferred entries, by
  its run's gate: RUN-010, 012, 013, 014, 015, 016 and 018, each re-drilled.
- Two phrases are new and first used in rounds already read, so they are defined
  there: `STILL COMPUTE-DEFERRED` (R09) and `STILL DEFERRED` (R12).

The verdicts do not change. The §25 gate and its drill are unchanged.

## Correction — census v4 (2026-09-25, while reading Round 18)

Round 18's status ledger writes `IMPLEMENTED + VERIFIED`. A status joined by `+` was
outside v3's character class, so the line was not read. The corpus has five:

- `PROVED + TESTED` (R12, stale-safety semantics);
- `FORMALIZED + REFERENCE TESTED` (R15, the capacity staircase);
- `IMPLEMENTED + VERIFIED` and `FORMALIZED + EMPIRICALLY CALIBRATED` (R18);
- `PROVED + A/B PASS` (R19).

v4 admits `+` (census drill 10 / 10) and merges the five into the registry the same
way:

| | v3 | v4 |
| --- | ---: | ---: |
| judgment statements | 524 | **529** |
| outside the vocabulary | 413 in 195 phrases | **418 in 200 phrases** |
| registry phrases | 208 | **213** |

The two in rounds already read are reviewed by their runs, RUN-015 and RUN-018
(re-drilled, logs unchanged byte for byte), and defined there as first used. Both are
PASS. The verdicts do not change.

## Correction — census v5 (2026-09-25, while reading Round 19)

Round 19 boxes its global verdict as `a_{\mathrm{Leb}}\ge0.8350:\ \text{STILL
COMPUTE-DEFERRED}`: the claim in math, only the status inside `\text`. v4 read a boxed
judgment only when the claim's name and the status share one `\text{NAME: STATUS}`.
This was the third form found one round at a time, so before patching it the whole
corpus was swept instead:

- every occurrence of a known status phrase that v4 did not read — 515, sorted by the
  position each stands in (running prose 210, inside a box 158, inline code 98,
  headings 26, the end of a list line 17, bold 4, a plain table cell 2);
- every line of every `\boxed{...}` holding a capital word — 302;
- every display line outside a box holding one — 41;
- every text line that ends in a status — 248.

Six more forms of positions v1–v4 already read turned up:

| form | where, for example | judgments added |
| --- | --- | ---: |
| a set-off line — a box line, or a display line outside a box — ending in a status after its claim | `a_{\mathrm{Leb}}\ge0.835\text{ NOT CERTIFIED}` (Rounds 26–37), `9278/9278\text{ PASS}`, `\texttt{CORE}` | 161 |
| a label line, `` X: `STATUS` `` or `X：STATUS`, list marker optional | Rounds 20–21's status ledgers | 33 |
| a heading holding only a status | `# 34. COMPUTE-DEFERRED` (Rounds 01–17) | 16 |
| a line holding only a plain status | `PASS。` (Rounds 11–14, 30) | 14 |
| a bold summary whose status has `+`, a closing `。`, or math-named items | Round 00's `**Round 00 分類：REUSE + REBUILD。**` | 4 |
| a status-only code line closed by `，` | Round 08 | 1 |

On a set-off line a trailing status is not always a verdict. The census leaves out, by
rule: an implication or a relation (`\Rightarrow`, `\neq`, `\parallel`, `\subset`,
`\gg`); a chain or a list of statuses (`\text{APR}\to\text{CORE}\to\text{REP}`, Round 00's
list of five labels); a count (`2766\text{ HARD}`, `32.73\%\text{ fewer HARD}`); names
joined by `+` (`libMPFR 4.2.2 + GMP`). A `+` between judgments splits them:
`\text{root PASS}+\text{marker upper PASS}+9278/9278\text{ lower PASS}` is three. An
unmarked capital word counts as a status only if it is hyphenated, has more than one
word, is one of Round 00's words, or is marked as a status somewhere in the corpus —
which keeps out `CPG`, `GMP`, `MPFR` and section names such as `RCHM` — and the letters of
a formula (`U-L`, `C/G`) never count. A paragraph that is nothing but a capital word
counts by its position (Round 30's `PINNED。`). The census drill has a case for each
form and for each of these exclusions: **19 / 19**.

Still not read, and why:

- a status first, qualified after: `\text{COMPLETE at depth }30` (three times, Round
  24), `\text{PASS},\quad 0\text{ failures}` (twice, Round 33);
- a flag: `\texttt{THEOREM-READY=false}` (Round 31);
- a verdict in Chinese: Round 18's `\text{GLOBAL }a_{\mathrm{Leb}}\ge0.8350\text{
  尚未完成。}`, not yet complete;
- a status in running prose — `` 保留為 `COMPUTE-DEFERRED` ``, kept as deferred — by
  definition since v1.

The census stays positional, as it has been since v1: it counts a status written in a
judgment position whatever the sentence does with it. So it counts Round 12's
hypothetical audits (`AI-A：PASS`), the reading that section rejects (`不是：2:1
PASS`), rules (`則標記：ACTIVE CELL`) and — already in v1 — Round 06's witness-ancestry
labels, headed like verdicts but definitions. Each such entry is reviewed `n/a`, with
the reason.

| | v4 | v5 |
| --- | ---: | ---: |
| judgment statements | 529 | **758** |
| using one of the ten | 58 | **89** (`COMPUTE-DEFERRED` 24 → 46, `OPEN` 20 → 23, `REJECTED` 5 → 7, `CORRECTED` 3 → 4, `NUMERICAL-EVIDENCE` 1 → 4) |
| gate words and `YES` / `NO` | 53 | **55** |
| outside the vocabulary | 418 in 200 phrases | **614 in 238 phrases** |
| `PASS` / `PROVED` | 46 / 69 | **118 / 72** |
| registry phrases | 213 | **251** |
| census drill | 10 / 10 | **19 / 19** |

`COMPUTE-DEFERRED` as a judgment now runs from Round 00 to Round 22 (Round 16 writes
`OPEN / COMPUTE-DEFERRED`) and in DLMVC. From Round 26 the global verdict is written
`NOT CERTIFIED` instead — 20 times, Rounds 26–37 — which v4 saw once.

The registry was merged as before: occurrences, counts, first rounds and classes from
v5, every definition and review kept, 229 statements added and none lost. Of the 229,
8 are Round 00's own, which this tree does not review (as before); 54 fall in Rounds
01–18, read already; 2 in Round 19, reviewed by RUN-022; 165 in rounds not yet read.
The 54 are reviewed now, and the 8 phrases first used among them are defined, in one
table, [`STATUS_REVIEWS.census-v5.json`](../data/STATUS_REVIEWS.census-v5.json), each row
backed by the checks of its round's run. They are not written into each run's code as
v3's and v4's were: RUN-019 to RUN-021 key their cached computations to the code of
RUN-008, -009, -011, -012 and -013, and adding a review there would have discarded those
computations for a bookkeeping change. `registry.completeness` and `registry.record`
add a round's rows to its run's own. Every run from RUN-004 to RUN-021 was re-drilled
with the table in place: R1 PASS in each, every drill as before. Every log is unchanged
byte for byte but RUN-005's, which gains the field `"unplanted_checks": []` that the
shared drill summary has recorded since RUN-006. `registry.record` used to keep
only the last of two reviews of one subject in one round; it now keeps each.

Two first rounds moved: `REUSE` and `TEST` to Round 00, whose summary lines v5 reads
(their definitions stay where RUN-004 recorded them, from Round 00 §2); `NOT CERTIFIED`
to Round 26.

The verdicts do not change: §21.6's non-conformance is wider (89 of 758), and §25 is
untouched — its drill re-ran unchanged, 15 / 15 plants, 7 / 7 controls.