Towards Superintelligence Alignment
proof

Lean dependency spine

P29 Self-control gap

Lean spine source

formal/AlignmentProofSpine/Successors.lean

Declarations: P29_better_self_modeling_can_increase_risk

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 P29_better_self_modeling_can_increase_risk
    {A B : System}
    (hcontrol : SelfControl A < SelfControl B)
    (hvis : CorrectionVisibility B ≤ CorrectionVisibility A) :
    SelfControl A - CorrectionVisibility A < SelfControl B - CorrectionVisibility B := by
  omega