OAI/NumberTheory/DukePrimeDegree/Geometry/VaryingCutBoundary.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Boundary avoidance across changing finite levels

The union bound and Borel--Cantelli apply to all cuts up to a level that changes with time. The summability hypothesis is an explicit numerical budget; no entropy or subordinate-partition conclusion is assumed.

  1. theorem OAI.DukePrimeDegree.ae_eventually_avoid_varying_cut_levels line 17