OAI/NumberTheory/DukePrimeDegree/Entropy/LowEntropyCollision.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual equal-leaf horospherical collisions

All sets, return pairs, recurrence times and annular translations are constructed from diagonal invariance and nontrivial root leaves. No horospherical separation premise is used here. The resulting distinct points avoid any prescribed null set.

  1. theorem OAI.DukePrimeDegree.RootPairSelectionData.exists_equal_leaf_collision line 24
  2. theorem OAI.DukePrimeDegree.exists_distinct_equal_leaf_horospherical_pair line 93