# RUN-014 — Round 11: the frontier theorems hold and the reference shards merge, but the digests and boxes cannot be rebuilt from the text, and the depth forecast is not a bound

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-25
**Subject:** `AMRAL_Lebesgue_Finite_Closure_Round_11_Global_Shards_v0.1.md` (AMRAL-LUC-FC-R11, dated 2026-09-18) and its package, read from the archive: `GLOBAL_SHARD_SPEC.json`, `VALIDATION.json`, `State_Crystal`, and the reference shards (`global_manifest.json`, `shard-A/B/C.json`, `merge_verification_summary.json`, a copy of Round 10's certificate). The two shard scripts were read only after this tree's reconstruction, and never run.
**Tools:** [`run014_round11_global_shards.py`](../code/run014_round11_global_shards.py) — random frontiers and forests; RUN-013's base leaves and replay; the digests re-derived; Mishra's repository at the commit his paper pins
**Logs:** [`run014-round11-global-shards.json`](../data/gate-logs/run014-round11-global-shards.json); snapshot [`round11-repository.json`](../data/external/round11-repository.json)

**Verdict: PASS, with one mischaracterized forecast and one gap in the specification.**

- Round 11 recasts the proof state as a complete prefix-free frontier of seed boxes.
  Its four `PROVED` hold, tested on random frontiers:
  - the frontier covers the root (Thm 4.1);
  - a seed may be replaced by its children at any time (Thm 5.1);
  - shards that partition the frontier can be verified separately and merged
    (Thm 8.1);
  - a forest of `S` roots has `N = 2L − S` nodes, also after resharding.
- **The reference shards are Round 10's certificate, regrouped.**
  - The three shards partition the frontier `{00, 01, 10, 11}`.
  - Their seed boxes are Round 10's base leaves, to the last bit, and their
    certificates are Round 10's bytes.
  - Every count checks, per shard and in total (`2·5688 − 4 = 11372`).
  - RUN-013 replayed every leaf of those certificates.
- **Mishra's code, read at the pinned commit, is as Round 11 describes it.**
  `verifyB.py` checks `2L − nseed = nodes`, the family-B emitter's default seed depth
  is 22, and `certgen.py` re-queues each task's unfinished DFS stack.
- **The gap.** Round 10 set this round the task of letting "a second AI verify a shard
  alone". The digests re-derive, but only by trial:
  - the payload hash is SHA-256 of compact JSON with sorted keys;
  - the Merkle root hashes sorted raw digests pairwise and pairs an odd node with
    itself.

  Neither the text nor the spec says so. With RUN-013's tie-break and child order,
  that makes four rules a second verifier must read out of code. The reference
  manifests also carry none of §30's policy hashes.

  Pairing an odd node with itself means that repeating the largest shard leaves the
  root unchanged. §22's "exactly once" check catches that case; the root alone does
  not.
- **The forecast (§19) is not an upper bound, as claimed.**
  - §19 calls `r_pred` a "theorem-derived upper-depth forecast" from a cell's centre
    margin.
  - At the global `0.835` root, the centre's margin is `4.0×10⁻³`, so the forecast is
    9 cycles.
  - The root contains Mishra's seed, whose base area 0.8347809 is below 0.835, so no
    depth closes the cells around it on the base alone.
  - This is the loose wording RUN-012 found in Round 09's 結論 J, built on.
  - It is harmless: §20 uses the forecast only to schedule.

Drill: 13 / 13 plants caught by exactly the named checks, 4 / 4 controls undisturbed,
155 / 155 must-stay-green assertions held. Each of the ten checks was blinded in turn,
and each was reported blind in exactly as many cases as plants name it.

---

## What Round 11 claims

1. **Frontiers** (§1–6).
   - Seeds are binary paths from the root.
   - A frontier is prefix-free, and complete when every descent from the root meets it.
   - A complete frontier covers the root (Thm 4.1).
   - Replacing a seed by its two children keeps the frontier complete (Thm 5.1), so an
     interrupted worker returns a frontier instead of a failure.
2. **Shards** (§7–13).
   - A partition of the frontier into shards proves the root when every seed is proved
     (Thm 8.1); order and workers are irrelevant.
   - `N = 2L − S` for the forest; resharding changes `S` and nothing else.
   - Shards are bound by SHA-256 of a canonical payload and by a Merkle root.
3. **Identity and the global root** (§14–20).
   - Seeds are identified implicitly (Mode A) or by explicit axis/side paths (Mode B,
     recommended).
   - Exact dyadic boxes.
   - The `0.835` root.
   - Seeding with a modest depth rather than Mishra's 22.
   - Work caps.
   - A depth forecast from Round 09 (§19), and scheduling.
4. **States and merge** (§21–24): `COMPLETE`, `EXPANDED`, `FAILED`; a thirteen-item
   merge checklist; multi-AI replay; ancestry.
5. **The reference** (§25–29): Round 10's four leaves in three shards (`{00, 11}`,
   `{01}`, `{10}`), replayed and merged as "REFERENCE-SHARDED-VERIFIED", local in
   scope.
