# RUN-015 — Round 12: the checkpoint machinery works, but three stored aggregates contradict their ledgers and a rejected certificate comes back unchanged

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

- `MULTI_AI_AUDIT_PROTOCOL_v0.1.md`, `CHECKPOINT_SCHEMA.json`, `VALIDATION.json`, `State_Crystal`;
- the reference checkpoints `v1` … `v5` and `state_transition_summary.json`;
- the copies of Round 11's shard files;
- `checkpoint_validator.py` and `state_transition_demo.py`, read only after this tree's reconstruction, and never run.

**Tools:** [`run015_round12_checkpoint_crystal.py`](../code/run015_round12_checkpoint_crystal.py) — this tree's own checkpoint validator; the digests re-derived; `jsonschema`
**Logs:** [`run015-round12-checkpoint-crystal.json`](../data/gate-logs/run015-round12-checkpoint-crystal.json)

**Verdict: PASS for the mechanics; PARTIAL for the aggregate and the correction semantics.**

- Round 12 stores the distributed proof state itself. A checkpoint holds:
  - the root and the target;
  - a bundle of proof-critical dependency hashes and its fingerprint;
  - the frontier;
  - append-only claim and audit ledgers;
  - an aggregate.
- **The mechanics work.**
  - Every digest re-derives. Payload digests and the fingerprint are SHA-256 of
    Round 11's canonical JSON. The root-domain hash is the digest of Round 11's root
    box. The arithmetic-policy hash is the digest of
    `{mode: REFERENCE_DRY_RUN, fp_pad: 1e-8}` (`2e-8` in V3).
  - This tree's own validator reproduces the five verdicts — true, true, false, false,
    true — with the same accepted, pending, stale and rejected claims.
  - A scheduler change leaves the fingerprint, and an arithmetic change moves it.
  - On random edits every proof-critical field moves the fingerprint, no
    performance-only field does, and key order does not matter. That is the stale-safety
    theorem (Thm 5.1), resting on SHA-256.
- **Three checkpoints' stored aggregates contradict their own ledgers.**
  - V3 (every claim stale) and V4 (shard B rejected) both store `theorem_ready: true`.
  - V4 and V5 list the rejected `claim-shard-B-v1` as active.
  - The demo wrote V2–V5 by copying V1 and editing single fields, and never recomputed
    the aggregate.
  - Neither the validator nor §14's validity list compares the stored aggregate with
    the ledger. A file can say theorem-ready when it is not, and nothing flags it.
- **A rejected certificate comes back unchanged.**
  - V5's "corrected" claim is a copy of the rejected claim under a new id, with the
    same certificate bytes.
  - Its A1 PASS is a literal record the demo writes, not a replay.
  - The A2 FAIL against those bytes stays unanswered.
  - The validator decides from each claim's status field and an A1 PASS, and never
    reads a FAIL audit. So a FAIL counts only if someone also rewrites the status, and
    a fresh claim id undoes it.
  - §12 says a hundred PASSes cannot cancel one valid counterexample; this design
    cannot enforce that.

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

---

## What Round 12 claims

1. **The checkpoint** (§1–6). A checkpoint is `(R, T, D, P, C, A, G)`: root, target,
   dependency bundle, frontier, claim ledger, audit ledger, aggregate.
   - The proof-critical bundle holds eight hashes: root domain, target, split
     semantics, geometry, arithmetic policy, witness catalog, verifier semantics and
     certificate format. Their fingerprint is `H_dep`.
   - Performance-only data stays out of `H_dep`.
   - A claim is eligible only while its fingerprint is current. So a dependency change
     cannot silently carry old claims into a new proof (Thm 5.1).
   - Invalidation may later be made selective.
2. **Ledgers and audits** (§7–13).
   - Claim states: `EMITTED`, `VERIFIED-INDEPENDENT-REPLAY`, `REJECTED`, `STALE`,
     `SUPERSEDED`, `CORRECTED`.
   - The ledgers are append-only. Evidence is monotone; belief may revert.
   - Supersession, and an audit ledger.
   - Audit levels A0–A3. Every final claim needs an A1 PASS.
   - Not a vote: one valid counterexample outweighs any number of PASSes.
   - A lagged verifier.
3. **Readiness** (§14–21).
   - Checkpoint validity, nine items.
   - `theorem_ready`: every frontier seed has exactly one current, verified, A1-passed,
     unsuperseded claim.
   - Scope is proof-critical metadata.
   - A checkpoint with a complete frontier, current dependencies, claims, pending seeds
     and deterministic split semantics suffices to continue without scheduler history
     (Thm 17.1).
   - How rejections, corrections, proof-critical and performance-only changes
     propagate.
4. **The reference** (§22–28): five checkpoints on Round 11's shards.

   | checkpoint | change | `theorem_ready` |
   | --- | --- | --- |
   | V1 | baseline | true |
   | V2 | scheduler only | true |
   | V3 | the pad `10⁻⁸ → 2×10⁻⁸` | false |
   | V4 | shard B rejected | false |
   | V5 | an appended correction of B | true |
