proof

P25 Obedience ≠ corrigibility

Lean spine source

Declarations: P25_obedience_not_corrigibility

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P25_obedience_not_corrigibility :
    ∃ a : Bool, ToyObeysCurrentCommand a ∧ ¬ ToyPreservesCorrectionOperator a :=
  ⟨false, trivial, by decide⟩