OAI/NumberTheory/DukePrimeDegree/Geometry/ControlledDistanceCuts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Small quotient observations with controlled distance boundaries

Each logarithmic ball admits finitely many distance cuts that cover it, have small relative lifts, and satisfy a common dyadic boundary estimate. Both the number of cuts and their boundary constants are explicit.

  1. theorem OAI.DukePrimeDegree.exists_controlled_distance_cuts line 19