CavityMinimumIncrement.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The true minimizing pressure envelopes dominate the original physical full-minus-base cavity increment, up to explicit vanishing penalty terms.