ModelSelectedBarrier.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual selected compact source pair satisfies the quantitative barrier comparison. Its horizontal, vertical and support terms are proved from the selection and transported height-error witness.

theorem OAI.CircleDomainRigidity.CompactScalarModel.selected_barrier_error line 18