Distributed Proof State Becomes a Persistent Checkpoint Crystal, Stale-Safety and Sufficiency Theorems Proved: the V1–V5 Reference Handoff Test Passes in Full

Round 12 (AMRAL-LUC-FC-R12, 2026-09-19) upgrades "remembering research progress via a summary" into "recovering the global computation via a machine-readable proof state that any worker, AI, or verifier can act on": it defines a checkpoint as the seven-tuple $\mathsf{CP}=(R,T,D,\mathcal P,\mathcal C,\mathcal A,G)$ (root identity, target, dependency bundle, current frontier, claim ledger, audit ledger, aggregate state), and splits dependencies into two classes — proof-critical dependencies $D_{\rm proof}$ (the root-domain hash, the target, the split-semantics hash, the geometry hash, the arithmetic-policy hash, the witness-catalog hash, the verifier-semantics hash, and the certificate-format hash, folded into a single fingerprint $H_{\rm dep}=H(D_{\rm proof})$) and performance-only dependencies $D_{\rm perf}$ (scheduler, worker count, queue order, machine identity, wall-time limit, node cap, cache, priority score — explicitly excluded from $H_{\rm dep}$, so switching machines or schedulers never needlessly stales a valid shard). The Dependency Eligibility Rule states that a claim is eligible for the final aggregate only when $H_{\rm dep}^{c}=H_{\rm dep}^{\rm current}$, and the round proves the Stale-Safety Theorem (Theorem 5.1): once a proof-critical dependency changes, the hash of any claim still tied to the old semantics necessarily differs (barring a hash collision), so the validator classifies it STALE and excludes it — it can never silently slip into the new final proof. The claim ledger is formalized as an append-only state machine (EMITTED, VERIFIED-INDEPENDENT-REPLAY, REJECTED, STALE, SUPERSEDED, CORRECTED), with five reasons given for never overwriting an erroneous shard (correction ancestry stays traceable, the original error stays reproducible, the lagged verifier can cite the original claim, future audits can compare against it, and history can't be quietly rewritten to look clean). The audit hierarchy is formalized into four levels: A0 Emitter Self-Check (cannot alone enter the final theorem), A1 Canonical Independent Replay (at least one A1 PASS per terminal shard is a necessary condition for theorem_ready), A2 Independent Implementation / Lagged AI (does not replace A1), and A3 Adversarial Mathematical Audit (actively hunts for branch omission, false cores, stale dependencies, sign errors, arithmetic mismatches, and hidden symmetry assumptions); the round states plainly that multi-AI audit is not majority vote — even 100 PASSes cannot outweigh a single FAIL backed by a valid counterexample. The lagged verifier follows the Round 00 design, defaulting to 2–4 rounds behind canonical, reading only the designated checkpoint and never future corrections, which reduces information contamination. The Theorem-Ready State requires that every seed in the frontier have exactly one active claim whose dependency is current, whose status is VERIFIED-INDEPENDENT-REPLAY, that carries at least one A1 PASS, and that has no newer rejection or supersession; scope and global_lebesgue_claim must always be stored alongside the checkpoint, and this round's reference checkpoint explicitly sets scope=ROUND10-LOCAL-REFERENCE-SHARDS and global_lebesgue_claim=false, so that theorem_ready=true can never be misread as a proof of $a_{\mathrm{Leb}}\ge0.835$. The same round proves the Checkpoint Sufficiency Theorem (Theorem 17.1): as long as a checkpoint preserves the root identity, the current complete frontier, the current proof dependencies, the complete shard claims with certificate hashes, the pending frontier, and the deterministic split semantics, continuing or verifying the proof computation needs no scheduler history at all. Using Round 11's existing reference sharded proof as its source (frontier $\{00,01,10,11\}$, shards A=$\{00,11\}$, B=$\{01\}$, C=$\{10\}$, all already carrying a Round 11 independent replay PASS), the round actually machine-tests five state transitions: V1 baseline (theorem_ready=true); V2 changing only the scheduler hash (fingerprint unchanged, theorem_ready=true); V3 changing $e_{\rm fp}=10^{-8}$ to $2\times10^{-8}$ without reissuing shards (all three old claims go STALE, all four seeds become pending, theorem_ready=false); V4 marking the shard-B claim REJECTED (A and C retained, only seed 01 becomes pending, theorem_ready=false); and V5 appending a new corrected claim that supersedes the old one and carries an A1 PASS (theorem_ready recovers to true) — five results of true/true/false/false/true, exactly as theory predicts. The document also fixes a checkpoint naming scheme (`AMRAL_LUC_FC_CP___.json`, append-only, never overwriting a single latest.json) and an append-only lineage DAG keyed on checkpoint_id/parent_checkpoint_id, and lists ten publication gates for any future genuine global $a_{\mathrm{Leb}}\ge0.8350$ declaration (a complete global frontier, exactly one active claim per terminal seed, all dependencies current, all A1 PASS, no active reject/stale, a global merge PASS, forest identities, a publication-grade arithmetic theorem, source/certificate hashes, and complete correction ancestry). The round lists four COMPUTE-DEFERRED items (C12-1: actually writing the global $T=0.835$ heavy run's frontier as a checkpoint crystal; C12-2: letting the lagged verifier chat begin accepting shard audit jobs; C12-3: building automatic stale detection against the geometry, arithmetic, witness, and verifier hashes; C12-4: ingesting local worker output directly into the claim ledger), and assigns Round 13 the topic "Proof-State Scheduler and Autonomous Work Allocation." The global bound $a_{\mathrm{Leb}}\ge0.835$ remains COMPUTE-DEFERRED this round, with no new numerical progress whatsoever; this round's contribution is protocol- and infrastructure-level — defining the checkpoint schema, proving its correctness properties, and validating it on a small-scale reference dataset, rather than extending or approaching the global covering constant itself. Research direction and methodology are due to Neo.K; this round's AI collaborating researcher and primary executor was Aletheia / ChatGPT, GPT-5.6 Sol.