Unconditional Euler-seven paired maximal-divisor middle-game escape

The exact support-index and Euler-characteristic calculation improves the paired cube condition from (6 * K)^3 < d to 189 * K^3 < d.

theorem BGS.Markoff.exists_iterate_larger_secondRotationOrder_of_nonzero_nonparabolic_eulerSevenPairedMaximalOrders (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (delta : ℝ) (hdelta : delta ≤ 1 / 2) (x : NormalizedPoint (ZMod p)) (hx : IsNormalizedMarkoff x) (hnonzero : x.u1 ≠ 0) (hnonparabolic : x.u1 ^ 2 ≠ 4) (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

Diagonalize a nonzero nonparabolic fiber and apply the exact Euler-seven paired maximal-order escape theorem.