5. **Operations** (§29–41): naming, lineage, where audits go, claim ancestry, the stale
   aggregate, progress metrics, the production checkpoint, the publication gate,
   C12-1 … 4 deferred, Round 13's topic.

The separate audit protocol restates §11–13, §18 and §36 for auditors.

## A — sources

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

## W — rebuilt

| check | Round 12 | rebuilt | result |
| --- | --- | --- | --- |
| W1 | §2–5: digests | every payload digest, fingerprint and the recoverable dependency hashes | PASS |
| W2 | §14–15, §18–21, §28: validation | this tree's validator on V1–V5 | PASS, all five verdicts |
| W3 | §22–23: the source | the claims against Round 11's shards and merge rows | PASS |
| W4 | §12, §14, §19, §32: semantics | stored aggregates; re-admitted bytes | recorded: 3 and 1 |
| W5 | Thm 5.1 | random edits to the bundle | PASS |

**W1 — digests.** Each checkpoint's `payload_sha256` is SHA-256 of its payload in
Round 11's canonical form: sorted keys, no spaces. Each fingerprint is the same digest
of the proof-critical bundle:

| checkpoint | fingerprint |
| --- | --- |
| V1, V2, V4, V5 | `a07225d3…` |
| V3 | `57ba4912…` |

Three of the recorded hashes can be traced to their inputs:

- the root-domain hash is the digest of Round 11's root box;
- the arithmetic-policy hash is the digest of `{mode: REFERENCE_DRY_RUN,
  fp_pad: 1e-8}`, and `2e-8` in V3;
- the source merge-summary hash is SHA-256 of the file's raw bytes. That is not the
  canonical form used everywhere else, so reformatting the file would change it.

The other five dependency hashes commit to descriptors that are not in the package.
The copies of Round 11's manifest, merge summary and shards are byte-identical to
Round 11's.

**W2 — this tree's validator.** The rules, taken from §8–9 and §14–15:

- a superseded claim is history, whatever its status;
- a claim marked `REJECTED` is rejected;
- a claim whose fingerprint is not the checkpoint's current one is stale;
- a claim is accepted if it is `VERIFIED-INDEPENDENT-REPLAY` with an A1 PASS;
- a seed with no accepted claim is pending;
- `theorem_ready` needs a complete prefix-free frontier, nothing pending, nothing
  covered twice.

| checkpoint | accepted | pending | stale | rejected | ready |
| --- | --- | --- | --- | --- | --- |
| V1 | A1, B1, C1 | — | — | — | true |
| V2 | A1, B1, C1 | — | — | — | true |
| V3 | — | 00, 01, 10, 11 | A1, B1, C1 | — | false |
| V4 | A1, C1 | 01 | — | B1 | false |
| V5 | A1, B2, C1 | — | — | — | true |

This matches the package's transition summary entry for entry, and the text's table.

**W3 — the source.** The three V1 claims carry Round 11's shard digests, seed lists and
Merkle root. The three A1 audits carry its merge rows (nodes, leaves, worst slack) and
the verifier-semantics hash. Every checkpoint marks its scope local
(`ROUND10-LOCAL-REFERENCE-SHARDS`, `global_lebesgue_claim: false`).

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

| checkpoint | stored `theorem_ready` | computed | stored active claims | computed |
| --- | --- | --- | --- | --- |
| V1 | true | true | A1, B1, C1 | A1, B1, C1 |
| V2 | true | true | A1, B1, C1 | A1, B1, C1 |
| V3 | **true** | false | A1, B1, C1 | none |
| V4 | **true** | false | A1, **B1**, C1 | A1, C1 |
| V5 | true | true | A1, **B1**, C1 | A1, B2, C1 |

**The stored aggregates.** Each of V2–V5 carries V1's aggregate unchanged. A reader of
the V3 file sees `theorem_ready: true` and `REFERENCE-THEOREM-READY-WITHIN-SCOPE`, while
by the round's own rules not one claim is eligible. §14's nine validity conditions do
not include agreement between the stored aggregate and the ledger. The package's
validator computes its own and never reads the stored one. So the error is invisible
to the machinery that is meant to catch stale state.

**The correction.** In V5:

- the corrected claim for shard B carries the same certificate digest as the claim V4
  rejected;
- the FAIL audit against that claim stands, and nothing answers it;
- the new claim's A1 PASS carries no replay metrics, unlike V1's.

§19 asks a correction only to pass a current A1 audit. §32 allows unchanged bytes only
for a dependency re-verification, and this is not one. §12 says no number of PASSes
cancels a valid counterexample. Here the verifier that passed the bytes in V1 passes
them again, and they are back.

If V4's FAIL had been a real counterexample, V5 would have put a refuted certificate
back into the proof. A rejection should attach to the certificate's bytes. It should
be cleared only by an audit that answers the counterexample, or by new bytes.

**W5 — stale safety.** Change any one of the eight proof-critical fields and the
fingerprint changes; change any performance-only field and it does not. Reordering
the bundle's keys leaves it unchanged.

