Unconditional paired maximal-divisor middle-game escape

The weighted trace curve arising from a diagonalized nonzero nonparabolic Markoff fiber is admissible for the in-repository general Corvaja--Zannier theorem. Thus the paired maximal-order escape applies with no additional geometric hypothesis.

theorem BGS.Markoff.exists_iterate_with_larger_secondRotationOrder_of_nonzero_nonparabolic_pairedMaximalOrders (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (delta : ℝ) (hdelta : delta ≤ 1 / 2) (x : NormalizedPoint (ZMod p)) (hx : IsNormalizedMarkoff x) (hnonzero : x.u1 ≠ 0) (hnonparabolic : x.u1 ^ 2 ≠ 4) (hbelowEndgame : ↑(rotationOrder x.u1) < ↑p ^ (1 / 2 + delta)) (hcube : (6 * (middleGameMaximalOrders p (rotationOrder x.u1)).card) ^ 3 < rotationOrder x.u1) (hlinear : 24 * (middleGameMaximalOrders p (rotationOrder x.u1)).card * rotationOrder x.u1 < p) : ∃ (n : ℕ), rotationOrder x.u1 < rotationOrder (normalizedRotate1^[n] x).u2

Diagonalize a nonzero nonparabolic fiber and apply the unconditional paired maximal-order escape theorem.