Nonparabolic order escape using maximal divisors

This is the geometric middle-game step with the maximal-divisor cover wired all the way through. The Corvaja--Zannier hypothesis and both numerical inequalities are required only for divisibility-maximal candidate orders.

theorem BGS.Markoff.exists_iterate_with_larger_secondRotationOrder_of_diagonalizedFiber_maximalOrders (p : ℕ) [Fact (Nat.Prime p)] [Fintype (quadraticFiniteField p)] (hpTwo : p ≠ 2) (delta : ℝ) (hdelta : delta ≤ 1 / 2) (x : NormalizedPoint (ZMod p)) (w s : (quadraticFiniteField p)ˣ) (hw : ↑w ^ 2 ≠ 1) (hpoint : algebraMapNormalizedPoint p x = splitFiberPoint w s) (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 : ↑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

Complete nonparabolic order escape from a diagonalized fiber, with the Corvaja--Zannier union restricted to maximal candidate orders.