P28 Missing invariant blocks safety

Declarations: P28_missing_cci_blocks_successor_safety

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 P28_missing_cci_blocks_successor_safety
    {A B : System}
    (h : ¬ CCIPreserved A B) :
    ¬ SuccessorSafe A B := by
  intro ⟨w⟩
  exact h w.cci