P06 Blanket / no extra gain

Declarations: P06_blanket_zero_external_gain

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 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. -/