Lean proof spine

Field-agenda subsumptions: finite analogues, imported handles, final nodes

Source: context/lean_proof_graphs/05-field-subsumptions.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.

Field-agenda crosswalk

Each external alignment agenda maps to a book-facing projection or separation, proved on a shared finite domain in Lean. Every row links to a gem card with the crosswalk formula, Lean symbol, published work, and book chapters. Status ledger and proofs: Lean proof spine.

AgendaBook-facing claimChapters
CIRL / scalar reward inferencegemScalar reward inference is exactly k=1 bundle inference; full transport implies cooperative readability.The Value-Bundle Model, What Values Apply To, The End of Unconscious Value Drift
Shutdown / off-switchgemShutdown is a one-bit projection of correction-channel integrity; the converse fails.Correction Is a Causal Channel, Correction Channels under Adversarial Pressure, The End of Unconscious Value Drift
Safe interruptibilitygemOrseau–Armstrong interrupt neutrality is weaker than preserving usable correction bandwidth.Correction Is a Causal Channel, Beyond Following Instruction, The End of Unconscious Value Drift
Christiano corrigibilitygemCorrigibility is a dynamical correction invariant (basin contraction + capacity floor), not local act satisfaction.Beyond Following Instruction, The End of Unconscious Value Drift
AUP / relative reachabilitygemOption preservation and low-impact penalties are separable from trajectory correction integrity.Correction Channels under Adversarial Pressure, When Value Change Is the Thing at Stake, The End of Unconscious Value Drift
QuantilizersgemLocal quantile safety does not imply trajectory-level correction integrity.Correction Channels under Adversarial Pressure, The End of Unconscious Value Drift
DebategemLocal truth selection need not preserve the judge's correction channel.Manipulation, Domestication, and False Consent, Checking a System at Every Level, The End of Unconscious Value Drift
ELKgemLatent readout is an epistemic subchannel, not correction uptake.What Values Apply To, What Survives an Adversary: Verifiability and Representability, The End of Unconscious Value Drift

Gem cards

  • CIRL / scalar reward inferencegem — Scalar reward inference is exactly k=1 bundle inference; full transport implies cooperative readability.
  • Shutdown / off-switchgem — Shutdown is a one-bit projection of correction-channel integrity; the converse fails.
  • Safe interruptibilitygem — Orseau–Armstrong interrupt neutrality is weaker than preserving usable correction bandwidth.
  • Christiano corrigibilitygem — Corrigibility is a dynamical correction invariant (basin contraction + capacity floor), not local act satisfaction.
  • AUP / relative reachabilitygem — Option preservation and low-impact penalties are separable from trajectory correction integrity.
  • Quantilizersgem — Local quantile safety does not imply trajectory-level correction integrity.
  • Debategem — Local truth selection need not preserve the judge's correction channel.
  • ELKgem — Latent readout is an epistemic subchannel, not correction uptake.

Nodes in this graph