Spine III: Correction and successors

Source: context/lean_proof_graphs/03-correction-successors.dot · Graphviz source (.dot)

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

Nodes in this graph

P23 No handle control ⇒ no correction (proof)
P24 Weakest handle capacity / CCI (proof)
Field.Interruptibility final nodes interrupt_policy_invariant_from_correction_interface interrupt_separated_from_correction (other)
Field.Impact final nodes auxiliary_reachability_preserves_correction_reachability reachability_not_correction_capacity (other)
Field.Quantilization final nodes quantile_soundness_preserves_trajectory_cci quantile_separated_from_trajectory (other)
P25 Obedience ≠ corrigibility (proof)
Field.Corrigibility final nodes christian_corrigibility_is_correction_invariant act_based_separated_from_dynamical (other)
Field.Debate final nodes debate_value_tracks_truth debate_exists_claim_judge_differs_from_truth local_truth_capacity_separated_from_judge_channel (other)
Amplification ≠ correction contraction (proof)
Field.ELK final nodes elk_readout_is_correction_projection elk_separated_from_uptake (other)
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)
forgeability_gap all-seven-green + Risk≤δ ⇏ TrueHarm≤δ (other)
MB4 Correction legitimacy (bridge)
MB5 Successor audit (bridge)
MB7b (from Spine I) (bridge)
MB7c Adversarial robustness (bridge)
MB8 CEV / process convergence (bridge)
MB10 Conserved-property signature not forged (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)