Towards Superintelligence Alignment

Appendix G on the web

Lean proof spine

A machine-checked conditional skeleton: if the stated definitions, certificates, and bridge assumptions hold, then the certification claims follow. Lean does not prove real systems satisfy the bridges.

Open overview graphJump to overview diagramView Lean sourceBridge crosswalk (Appendix B)

Overview diagram

Same Graphviz source as Appendix G, figure 00-overview. Click nodes to drill down.

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

Field results rederived and subsumed

External alignment agendas projected into the book's invariants on a shared finite domain.

Bridge assumptions

MB1–MB10 connect measured systems to book predicates. Bridges are never hidden inside definitions.

Complete Lean proof spine

Proved nodes, counterexamples, and how the four sub-spines compose into certified-class safety.

Modules

ModuleBook chapters
Core carriers and bridges
AlignmentProofSpine/Core.lean		foundations
Boundaries and measurement
AlignmentProofSpine/Boundaries.lean		6–7, 10, 36
Capability and B-IQ
AlignmentProofSpine/Capability.lean		11–14, 33, 36
Value bundles and transport
AlignmentProofSpine/Bundles.lean		15–23, 30
Correction channels
AlignmentProofSpine/Correction.lean		25–29, 41–43
Successors and continuity
AlignmentProofSpine/Successors.lean		28–31
Basins, layers, certification
AlignmentProofSpine/Certification.lean		1–5, 35, 39, 44
Adversarial measurement
AlignmentProofSpine/Adversarial.lean		32–37
Successor forgeability (MB10)
AlignmentProofSpine/Forgeability.lean		8, 31, 43, 48
Field-agenda crosswalk
AlignmentProofSpine/Field.lean		Appendix B crosswalk

Try-it-out snippets

Self-contained finite proofs and counterexamples, pre-linked toLean 4 Web. Add a file underformal/playgrounds/ and run npm run sync — URLs are generated automatically.

What Lean checks

Three kinds of result appear throughout: proof local theorems,counterexample finite separations, andbridge empirical handoffs (MB1–MB10). Headline certification theorems depend on explicit bridge records — inspect with #print axioms in the repo.