# RUN-016 — Round 13: the merge rules are sound and the race replays, but the reference merger never writes the aggregate and cannot hold two valid certificates

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-25
**Subject:** `AMRAL_Lebesgue_Finite_Closure_Round_13_Autonomous_Scheduler_v0.1.md` (AMRAL-LUC-FC-R13, dated 2026-09-19) and its package, read from the archive:

- `WORKER_MERGER_PROTOCOL_v0.1.md`, `JOB_PROPOSAL_SCHEMA.json`, `VALIDATION.json`, `State_Crystal`;
- the reference race: `issued_jobs.json`, four race checkpoints, `race_transition_summary.json`, and copies of Round 12's files;
- `reference_scheduler_merger.py`, read only after this tree's reconstruction, and never run.

**Tools:** [`run016_round13_autonomous_scheduler.py`](../code/run016_round13_autonomous_scheduler.py) — this tree's own merger; RUN-015's validator; random primitive sequences; `jsonschema`
**Logs:** [`run016-round13-autonomous-scheduler.json`](../data/gate-logs/run016-round13-autonomous-scheduler.json)

**Verdict: PASS for the merge theorems and the race; PARTIAL on the scheduler/merger ABI.**

- Round 13 lets workers propose and only a single canonical merger write. A proposal is
  merged by semantic preconditions, not by the checkpoint it started from:
  - an expansion, only of a pending terminal seed;
  - a certificate of a pending seed;
  - or a certificate of an ancestor, whose current descendants it then replaces
    (Certified Ancestor Contraction, Thm 10.1).

  Six primitives keep the frontier complete and prefix-free (Atomic Merge, Thm 20.1).
- **Both theorems hold.** On 60 random sequences of 80 primitive steps each, the
  frontier stayed complete and prefix-free, and readiness always meant a current
  accepted claim for every seed.
- **The race replays.** It is an expansion of seed 01, then a late certificate of 01,
  then a late expansion. This tree's own merger reproduces the three decisions:
  - accept the expansion;
  - accept the certificate by contracting `{010, 011}` back to `01`;
  - mark the last expansion obsolete.

  Its validator reproduces the four states (not ready, not ready, ready, ready). That
  matches the files, the summary and the text's table.
- **The ABI is incomplete in its reference.**
  - The merger writes the frontier but never the aggregate. All four race checkpoints
    carry Round 12's V1 aggregate: `theorem_ready: true`, including at the start and
    after the expansion, while seeds are pending. The protocol gives the merger sole
    authority over exactly those fields.
  - §15–16 make duplicate certification legal, with one certificate chosen as primary.
    The validator the merger uses counts a seed with two valid claims as covered twice,
    and blocks readiness.
  - The late certificate is Round 12's V5 claim, the bytes V4 rejected, re-admitted
    without an answer to the FAIL (RUN-015). The bytes themselves are sound; RUN-013
    replayed every leaf.

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

---

## What Round 13 claims

1. **Authority** (§1–6).
   - Workers never write the checkpoint; they submit immutable proposals against
     immutable jobs.
   - Leases are performance data.
   - The merger first checks hashes, the fingerprint (else `STALE-PROPOSAL`), seed
     identity and schema.
2. **Merging** (§7–19).
   - An expansion is accepted only for a pending terminal seed; otherwise it is
     `OBSOLETE-EXPANSION`, with no arbitrary rebase.
   - A certificate closes a pending seed, or contracts current descendants into a
     certified ancestor (Thm 10.1).
   - Races resolve either way. Descendant evidence is kept.
   - Rejection after contraction reopens the ancestor.
   - Multiple certificates are all kept, and the one with the least canonical claim hash
     is primary. Duplicate compute is legal.
   - Stale workers are rebased semantically.
   - A FAIL audit is checked before it rejects, and a valid counterexample dominates.
3. **Invariants** (§20–27): Thm 20.1; a single writer; a merge journal; job sources,
   priority (tail-first), caps; the worker and merger loops.
4. **The reference race** (§28–33). From Round 12's V4, two jobs on seed 01 run
   concurrently, and a third, late expansion follows:

   | step | frontier | ready |
   | --- | --- | --- |
   | start | `{00, 01, 10, 11}` | false |
   | expand | `{00, 010, 011, 10, 11}` | false |
   | late certify, contraction | `{00, 01, 10, 11}` | true |
   | late expand | unchanged | true |
