OAI/NumberTheory/DukePrimeDegree/Geometry/TemperedCutBoundary.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Boundary avoidance up to the actual orbit height

The proper height grows sublinearly without an integrability assumption. It is therefore eventually below a sufficiently slow linear cutoff, where the exponential boundary budget is summable.

  1. theorem OAI.DukePrimeDegree.ae_eventually_avoid_cuts_up_to_height line 18