RawGatedBarrier.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Combine the proved finite-gate penalty with the actual chain-distance construction. This is the bounded raw barrier, before Sobolev regularization and the compatibility argument for the new smooth coordinate.

theorem OAI.CircleDomainRigidity.exists_raw_gated_barrier line 22