5. **Governance** (§34–41): the frontier may refine and contract, while evidence only
   grows; worker-result categories; the authority split; C13-1 … 5 deferred;
   Round 14's topic.

The worker–merger protocol restates §1–20 for implementers.

## A — sources

**A0.** 10 anchors. Round 13 has no reference list.

## W — rebuilt

| check | Round 13 | rebuilt | result |
| --- | --- | --- | --- |
| W1 | Thm 10.1, 20.1 | 60 random sequences of the six primitives, 80 steps each | PASS |
| W2 | §28–33: the race | this tree's merger and validator | PASS, three decisions and four states |
| W3 | §28: the source | Round 12's V4 and V5, byte for byte | PASS |
| W4 | §1, §14–16, and the protocol's §14 | the files against the round's own rules | recorded: 4, 1, 1 |

**W1 — the theorems.** A toy proof state holds frontier paths, claims on paths and a
current fingerprint. Each step applies one of the six primitives at random:

- close a pending seed;
- expand a pending seed;
- contract the seeds under an ancestor into a certified ancestor;
- reject an active claim;
- add an auxiliary claim;
- change the fingerprint.

After every step the frontier's Kraft sum was 1, and whenever every seed was covered,
each had a current accepted claim.

Contraction is sound for a reason worth stating. In a complete frontier, the seeds
below any ancestor `p` form a complete frontier below `p`, so their Kraft sum is
`2^{−|p|}`. Replacing them by `p` changes nothing.

**W2 — the race.** This tree's merger follows §7–12 and §27. An expansion is accepted
if its seed is in the frontier and uncovered, and is obsolete if the seed is covered.
A certificate closes a pending seed, or contracts the seed's current descendants when
they form a complete frontier below it.

Run from the start checkpoint, with the late certificate taken from Round 12's V5:

| proposal | decision | frontier | ready |
| --- | --- | --- | --- |
| start | — | `00, 01, 10, 11` | false |
| `proposal-expand-01-v1` | `ACCEPT-EXPAND` | `00, 010, 011, 10, 11` | false |
| `proposal-certify-01-late-v1` | `ACCEPT-CERTIFY-ANCESTOR-CONTRACTION` | `00, 01, 10, 11` | true |
| `proposal-expand-01-too-late` | `OBSOLETE-COVERED-BY-CERTIFICATE` | unchanged | true |

This matches the orchestration ledger, the four checkpoints' frontiers, the summary and
the text's table.

**W3 — the source.** Round 13's copies of Round 12's V4, V5, validator and shards are
byte-identical to Round 12's. The start checkpoint is V4, with the same claims, audits
and dependency bundle, and V4 as its parent. The late claim is V5's
`claim-shard-B-v2-corrected`, record for record. Every race checkpoint's digest
re-derives.

**W4 — the round's rules, applied to its own files.**

- **The aggregate is never written.** All four race checkpoints carry V1's aggregate:
  `theorem_ready: true` and active `A-v1, B-v1, C-v1`. At the start, seed 01 is
  pending. After the expansion, 010 and 011 are. Afterwards, the active list names the
  rejected `B-v1` rather than `B-v2`.

  The protocol's §14 reserves `current_frontier`, `active_claim_ids`, `theorem_ready`
  and `pending_seed_paths` to the merger. The reference merger updates the first of
  these and leaves the other three as they were, the fault RUN-015 found in Round 12's
  demo.
- **The late certificate is the rejected bytes.** Its digest is that of `B-v1`, which
  V4 rejected on a FAIL audit that is never answered; its A1 PASS is V5's literal record.
  The contraction is nonetheless sound in fact: RUN-013 replayed `lift_01.bin`, and
  every leaf clears 0.835.
- **A legal duplicate blocks readiness.** §15–16 keep two valid certificates of one
  seed and select a primary by the least canonical claim hash. Add a second valid claim
  of seed 01 to the after-certify checkpoint, and Round 12's rule — mirrored in
  RUN-015's validator and read in the package's — counts 01 as covered twice. The
  checkpoint stops being ready. The selector §15 describes is not implemented.

