OAI/NumberTheory/DukePrimeDegree/Geometry/RootPairTimeSelection.lean

Actual diagonal recurrence with simultaneous leaf covariance

The correct two-coordinate shearing flow has a large measurable set on which both recurrence estimates hold on every long interval. Removing one null set also gives leaf covariance at almost every time. The common time can therefore satisfy all six recurrence conditions and all six covariance identities used in the two-scale argument.