P08 Violation blocks candidate

Declarations: P08_boundary_violation_blocks_candidate

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 P08_boundary_violation_blocks_candidate {A : System} :
    BoundaryViolation A → ¬ BoundaryCandidate A := fun h hc => hc h