OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingSignedCollision.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact collisions at signed annular return times

Equal leaf data on compact simultaneous returns survive the signed bounded shearing limit. A uniform horospherical separation property then excludes such sequences.

  1. theorem OAI.DukePrimeDegree.signed_shearing_forces_horospherical_collision line 20
  2. theorem OAI.DukePrimeDegree.no_small_signed_shearing_pairs line 48