OAI/NumberTheory/DukePrimeDegree/Dynamics/IntrinsicShearingCollision.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Two annular equal-leaf sequences force a horospherical collision

The compactness argument is expressed directly in terms of the actual intrinsic leaves. Countable determining data allow passage to the limit on a Lusin compact set. Arithmetic freeness ensures that the nonidentity limiting matrix moves the limiting point.

  1. theorem OAI.DukePrimeDegree.two_annular_equal_leaves_force_collision line 22