Maximal-divisor middle-game assembly

This module lifts the maximal-order Corvaja--Zannier escape from a chosen coordinate to the maximum of the three coordinate rotation orders.

theorem BGS.Markoff.exists_sameNormalizedComponent_maximalOrder_increase_of_maximalDivisorBounds (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] [Fintype (quadraticFiniteField p)] (hpTwo : p ≠ 2) {delta : ℝ} (hdelta : delta ≤ 1 / 2) (hBound : WeightedTraceTorsionIntersectionBound p (quadraticFiniteField p)) (x : NormalizedMarkoffSurface (ZMod p)) (hbelow : ↑(maximalCoordinateRotationOrder ↑x) < ↑p ^ (1 / 2 + delta)) (hcube : (corvajaZannierCorollaryTwoSafeCoefficient * (middleGameMaximalOrders p (maximalCoordinateRotationOrder ↑x)).card) ^ 3 < maximalCoordinateRotationOrder ↑x) (hlinear : corvajaZannierCorollaryTwoSafeCoefficient * (middleGameMaximalOrders p (maximalCoordinateRotationOrder ↑x)).card * maximalCoordinateRotationOrder ↑x < p) : ∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent x y ∧ maximalCoordinateRotationOrder ↑x < maximalCoordinateRotationOrder ↑y

One middle-game step strictly increases the maximum coordinate order when the two size inequalities use only divisibility-maximal candidate orders.