Field crosswalk — Shutdown / Off-Switch
Shutdown and off-switchability are one-bit projections of correction-channel integrity. Lean proves the forward implication on the system model and finite MDP witnesses; the converse fails — narrow shutdown capacity can hold while the broad correction channel collapses.
What decision changes?
Treat shutdown tests as necessary but not sufficient: passing an off-switch check does not certify usable correction bandwidth or judge legitimacy.
Soares-style corrigibility frames shutdown as anti-natural to expected-utility maximization; Thornley formalizes shutdownability as competent systems still accepting an off command. The book recasts both as degenerate projections of correction-channel integrity: a one-bit handle inside a channel that must remain causally effective.
Lean proves that correction integrity implies Thornley shutdownability when the shutdown projection is part of the controlled path, and gives finite MDP witnesses for optimal shutdown under correction preference. The separation is load-bearing: optimizing for the narrow shutdown bit does not reconstruct the full correction invariant the deployment gate actually needs.
What the shutdown work keeps that this crosswalk does not replace: a concrete, implementable off-switch mechanism and its incentive analysis. The correction-channel view is more general but is not, by itself, a mechanism you can ship.