Paired maximal-divisor middle-game assembly

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

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

One paired middle-game step strictly increases the maximum coordinate order under the coefficient-sensitive maximal-divisor inequalities.