Towards Superintelligence Alignment

Lean dependency spine

Field-agenda crosswalk

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

Overview of existing formalizations

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 tags follow Lean's FieldResultStatus ledger (rederivedFinite, separationOnly, importedAssumption); MB defeater rows use counterexample. Ledger and proofs: Lean dependency spine.

AgendaBook-facing claimLedgerChapters
CIRL / scalar reward inferencegemScalar reward inference is exactly k=1 bundle inference; full transport implies cooperative readability.rederivedFiniteimportedAssumptionThe 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.rederivedFiniteseparationOnlyimportedAssumptionCorrection 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.rederivedFiniteseparationOnlyimportedAssumptionCorrection 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.rederivedFiniteimportedAssumptionBeyond Following Instruction, The End of Unconscious Value Drift
AUP / relative reachabilitygemOption preservation and low-impact penalties are separable from trajectory correction integrity.rederivedFiniteimportedAssumptionCorrection 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.rederivedFiniteimportedAssumptionCorrection Channels under Adversarial Pressure, The End of Unconscious Value Drift
DebategemFinite claim-tree debate rederives soundness, completeness, and judge-error-flip; local truth selection need not preserve the judge's correction channel.rederivedFiniteseparationOnlyimportedAssumptionManipulation, 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.rederivedFiniteseparationOnlyimportedAssumptionWhat Values Apply To, What Survives an Adversary: Verifiability and Representability, The End of Unconscious Value Drift
Embedded agency / ε-boundarygemAn ε-boundary certificate projects agent candidacy; composite bypass breaks the converse.counterexampleWhat Is an Agent Without Anthropomorphism?, Finding the Boundary, Agency Under Strategic Opacity, Parasites in the Correction System, The End of Unconscious Value Drift
Goodhart selection / basingemBasin stability is a selection projection; stable basins can be stably bad.counterexampleAlignment Is Selected or Destroyed by Its Environment, Multi-Agent Superintelligence and Inferential Coupling, The Alignment Attractor, Conductive Artifacts and Pivotal Processes, Towards Superintelligence Alignment
Grounding certificategemClass-green coverage can hold while value-relevant state drifts off-class.counterexampleAlignment as a Dynamical Guarantee, What Values Apply To, What Survives an Adversary: Verifiability and Representability
Deployment safety / safety casegemCase-green plus tolerance does not imply Safe without scope discipline.counterexampleA Safety Case for Superintelligence Alignment, What Survives an Adversary: Verifiability and Representability, Lethality Stress Test and Open Issues, The End of Unconscious Value Drift
Hidden capability / trace BIQgemSubsample trace BIQ is an appearance projection; bounded apparent BIQ does not discharge hidden productive control.rederivedFiniteAgency Under Strategic Opacity, Measuring Capability Without Task Ontology, Certification Without Construction, What Survives an Adversary: Verifiability and Representability, Who Still Counts After Transformation

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 — Finite claim-tree debate rederives soundness, completeness, and judge-error-flip; local truth selection need not preserve the judge's correction channel.
  • ELKgem — Latent readout is an epistemic subchannel, not correction uptake.
  • Embedded agency / ε-boundarygem — An ε-boundary certificate projects agent candidacy; composite bypass breaks the converse.
  • Goodhart selection / basingem — Basin stability is a selection projection; stable basins can be stably bad.
  • Grounding certificategem — Class-green coverage can hold while value-relevant state drifts off-class.
  • Deployment safety / safety casegem — Case-green plus tolerance does not imply Safe without scope discipline.
  • Hidden capability / trace BIQgem — Subsample trace BIQ is an appearance projection; bounded apparent BIQ does not discharge hidden productive control.

Nodes in this graph