OAI/NumberTheory/DukePrimeDegree/Geometry/HorosphereCollision.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Excluding bounded shearing collisions on a compact Lusin set

The arithmetic no-coordinate-zero property excludes every nonidentity horospherical stabilizer. Hence a compact leaf-data separation property rules out the selected shearing sequences at any fixed bounded size.

  1. theorem OAI.DukePrimeDegree.no_signed_shearing_pairs_on_free_compact line 20