PrescribedInteriorCost.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The interior adapted-failure estimate bounds the cleanup cost, while the one-point theorem pays for the boundary rows.

theorem OAI.SLEExactGauge.prescribed_missed_cost_tendsto_zero_of_interior line 16