Euler-seven paired nonparabolic order escape

This is the diagonalized-fiber wiring for the exact cube condition 189*K^3 < currentOrder.

theorem BGS.Markoff.exists_iterate_larger_secondRotationOrder_of_diagonalizedFiber_eulerSevenPairedMaximalOrders (p : ℕ) [Fact (Nat.Prime 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) (hadmissible : WeightedTraceCurveIsCorvajaZannierAdmissible (↑s) (splitFiberProduct w * ↑s⁻¹)) (hbelowEndgame : ↑(rotationOrder x.u1) < ↑p ^ (1 / 2 + delta)) (hcube : 189 * (middleGameMaximalOrders p (rotationOrder x.u1)).card ^ 3 < rotationOrder x.u1) (hlinear : 24 * (middleGameMaximalOrders p (rotationOrder x.u1)).card * rotationOrder x.u1 < p) : ∃ (n : ℕ), rotationOrder x.u1 < rotationOrder (normalizedRotate1^[n] x).u2