Towards Superintelligence Alignment
proof

Lean dependency spine

P27 Successor invariant chain

Lean spine source

formal/AlignmentProofSpine/Successors.lean

Declarations: P27_successor_invariant_chain

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P27_successor_invariant_chain
    (P : System → Prop)
    {A B : System}
    (h0 : P A)
    (hstep : ∀ X Y, Successor X Y → P X → P Y)
    (hchain : SuccessorChain A B) :
    P B := by
  induction hchain with
  | refl A => exact h0
  | step hsucc _ ih => exact ih (hstep _ _ hsucc h0)