OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingCandidateWindows.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Four fixed candidate windows for two moving annuli

The inverse scale at a selected time is in one of two exponential regimes. Adding the logarithm of a fixed enlargement to both candidate exponents supplies the second annulus, while keeping all four exponents in the recurrence range once the logarithmic time window is large.

  1. theorem OAI.DukePrimeDegree.rootShearing_four_candidate_windows line 22