Remove the superseded Stateright disaster recovery model

[Amaury Chamayou (achamayou)]

Draft dependency gate

DRAFT - DO NOT MERGE EARLY. This part 3/4 PR is blocked on human review and green full migration CI for n=1,2,3 on predecessor PR #8279 at its final exact head SHA. The currently observed PR #8279 head is 88fc1f0c6c8c5a0afbcf7deb8d265da05b78b4a4; if that head changes, the full migration evidence must be rerun and pass at the new final head before this PR can merge.

Stack predecessors: #8277 (part 1/4) and #8279 (part 2/4).

Summary

This is the net-deletion transition layer after the temporary migration bridge has established bounded equivalence between the legacy Rust/Stateright model and the canonical Lean model.

It deletes exactly:

• the complete temporary lean/disaster-recovery-migration/ package;
• .github/workflows/lean-disaster-recovery-migration.yml;
• the complete legacy tla/disaster-recovery/ Rust/Stateright project, including the temporary exporter.

The scheduled Stateright job in .github/workflows/ci-verification.yml is replaced with canonical Lean verification: install the pinned toolchain, restore the Mathlib cache, build the package, check AxiomChecks.lean, and run canonical-checks.

Immutable canonical model

Every file under lean/disaster-recovery/, including the canonical model, proofs, tests, package metadata, and .github/workflows/lean-disaster-recovery.yml, has zero diff from the parent branch. This PR does not alter the code measured by PR #8279 before deleting the temporary evidence bridge.

Validation

• lake exe cache get
• lake build
• lake env lean -DwarningAsError=true AxiomChecks.lean
• lake exe canonical-checks
• scripts/ci-checks.sh
• stale-reference search for the deleted packages, Stateright, comparator, migration executables, and old Rust job: no matches
• parent diff audit: no canonical Lean, trace, C++, tests, or CHANGELOG.md changes

The next and final layer adds trace validation independently under lean/disaster-recovery-trace/.