Lean proof spine

Spine III: Correction, risk, and successors

Source: context/lean_proof_graphs/03-correction-successors.dot

Rendered with Graphviz (same sources as the book). Click a node for details; sub-spine boxes (Spine I–IV) open the matching sub-diagram.

Nodes in this graph

P23 No handle control ⇒ no correction (proof)
P24 Weakest handle capacity / CCI (proof)
P25 Obedience ≠ corrigibility (proof)
P26 Update without fixed point (proof)
P13 Risk = Control − CCI (proof)
P29 Self-control gap (proof)
P27 Successor invariant chain (proof)
P28 Missing invariant blocks safety (proof)
Syntactic tiling ≠ import-preserving transport (proof)
MB4 Correction legitimacy (bridge)
MB5 Successor audit (bridge)
MB7b (from Spine I) (bridge)
MB7c Adversarial robustness (bridge)
MB8 CEV / process convergence (bridge)
From Spine II: P22b transport (other)
From Spine I: P11 control, MB7b (other)
Exports: CCI, Risk bound, SuccessorSafe, MB7c, MB8, TrueHarm bound (MB10) (other)
FSHUT (other)
FINT (other)
FIMPACT (other)
FQUANT (other)
FDEB (other)
P25A (proof)
FELK (other)
FCORR (other)
PFORGE (other)
MB10 (bridge)