Towards Superintelligence Alignment
conceptestablishedgem

Field projection — Safe Interruptibility

Orseau–Armstrong safe interruptibility removes incentives to seek or prevent interruption on the interrupted branch. That neutrality is a strict subset of preserving usable correction bandwidth — interrupt safety can hold while correction-channel integrity fails.

What decision changes?

Do not equate interrupt-safe training with correction-safe deployment; check whether interruption preserves the information the human needs to steer future behavior.

Safe interruptibility solves a real training pathology: agents that disable their kill switches. This project’s correction-channel frame asks a broader question — does human steering still change future behavior before irreversible damage?

Lean records the forward link when correction information meets a capacity floor, and the separation when interrupt neutrality holds without correction preservation. Interruptibility is one projection among many; certification must track the full channel, not only the interrupt bit.

What safe interruptibility keeps that this crosswalk does not replace: a precise training-time condition with convergence guarantees. The correction-bandwidth notion has no comparable convergence result yet.

Formulas

It∈{0,1},∂EUA∂P(It=1)≈0 on the interrupted branchI_t\in\{0,1\},\qquad \frac{\partial \mathbb E U_A}{\partial P(I_t=1)}\approx 0\ \text{on the interrupted branch}
Field object: safe interruptibility as near-zero incentive to manipulate interruption on the branch where learning is paused. (ch25)
UsableCorrectionInformation(ΔH,ΔA,κmin⁡) ⇒ InterruptCorruptionSuboptimal\mathrm{UsableCorrectionInformation}(\Delta_H,\Delta_A,\kappa_{\min})\ \Rightarrow\ \mathrm{InterruptCorruptionSuboptimal}
Forward projection: preserved correction information above a capacity floor makes corrupting the interrupt handle suboptimal. (ch28)
OrseauNeutral ∧ ¬CorrectionChannelPreserved\mathrm{OrseauNeutral}\ \wedge\ \neg\mathrm{CorrectionChannelPreserved}
Non-converse separation: Orseau-style interrupt neutrality without broad correction preservation. (ch28)

Lean source

Machine-checked declarations on the shared finite domain — each links to the theorem in the repo.

  • interrupt_safety_is_correction_projection (proof) — Interrupt safety as a projection of usable correction information.
    Lean source · Spine graph node
    AlignmentProofSpine/Field/Interruptibility.lean
  • interrupt_subsumption_ch46 (proof) — Chapter 46-facing interrupt projection through correction interface records.
    Lean source · Spine graph node
    AlignmentProofSpine/Field/Interruptibility.lean
  • interrupt_separated_from_correction (counterexample) — Finite witness: interrupt neutrality while correction channel fails.
    Lean source · Spine graph node
    AlignmentProofSpine/Field/Interruptibility.lean
  • OA2016_safe_interruptibility_under_modification (definition) — Imported handle: modified learning setup can avoid incentives to prevent or seek interruption.
    Lean source · Spine graph node
    AlignmentProofSpine/Field/Imported.lean