proof

P44 Invariants ≠ legitimacy

Lean spine source

formal/AlignmentProofSpine/Philosophy.lean

Declarations: P44_technical_invariants_do_not_determine_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 P44_technical_invariants_do_not_determine_legitimacy :
    ∃ (L₁ L₂ : Bool) (c : ToyChange),
      ToyTechnicalInvariant c ∧ ToyAccepts L₁ c ∧ ¬ ToyAccepts L₂ c :=
  ⟨true, false, false, trivial, rfl, by decide⟩

/-- C-LAYER (P45): layered alignment has a philosophical boundary — even granting
    all technical invariants, legitimacy remains underdetermined. This is exactly
    the disagreement exhibited by `P44`. -/