The nonparabolic middle-game order-escape step

This module composes the weighted finite escape, the concrete roots-of-unity right subgroups, the split/nonsplit trace classification, and the weighted coset coordinate identity. The only deep input is the weighted Corvaja--Zannier cardinal estimate on the actual solution finsets.

theorem BGS.Markoff.algebraMapNormalizedPoint_iterate_normalizedRotate1 (p n : ℕ) [Fact (Nat.Prime p)] (x : NormalizedPoint (ZMod p)) : algebraMapNormalizedPoint p (normalizedRotate1^[n] x) = normalizedRotate1^[n] (algebraMapNormalizedPoint p x)

Scalar extension commutes with every iterate of the normalized rotation.

theorem BGS.Markoff.rotationOrder_mem_middleGameCandidateOrders_of_nonparabolic (p currentOrder : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (t : ZMod p) (hnonparabolic : t ^ 2 ≠ 4) (hsmall : rotationOrder t ≤ currentOrder) : rotationOrder t ∈ middleGameCandidateOrders p currentOrder

A nonparabolic trace whose rotation order is at most currentOrder has a candidate order dividing p - 1 or p + 1.

theorem BGS.Markoff.splitFiberProduct_ne_one_of_four_ne_zero {E : Type u_1} [Field E] (w : Eˣ) (hfour : 4 ≠ 0) : splitFiberProduct w ≠ 1

The split-fiber invariant is never one in odd characteristic.

theorem BGS.Markoff.exists_iterate_with_larger_secondRotationOrder_of_diagonalizedFiber (p : ℕ) [Fact (Nat.Prime p)] [Fintype (quadraticFiniteField 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) (hbelowEndgame : ↑(rotationOrder x.u1) < ↑p ^ (1 / 2 + delta)) (hcube : (corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 3 < rotationOrder x.u1) (hlinear : corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card) * rotationOrder x.u1 < p) (hCZ : ↑s * (splitFiberProduct w * ↑s⁻¹) ≠ 1 → ∀ d ∈ middleGameCandidateOrders p (rotationOrder x.u1), ↑(weightedTraceEquationSolutions (↑s) (splitFiberProduct w * ↑s⁻¹) (Subgroup.zpowers w) (middleGameRightSubgroup p d)).card ≤ corvajaZannierTraceUpperBound p (rotationOrder x.u1) (Nat.card ↥(middleGameRightSubgroup p d))) : ∃ (n : ℕ), rotationOrder x.u1 < rotationOrder (normalizedRotate1^[n] x).u2

Complete nonparabolic order escape from a diagonalized presentation of the current fiber.

The numeric hypotheses are the already-isolated finite middle-game range. hCZ is the sole deep premise: the weighted Corvaja--Zannier estimate for the actual cyclic left subgroup and the canonical right subgroups.