OAI/Analysis/CircleDomains/Topology/GatedCollarSplicing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One-ended collar splicing preserves all prescribed hit locations when the joining levels miss the hit contours. Dust avoidance is retained at all nonterminal times in the very same constructed path.

  1. theorem OAI.CircleDomainRigidity.exists_weighted_oneEnded_splicing_preserving_gates line 22
  2. theorem OAI.CircleDomainRigidity.exists_weighted_twoEnded_splicing_preserving_gates line 82