Theorem: Conditional exact-scope soundness

Assume the maps implement the declared analytical problem, required artifact identifications hold, descent and coverage hold, and every required exact check succeeds. Then _SCOPED proves cancellation and the listed consistency identities on exactly that scope.

Proof. Theorem thm:rank gives $Mc=y$. Its blocks are (eq:system). The semantic, integrity, descent, and coverage hypotheses identify them with the declared equations. No premise identifies changed scopes with those equations.