OAI/NumberTheory/DukePrimeDegree/Geometry/CountableCutNeighborhoods.lean

Neighborhoods in countable future atoms from controlled cuts

The actual orbit height selects a finite family of cuts at each time. Their exponential boundary budget and the radial height budget make the whole countable future observation locally constant along a uniformly contracting continuous family.