P06 Blanket / no extra gain

Declarations: P06_blanket_zero_external_gain

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 P06_blanket_zero_external_gain {b : Boundary} :
    Blanket b → NoExtraExternalPredictiveGain b := fun h => h.2

/-- C-EPS (P07): an exact boundary is a 0-boundary. -/