6. **Specifications** (§30–39): minimum manifest fields, checkpoints, why sharding is
   sound, arithmetic and version policy, C11-1 … 5 deferred, Round 12's topic.

Round 11 has no reference list. It describes Mishra's code three times (§10, §17,
§18); X1 reads that code.

## A, X — sources

**A0.** 25 anchors.

**X1 — Mishra's repository, at `da956b1`.**

| Round 11 | the repository | |
| --- | --- | --- |
| §10: Mishra's verifier audits `2L − n_seed = N` | `verifyB.py`: `if 2*leaves - nseed != nodes:` | ✓ |
| §17: Mishra seeds at depth 22, `2^{22}` seeds | `certemitB.py`: the depth argument defaults to 22 | ✓ |
| §18: `certgen.py` re-queues an unfinished DFS stack | `certgen.py`: each task "returns its unfinished DFS stack, which is re-queued" | ✓ |

## W — rebuilt

| check | Round 11 | rebuilt | result |
| --- | --- | --- | --- |
| W1 | §2–5, §8: frontiers | 200 random frontiers; the boxes of 20 of them, with random 3-shard partitions, against 400 random root points each | PASS |
| W2 | §10–11: forests | 200 random forests, each resharded by a cut | PASS |
| W3 | §25–28: the reference | the frontier, the partition, boxes, bytes, counts; RUN-013's replay | PASS |
| W4 | §12–13: binding | every payload digest and the Merkle root re-derived | PASS, by trial |
| W5 | §19: the forecast | the global root against the seed inside it | not an upper bound |

**W1 — frontiers.** A finite prefix-free set of paths is complete exactly when its
Kraft sum `Σ 2^{−|p|}` is 1. Two hundred frontiers were grown by random replacements.
Each passed both this test and the text's own descent definition, read literally.

Replacement keeps the sum at 1, since `2^{−|p|} = 2 · 2^{−|p|−1}`. For 20 of the
frontiers, the seed boxes were built by halving in a fixed axis order. Each of 400
random root points lay in some box, and in some shard of a random three-way partition.

**W2 — forests.** In 200 random forests of 1–7 trees, the nodes, counted directly as
the prefixes of the leaves, equal `2L − S`. Cutting a tree at a random depth and
promoting the subtrees below the cut to roots keeps the identity, with `S` grown by
the number of new roots less one (§11).

**W3 — the reference shards.**

| shard | seeds | nodes | leaves | `2L − S` |
| --- | --- | ---: | ---: | ---: |
| A | `00`, `11` | 5686 | 2844 | 5686 |
| B | `01` | 2853 | 1427 | 2853 |
| C | `10` | 2833 | 1417 | 2833 |
| all | 4 | 11372 | 5688 | 11372 |

- The frontier `{00, 01, 10, 11}` is complete, and the shards partition it.
- Each seed's box, as the shard lists it, is RUN-013's base leaf of the same name,
  bit for bit.
