Feeding the geometric Corvaja--Zannier estimate into a Markoff move

This module connects the weighted torsion-intersection bound to the already completed middle-game order-escape chain. The actual weighted trace curve's admissibility is proved from its Markoff coefficients.

Given those premises, Lean returns a natural iterate of the Markoff rotation with strictly larger neighboring rotation order. No independent weighted-finset estimate remains between the cited curve theorem and the dynamical conclusion.

theorem BGS.Markoff.exists_iterate_with_larger_secondRotationOrder_of_weightedTraceBound (p : ℕ) [Fact (Nat.Prime p)] [Fintype (quadraticFiniteField 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 : (corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 3 < rotationOrder x.u1) (hlinear : corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card) * rotationOrder x.u1 < p) (hBound : WeightedTraceTorsionIntersectionBound p (quadraticFiniteField p)) : ∃ (n : ℕ), rotationOrder x.u1 < rotationOrder (normalizedRotate1^[n] x).u2

The uniform weighted-trace bound, after Lean verifies every concrete diagonalized Markoff trace curve, produces an actual middle-game order-increasing iterate.