OAI/Analysis/CircleDomains/Selection/RegularLevelReturn.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compactness forces a positive return time for each nonstationary regular-level orbit. Uniqueness turns every return into a true period.

  1. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.return_of_collision line 12
  2. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.exists_positive_period line 25