P07 Exact boundary

Declarations: P07_exact_boundary_is_epsilon_boundary

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 P07_exact_boundary_is_epsilon_boundary {b : Boundary} :
    ExactBoundary b → EpsilonBoundary 0 b := fun h => h

/-- C-BND (P08): a boundary violation blocks the boundary-candidate status. -/