proof

P45 Philosophical boundary

Lean spine source

Declarations: P45_layered_alignment_has_philosophical_boundary

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 P45_layered_alignment_has_philosophical_boundary :
    ∃ (L₁ L₂ : Bool) (c : ToyChange),
      ToyTechnicalInvariant c ∧ ToyAccepts L₁ c ∧ ¬ ToyAccepts L₂ c :=
  P44_technical_invariants_do_not_determine_legitimacy