Thm 5.1's argument is sound, but only for what the bundle contains. What the
split-semantics hash pins cannot be checked from the package. That includes the lift
split's tie-break and child order, which RUN-013 found only in code.

## P — the package

**P1.** All five checkpoints validate against `CHECKPOINT_SCHEMA.json`. The schema
leaves claims and audits untyped, so it cannot notice either W4 finding.

The audit protocol agrees with the text in substance, with two differences:

- it uses two states the text's ledger lacks, `REJECTED-PENDING-REVIEW` and
  `STALE-AGGREGATE`;
- its publication gate lists nine of §36's ten items, dropping "source and
  certificate hashes".

**P2.** `VALIDATION.json` describes the round's document, the state crystal and the
audit protocol correctly: SHA-256, bytes, `$$` count and parity, the two flags. Its
digests of the schema, the validator and the demo match the archive. Its baseline is
the summary's V1, and its expected and obtained results are the summary's five verdicts.

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

- `state_transition_demo.py` builds V2–V5 by deep-copying a checkpoint and editing
  fields, and never touches `aggregate`, which explains W4's first finding. It builds
  V5's corrected claim with `copy.deepcopy(orig)` and a new id, and appends the A1
  PASS as a literal with the reason "append-only correction demo".
- `checkpoint_validator.py` checks the payload hash, the frontier and the fingerprint,
  and selects claims as W2 does. It never reads a FAIL audit or the stored aggregate.

## The theorems, read

| Round 12 | statement | verdict | note |
| --- | --- | --- | --- |
| §1–3 | the checkpoint; proof-critical and performance-only dependencies | PASS | W1 |
| §4, Thm 5.1 | eligibility; stale safety | PASS | SHA-256 of the canonical bundle (W1, W5); protects what the bundle contains |
| §6 | selective invalidation | n/a | described, not implemented |
| §7–10 | claim states; append-only; supersession; audit ledger | PASS | |
| §11–13 | audit levels; not a vote; the lagged verifier | PASS | the reference validator does not enforce §12 (W4) |
| §14–15 | checkpoint validity; theorem-ready | PARTIAL | no condition ties the stored aggregate to the ledger; three files contradict themselves (W4) |
| §16 | scope | PASS | W3 |
| Thm 17.1 | checkpoint sufficiency | PARTIAL | hypothesis 6 is met by a hash; a hash confirms split semantics but does not supply them, and their descriptor is not in the package |
| §18, §20–21 | rejection; proof-critical and performance-only changes | PASS | W2 |
| §19 | correction | PARTIAL | re-admits the rejected bytes on a PASS no replay produced (W4) |
| §22–28 | the reference transitions | PASS | W2 |
| §29–36 | naming; lineage; audits; ancestry; stale aggregate; progress; production; publication gate | PASS | |
| §37–41 | files; deferred runs; Round 13; checklist; handoff | n/a | |

## The status registry

Round 12's 22 judgments are reviewed, and its 8 first-used phrases defined: `TESTED`,
`STALE`, `VERIFIED-INDEPENDENT-REPLAY`, `EMITTED`, `NOT-THEOREM-READY`, `SUPERSEDED`,
`STILL DEFERRED` and `PROVED + TESTED`. Ten of the 21 are claim and aggregate states, recorded as
labels. One, §0's boxed "GLOBAL 0.8350 COMPUTE: STILL DEFERRED", was added by
census v3 (RUN-003), and one, §40's "Stale-safety semantics: PROVED + TESTED" (PASS), by
census v4 (RUN-003).
The three PARTIALs are:

- "DISTRIBUTED PROOF CHECKPOINT ABI: CLOSED" — the stored aggregates;
- "STALE / CORRECTION SEMANTICS: CLOSED" — the re-admission;
- "Append-only correction: TESTED" — the same.

| verdict | judgments |
| --- | ---: |
| PASS | 7 |
| PARTIAL | 3 |
| n/a | 12 |

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| the document's V4 row | 1 | A0 |
| the digest without sorted keys | 1 | W1, W5 |
| V1's pad read as `10⁻⁷` | 1 | W1 |
| a validator blind to staleness; V3 claimed ready in the table | 2 | W2 |
| the scope claimed global | 1 | W3 |
| the stored aggregates assumed right; the re-admission assumed absent | 2 | W4 |
| the protocol's extra states assumed in the text | 1 | P1 |
| `VALIDATION.json`'s V4 result flipped | 1 | P2 |
| a review dropped | 1 | R1 |

Four controls:

- the unmodified inputs;
- the document with CRLF line endings;
- the digest with ASCII escaping;
- the digest of a bundle with its keys reversed.

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

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

## What this round does not establish

- **Anything about the geometry.** Round 12 validates proof-state bookkeeping over
  Round 10's certificate, which RUN-013 replayed.
- **What the other five dependency hashes pin.** Their descriptors are not in the
  package.
- **A fix.** The two remedies suggested above — a validity condition tying the stored
  aggregate to the ledger, and rejections bound to certificate bytes — are this tree's
  suggestions, untested.