OAI/Analysis/CircleDomains/Modulus/WeightedCollarAvoidance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Collar splicing preserves avoidance of any set missed by both the original paths and the chosen collar levels, including forbidden gate hits.

  1. theorem OAI.CircleDomainRigidity.collar_level_exclusion_zero line 22
  2. theorem OAI.CircleDomainRigidity.exists_weighted_oneEnded_splicing_avoiding_set line 36
  3. theorem OAI.CircleDomainRigidity.exists_weighted_twoEnded_splicing_avoiding_set line 93