- The copies of Round 10's certificates are byte-identical to Round 10's and match its
  manifest.
- The merge summary's rows are the counts above. Each worst slack is the least of its
  seeds' in Round 10's summary.
- RUN-013 found no failing leaf in any of the four certificates.

**W4 — the digests.** Every payload digest (three shards, and the global manifest's
own) is SHA-256 of the payload written as JSON with sorted keys and no spaces. The
Merkle root takes the three shard digests sorted, as raw bytes: each parent is
SHA-256 of its two children's bytes, and an odd node is paired with itself.

Neither the text ("canonicalize", "binary Merkle root") nor the spec states either
form. Two other natural readings do not reproduce the recorded root: promoting the odd
node, and hashing hex strings. The rules were found by trial, and the package's
scripts, read afterwards, use exactly them.

Pairing an odd node with itself has a known consequence. The three digests and the
same three with the largest repeated have one root. So the root does not bind the
number of shards. §22's "every seed exactly once" is the check that catches a repeat,
and the package's merge verifier makes it.

**W5 — the forecast.** §19 predicts the refinement depth of a cell from its centre's
representative margin, `r_pred = ⌈log₂(S(C)/τ⋆(m, T))⌉`, and calls it a
"theorem-derived upper-depth forecast". At the global `0.835` root:

- the centre (all bodies at the origin, `φ_5 = π/5`) has base area 0.8389855, a
  margin of `3.99×10⁻³`;
- so `S_0 = 0.6101` and `r_pred = 9` cycles;
- but the root contains Mishra's seed `q†`, with base area 0.8347809 < 0.835.

Every cell around `q†`, at every depth, contains a placement whose base hull is below
the target, so none can close on the base alone. Nine cycles is no bound. Round 09's
depth theorem needs `m` to bound the margin of every representative the refinement
meets, as its §26 says. A single centre's margin does not; RUN-012 noted that 結論 J's
wording was looser than its proof, and §19 builds on the wording. §20 uses the forecast
only to order work, so nothing unsound follows.

## P — the package

**P1 — the spec and the reference manifests, against the text.** The spec's target
and shard states agree with §21, and it prefers §14's Mode B. Three gaps against the
text:

- **The spec's merge checks.** They list eleven of §22's thirteen. The two missing are
  the global manifest's own hash and target-and-policy agreement. The package's merge
  verifier does check the global hash.
- **Shard fields (§30).** The reference shard payloads have no `program_id`, `round`,
  `root_domain_hash`, `split_policy_hash`, `arithmetic_policy_hash`,
  `witness_catalog_hash`, `shard_status`, or per-seed `worst_slack`. They carry each
  seed's box explicitly, which serves as its box identity.
- **Global fields (§31).** The global manifest has no `proof_policy_version` and no
  `verifier_requirements`. It carries the root domain explicitly.

The missing `split_policy_hash` is the gap RUN-013 found: nothing in either round's
manifests fixes the lift split's tie-break or child order.

**P2.** The package's description of its document, state crystal and spec matches the
archive, and its copy of the merge summary is the reference's.

**The scripts, read after the reconstruction.**

- They compute the digests exactly as W4 found: `sort_keys=True`,
  `separators=(",", ":")`, and a Merkle layer that appends its last node when odd.
- The merge verifier checks, in order:
  - the global hash, the frontier's completeness (by descent), and seed uniqueness
    and partition;
  - the seed boxes (exact tuples) and the certificate hashes;
  - the per-shard and global identities, and the Merkle root.
- It delegates every leaf to Round 10's verifier, which it calls "already
  independent". RUN-013 found that verifier's core code to be the emitter's,
  transcribed, so the independence of the whole chain rests on the hull routine and
  on outside replays such as this tree's.

## The theorems, read

