OAI/Analysis/CircleDomains/Topology/GatePenaltySeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Step 2 of the compatible-barrier construction: replace the finitely many gate restrictions by a bounded penalty. Good paths retain the original half-unit separation; every bad path pays at least one unit.

  1. theorem OAI.CircleDomainRigidity.exists_ungated_half_separation line 22