Paired nonparabolic order escape using maximal divisors

This is the geometric diagonalized-fiber step for the paired maximal-order union. A hypothetical bounded target coordinate is first shown to be nonparabolic. Its trace is then represented by a non-two-torsion element of a maximal candidate subgroup, exactly the kind of witness excluded by the paired finite escape theorem.

theorem BGS.Markoff.exists_iterate_with_larger_secondRotationOrder_of_diagonalizedFiber_pairedMaximalOrders (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 : (6 * (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

Complete order escape from a diagonalized fiber under the paired coefficient conditions (6*K)^3 < currentOrder and 24*K*currentOrder < p.