proof

P44 Invariants ≠ legitimacy

Lean spine source

Declarations: P44_technical_invariants_do_not_determine_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 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`. -/