Lean

Lean checks what follows if named hypotheses hold. Those hypotheses are bridge axioms in the dependency spine: inputs, not theorems. The book assumes we can find the real optimizer's boundary. Lean's matching hypothesis is that a named estimator of that boundary is sound. A green estimator with the real controller elsewhere falsifies the Lean hypothesis without making the search problem meaningless. A different book assumption never becomes a Lean input: that civilization still has enough correction capacity to participate.

• Does CorrectionIntegrity faithfully capture corrigibility?
• Is scalar CIRL enough?
• Does ELK solve alignment?
• Does debate guarantee aligned oversight?

Appendix G translates the spine. Appendix B maps chapter assumptions to field cruxes and to Lean bridges. See also the bridge assumptions card. These checks do not prove real systems are aligned.