Feeding the weighted trace bound into maximal-divisor escape

The general Corvaja--Zannier theorem already provides a uniform estimate for all finite multiplicative subgroups. This adapter applies it only to the divisibility-maximal right subgroups required by the improved middle game.

theorem BGS.Markoff.exists_iterate_with_larger_secondRotationOrder_of_nonzero_nonparabolic_maximalOrders (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 * (middleGameMaximalOrders p (rotationOrder x.u1)).card) ^ 3 < rotationOrder x.u1) (hlinear : corvajaZannierCorollaryTwoSafeCoefficient * (middleGameMaximalOrders p (rotationOrder x.u1)).card * rotationOrder x.u1 < p) (hCZ : ∀ (w s : (quadraticFiniteField p)ˣ), ↑w ^ 2 ≠ 1 → algebraMapNormalizedPoint p x = splitFiberPoint w s → ↑s * (splitFiberProduct w * ↑s⁻¹) ≠ 1 → ∀ d ∈ middleGameMaximalOrders p (rotationOrder x.u1), ↑(weightedTraceEquationSolutions (↑s) (splitFiberProduct w * ↑s⁻¹) (Subgroup.zpowers w) (middleGameRightSubgroup p d)).card ≤ corvajaZannierTraceUpperBound p (rotationOrder x.u1) (Nat.card ↥(middleGameRightSubgroup p d))) : ∃ (n : ℕ), rotationOrder x.u1 < rotationOrder (normalizedRotate1^[n] x).u2

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

theorem BGS.Markoff.exists_iterate_with_larger_secondRotationOrder_of_weightedTraceBound_maximalOrders (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 * (middleGameMaximalOrders p (rotationOrder x.u1)).card) ^ 3 < rotationOrder x.u1) (hlinear : corvajaZannierCorollaryTwoSafeCoefficient * (middleGameMaximalOrders p (rotationOrder x.u1)).card * rotationOrder x.u1 < p) (hBound : WeightedTraceTorsionIntersectionBound p (quadraticFiniteField p)) : ∃ (n : ℕ), rotationOrder x.u1 < rotationOrder (normalizedRotate1^[n] x).u2

The in-repository weighted torsion-intersection theorem supplies every maximal-order estimate needed by the improved escape step.