Euler-seven paired maximal-divisor middle-game assembly

This lifts the exact 189 * K^3 < d paired escape from a chosen coordinate to the maximum of the three coordinate rotation orders.

theorem BGS.Markoff.exists_sameNormalizedComponent_maximalOrder_increase_of_eulerSevenPairedMaximalDivisorBounds (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 : 189 * (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 exact Euler-seven paired middle-game step strictly increases the maximum coordinate order.