OAI/Analysis/CircleDomains/Selection/SingletonBandCrossing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The topological threshold step in Lemma 6.6. A path joining opposite band values must have a nonsingleton level contact. Consequently, when free contacts have singleton components, a threshold is paid at a domain point or a flagged point.

  1. theorem OAI.CircleDomainRigidity.exists_nonsingleton_band_contact line 17
  2. theorem OAI.CircleDomainRigidity.singleton_free_contacts_force_paid_level line 47