Towards Superintelligence Alignment
proof

Lean dependency spine

P41 Value preservation ≠ legitimacy

Lean spine source

formal/AlignmentProofSpine/Philosophy.lean

Declarations: P41_current_value_preservation_does_not_decide_legitimacy

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 P41_current_value_preservation_does_not_decide_legitimacy :
    ∃ c : ToyChange, ToyPreservesCurrentValues c ∧
      ∃ L₁ L₂ : Bool, ToyAccepts L₁ c ∧ ¬ ToyAccepts L₂ c :=
  ⟨false, trivial, true, false, rfl, by decide⟩

/-- Toy person-states represented by `Bool`. -/