P08 Violation blocks candidate

Declarations: P08_boundary_violation_blocks_candidate

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