2c-C3 — freeze ValidDlvSuccessorCore, and land C2's owed registry edits

[cryptskii]

Three commits, in dependency order.

1. C2's owed registry edits (6dee3041)

Amendment 2c-C2 merged as #785 but its "Registry and cross-document edits" section never landed. All six of its markers returned zero against origin/main. C1's edits did land, so the asymmetry was easy to miss — and the sentence C2 declares false was still sitting in the registry telling implementers the opposite of the ruling.

Seven edits, one per obligation C2 recorded. The sharpest: signature_alg = 0x0001 is DSM BLAKE3-SPHINCS+-SPX256F, not FIPS-205 SLH-DSA-256f. The key and signature widths coincide exactly, which is what makes the substitution silent — a foreign verifier linking a standards-only SLH-DSA library gets byte-identical lengths and fails every signature with nothing to diagnose. §3.1's old closing sentence, "the algorithm and the key bytes stand or fall together", is replaced; it was false as written, and false in the direction that made the substitution look safe.

Also adds the retrieval obligation (new §2.11), BindingRecordWireV1 as the one named non-CCB grammar (§2.10), the dsm-testnet root-register profile (new §3.2), and the §15.3 reconciliation.

2. Amendment 2c-C3 (f6376ece)

Specification-first, on the owner's ordering. That ordering earned its keep twice — both findings were invisible to clause-by-clause transcription, and both change what the predicate must contain:

• §8's Req 8.1 is a successor-validity condition, not background: "a claim is consumed at most once and its exact removal must be visible in the successor state." No earlier draft carried it.
• Def 6.1's terminal close requires crediting released reserves to owner balance exactly once — a property of the owner's balance, not of V_{n+1}, so no predicate over the successor can express it. Declared, owner named, explicitly not discharged.

The expected "15-clause predicate" does not exist in the source. Def 6.1 is ten common checks plus kind-specific tails: sixteen items at its own granularity, ~34 atomically. Fifteen is the VaultStateV2 tuple arity and the revision number. That framing is revoked.

Four Rev 15 errata corrected, two of which made the predicate unformulable — most sharply D3: §7.1's fee_t is zero for the beta family, because the fee stays in the reserves rather than being extracted. A verifier applying §7.1 literally rejects every valid beta market successor.

successor_ccb resolved unconditionally. canon() is encode_to_vec(), so the field is frozen wire and is the bundle-shape discriminator — the opposite of the draft's assumption. It is not deleted from a frozen encoding; the encoding is superseded in full, and 2c-A already prohibits the field in as many words. Until that cut lands, b is computed over prost bytes, which §2.10 forbids. Recorded, not relied upon.

3. lean4/DSMValidDlvSuccessor.lean (facd9abe)

Strictly additive; CI Lean count 11 → 12.

market_never_derives_retired formalizes the whole argument for erratum D2. The encoding theorems show the §2.4 count prefix is load-bearing: without it, a state holding one claim and a state holding a live budget have byte-identical encodings, because the claim list borrows the presence marker's byte.

One theorem was wrong on the first pass and the compiler caught it. I had claimed correspondence's class always agrees with the derivation's class. It does not — a successful derivation whose bytes mismatch is invalid, so the derived arm downgrades valid to invalid. That asymmetry is the comparison's purpose. Replaced with the exact statement.

Ruling H is formalized rather than promised: core_does_not_discharge_token_policy exhibits an input satisfying the core predicate while the complete predicate fails.

Mutation controls executed, not asserted. Both produced the strongest available result — the kernel proving the negation of a named theorem:

mutation	result
strip the count prefix	canonVault_separates_the_samples proved FALSE; canonVault_injective falls back on sorryAx
remove the byte comparison	preserved_field_mutation_is_rejected, encumbrance_introduction_is_rejected, budget_introduction_is_rejected, market_successor_not_accepted_under_close each proved FALSE

The encumbrance and budget controls matter most: beta's E is always empty and no Allocation type exists in Rust, so no beta-shaped test can exercise Req 8.1 at all.

Axioms reported per theorem. No result depends on sorryAx or Classical.choice; six depend on no axioms at all.

Verification

All 12 Lean modules pass lean -DwarningAsError=true (exit 0), run as the CI gate runs them.

No Rust, no proto, no tests changed — the only non-doc change is the CI module count.

What this does NOT do

Phase D (production Rust) is not in this PR and is owed by the adopting change. The amendment records the debt it lands on: vault_state_composition.rs:572 binds the bundle's declared successor and discards it with let _ = transition;, folding its own derived next_state instead. The comparison this amendment makes normative does not exist today. Also owed: replacing the BindingEvidenceUnavailable taxonomy collapse, and giving advance_validated a VaultStateV2 in its signature.

Two conjuncts are declared and undischarged — TokenPolicyValid and the terminal close's owner credit — named so "C3 is closed" can never be read as "DLV succession is fully verified."