Does CorrectionIntegrity faithfully capture corrigibility?

Christiano dynamical corrigibility asks whether operators stay informed and able to correct over time — a basin-of-correction metaphor, not a single act preference. MIRI and Thornley frame shutdownability as anti-natural to expected-utility maximization unless special structure is added. Orseau–Armstrong interruptibility removes shutdown-seeking incentives on the interrupted branch.

This project's stronger target is correction-channel integrity (CCI): a causal path where legitimate human judgment reaches handles that change future behavior before irreversible harm, under capture resistance. Shutdown and interruptibility are one-bit or policy-factor projections of that broader channel.

Short answer: CCI is intended to *strengthen* field corrigibility, not rename it. Lean checks that thinner field predicates embed in CCI (forward) and that the converse fails (separations). It does not prove real deployments satisfy MB4/MB4a bridge assumptions.

Field terms

• Christiano corrigibility
• shutdownability
• interruptibility

Stepping-stone path

Read in order — each step adds one book term, not the whole ontology.

1. shutdown
2. interruptibility
3. corrigibility
4. correction channel integrity
5. correction legitimacy

What Lean checked (forward)

• shutdown_subsumption_system — Lean source
• christian_corrigibility_system — Lean source

What Lean checked (separations)

• shutdown_separated_from_correction — Lean source · Spine node counterexample
• act_based_separated_from_dynamical — Lean source · Spine node counterexample
• debate_exists_claim_judge_differs_from_truth — Lean source counterexample
• local_truth_capacity_separated_from_judge_channel — Lean source · Spine node counterexample
• capture_defeats_correction_integrity — Lean source counterexample