## P — the package

**P1.** Both issued jobs validate against the job schema, and both mark their leases
`semantic: false`.

The orchestration ledger records `proposal_id`, `decision`, the seed, and the
descendants added or contracted. It lacks four of §22's six merge-journal fields:
`base_checkpoint_id`, `current_checkpoint_id_at_merge`, `reason` and
`result_checkpoint_id`.

The text names a late expansion of a certified seed twice. §12 calls it
`OBSOLETE-COVERED-BY-CERTIFIED-ANCESTOR`; §32, the protocol and the reference use
`OBSOLETE-COVERED-BY-CERTIFICATE`.

**P2.** `VALIDATION.json` describes the round's document, the state crystal and the
protocol correctly: SHA-256, bytes, `$$` count and parity, the two flags. Its digests of
the schema and the merger match the archive, and its race summary is the reference's.

**`reference_scheduler_merger.py`, read after the reconstruction.**

- `merger_expand` and `merger_certify` decide as W2's merger does.
- Both write `frontier`, `claim_ledger`, `audit_ledger` and the journal, and never
  `aggregate`.
- `merger_certify` checks the proposal's fingerprint and its relation to the frontier,
  not whether its bytes were rejected before. It appends V5's claim and V5's A1 record
  as given.

## The theorems, read

| Round 13 | statement | verdict | note |
| --- | --- | --- | --- |
| §1–6 | authority; jobs; leases; proposals; first-stage checks | PASS | |
| §7–9 | expansion and certification acceptance | PASS | W2 |
| Thm 10.1 | Certified Ancestor Contraction | PASS | the seeds below `p` have Kraft sum `2^{−|p|}` (W1) |
| §11–14 | race resolution both ways; evidence kept; rejection after contraction | PASS | W2 |
| §15–16 | multiple certificates; duplicate compute | PARTIAL | the reference validator counts a duplicate as a coverage conflict (W4) |
| §17–19 | semantic rebase; audits; counterexample dominance | PASS | as rules; Round 12's validator does not read FAIL audits (RUN-015) |
| Thm 20.1 | Atomic Merge | PASS | W1; the reference files' stored aggregates do not follow it (W4) |
| §21–27 | single writer; journal; jobs; priority; caps; loops | PASS | the reference journal omits four fields (P1) |
| §28–33 | the reference race | PASS | W2, W3 |
| §34–37 | why it matters; monotonicity; categories; authority | PASS | |
| §38–41 | deferred runs; Round 14; checklist; handoff | n/a | |

## The status registry

Round 13's 17 judgments are reviewed, and its 6 first-used phrases defined:
`COUNTEREXAMPLE-CANDIDATE`, `EXPANSION-CANDIDATE`, `OBSOLETE-EXPANSION`,
`PROOF-CANDIDATE`, `SEARCH-CANDIDATE` and `STALE-PROPOSAL`. Seven of the 17 are
worker-result categories and proposal labels, recorded as such. One, §0's boxed
"GLOBAL 0.8350 HEAVY COMPUTE: STILL DEFERRED", was added by census v3 (RUN-003). The PARTIAL is
"AUTONOMOUS SCHEDULER / MERGER ABI: CLOSED", for W4's aggregate and duplicate findings.

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

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| the document's late-expansion row | 1 | A0 |
| a contraction that keeps one descendant | 1 | W1, W2 |
| the text's table with the expansion ready | 1 | W2 |
| the race summary with the expansion ready | 1 | W2, P2 |
| the race started from V1 | 1 | W3 |
| the stored aggregates assumed right; duplicates assumed harmless | 2 | W4 |
| the merge journal assumed complete | 1 | P1 |
| the merger's recorded digest | 1 | P2 |
| a review dropped | 1 | R1 |

Four controls:

- the unmodified inputs;
- the document with CRLF line endings;
- the contraction written as a filter;
- the issued jobs in reverse order.

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

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

## What this round does not establish

- **Races beyond the one run.** Duplicate certification, expand against expand,
  certify against a failing audit, and a dependency change mid-run are Round 13's own
  C13-5.
- **Any geometry.** The race reuses Round 10's certificate for seed 01.