formal(2c-D): C2's models — completion ordering, composed reserve provenance, and a walk that folds only what certifies

[cryptskii]

Formal alignment for C2 (#856)

C2 changed three things the Lean tree did not yet say. This brings the models to the shipped code.

Module	What it machine-checks
DSMSettlementCompletion.lean (new, 17th)	D-f and C2-R1 point 4: the ONE completion pass the settle route and the resume share. The fence releases only after the exact receipt is at quorum and only in a certifiable pass; below quorum or uncertified it stays held; a receipt already at quorum is verified, not re-sent; a second pass changes nothing; a pass never changes b or the permitted successor (it resumes, never retries).
DSMComposedReserveProvenance.lean (new, 18th)	D-g: owner backing at one baseline generation; past it, the parent is exactly the last state of a linked, consecutive history from that baseline. Soundness, each conjunct's necessity, LP-absent generations 1 and 2, and composition that stops AT its target — so provenance of generation n never reads the state the settlement consuming n produces.
DSMAcceptedSuccessorWalk.lean	D-d: partialPendingRealization deleted. The walk folds exactly what certifies; a market successor without the 2c-D witness is not folded, and with it certifies.
DSMBundleAcceptance.lean	Banner corrected: fence release and Req 21.16 are no longer "owed"; it points at the two new modules.

Also: the CI Lean pin moves 16 → 18, and 2c-D §14's D-f and D-g name the modules that check them.

What these models do NOT claim

Certification is an input (certifiable), re-supplied every pass, never modelled here — that is the walk's and §7's. Quorum reachability is an input. commitOf is a model encoding, not vault_state_commitment. That a parent is the CURRENT frontier is the binding register's exclusivity, not the reserve rule. These are models of the normative rules, not refinement proofs from the Rust.

Mutation controls — executed

Each deletes or weakens one conjunct; the kernel then proves the named sample theorem false (decide proved the proposition false, at a line inside that theorem). Each was reverted from a byte copy and verified with cmp.

#	Mutation	Named theorem the kernel proved false
CR1	linked dropped from the reserve rule	an_unlinked_state_is_refused
CR2	ends-at-the-parent dropped	a_history_that_stops_early_provenances_nothing
CR3	generation step dropped from linkedStep	a_leaping_generation_is_refused
CR4	composeUntil no longer stops at its target	composition_for_provenance_never_reaches_the_consuming_settlement
SC1	release no longer waits for publication	below_quorum_the_sample_holds
SC2	certification check dropped from the pass	an_uncertifiable_sample_never_releases
AW2	market arm returns .valid without the witness	the_separation_is_not_vacuous

Verification

• All 18 modules: lean -DwarningAsError=true OK on the pinned v4.23.0; zero sorryAx in every axiom report.
• make lint and ci/production_safety_checks.sh not re-run: this PR changes no Rust and no TLA+ relative to e58340cf, where both passed.