proof

P07 Exact boundary

Lean spine source

Declarations: P07_exact_boundary_is_epsilon_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 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. -/