OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingSelection.lean

Selecting a nontrivial shearing sequence from two annuli

This is the last compactness step in the two-scale argument of EKL, Section 4.5. A scale tending to zero makes every annular return diverge. The two-scale estimate selects a return with uniformly positive displacement; the common upper scale controls its entire trajectory. On a compact set with the stated horospherical separation property this contradicts arithmetic freeness. The separation property is a separate input here, not a claim that the low-entropy product theorem is proved.