proof

P41 Value preservation ≠ legitimacy

Lean spine source

Declarations: P41_current_value_preservation_does_not_decide_legitimacy

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 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`. -/