| Round 11 | statement | verdict | note |
| --- | --- | --- | --- |
| §1–3 | seed paths; prefix-free; complete | PASS | complete iff the Kraft sum is 1; W1 checks both definitions |
| Thm 4.1 | complete-frontier coverage | PASS | induction on the frontier tree; W1 |
| Thm 5.1 | frontier replacement | PASS | the Kraft sum is unchanged; W1 |
| §6–7 | resume; shards | PASS | |
| Thm 8.1 | shard partition | PASS | only "no missing seed" matters for soundness; W1, W3 |
| §9 | order is irrelevant | PASS | |
| §10–11 | forest identity; reshard identity | PASS | W2; Mishra's verifier checks the same (X1) |
| §12–13 | content address; Merkle binding | PASS | W4; both forms only in code; a repeated largest shard keeps the root |
| §14–15 | seed identity; dyadic state | PASS | the reference uses Mode A with explicit boxes |
| §16–18 | the global root; seeding; work caps | PASS | X1 |
| §19 | the depth forecast | FAIL | not an upper bound: 9 cycles at a root that contains `q†` (W5); harmless, since only scheduling uses it |
| §20–24 | scheduling; states; merge checklist; multi-AI; ancestry | PASS | the spec lists 11 of the 13 merge checks (P1) |
| §25–29 | the reference sharding | PASS | W3, W4 |
| §30–32 | minimum fields; checkpoints | PARTIAL | the reference manifests omit most of them (P1) |
| §33–36 | soundness; reshard example; arithmetic; versions | PASS | |
| §37–40 | deferred runs; Round 12; checklist; handoff | n/a | |

## The status registry

Round 11's 18 judgments are reviewed, and its 6 first-used phrases defined:
`IMPLEMENTED`, `COMPLETE`, `EXPANDED`, `ACTIVE/HARD`, `FAILED` and
`GLOBAL-CERTIFICATE-CANDIDATE`. Eight of the 18 are shard and ledger states, recorded
as labels. One, §0's boxed "GLOBAL 0.8350 HEAVY RUN: COMPUTE-DEFERRED", was added
by census v3 (RUN-003). The PARTIAL is the "SHARDED CERTIFICATE ARCHITECTURE: CLOSED" of §0: its
theorems hold, but a second verifier cannot rebuild the digests or the lift boxes from
the text and manifests alone.

| verdict | judgments |
| --- | ---: |
| PASS | 7 |
| PARTIAL | 1 |
| n/a | 10 |

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| the document's shard-B identity edited | 1 | A0 |
| Mishra's seed depth as 20 | 1 | X1 |
| a replacement that drops a child | 1 | W1 |
| the forest identity for a single root | 1 | W2, W3 |
| a seed listed in two shards | 1 | W3, W4 — the global manifest's own digest no longer matches |
| the text's leaf count for shard A | 1 | W3 |
| the canonical form without sorted keys; the Merkle odd node promoted | 2 | W4 |
| the forecast claimed an upper bound | 1 | W5 |
| the reference's shard fields assumed complete; the spec's merge checks assumed complete | 2 | P1 |
| the spec's recorded digest | 1 | P2 |
| a review dropped | 1 | R1 |

Four controls:

- the unmodified inputs;
- the document with CRLF line endings;
- the forest identity written as `L + (L − S)`;
- the replacement written as a set comprehension.

**13 / 13 plants, 4 / 4 controls, 155 / 155 must-stay-green assertions; no check
without a plant.**

| check blinded | cases reported blind | plants naming it |
| --- | ---: | ---: |
| A0 | 1 | 1 |
| X1 | 1 | 1 |
| W1 | 1 | 1 |
| W2 | 1 | 1 |
| W3 | 3 | 3 |
| W4 | 3 | 3 |
| W5 | 1 | 1 |
| P1 | 2 | 2 |
| P2 | 1 | 1 |
| R1 | 1 | 1 |

## What this round does not establish

- **Anything global.** The reference is Round 10's local box, regrouped; Round 11 says
  the same.
- **That a second verifier could work from the specification alone.** Four rules it
  would need are only in code: the tie-break, the child order, the canonical JSON form
  and the Merkle odd rule.
- **The forecast's usefulness.** It was tested only at the root, where it fails as a
  bound; as a scheduling heuristic it is untested.