OAI/NumberTheory/DukePrimeDegree/Geometry/SynchronizedAnnuli.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous small central portions at both shearing radii

This combines the two exponential regimes, all four candidate windows, and the actual leaf scaling law. It proves the leaf-mass conclusion of EKL Lemma 4.6 at the inverse shearing scale and at a fixed enlargement, for both initial points, at one common recurrence time.

  1. theorem OAI.DukePrimeDegree.exists_synchronized_leaf_annuli line 22