The parabolic middle-game branch

The weighted Corvaja--Zannier argument is only needed for semisimple coordinate traces. The two parabolic traces have exact rotation orders p and 2 * p, already beyond every endgame threshold p ^ (1 / 2 + delta) with delta <= 1 / 2.

For primes congruent to one modulo four, this module also connects the explicit affine-line parametrizations to the concrete rotation cycles through every point on the two parabolic fibers. For primes congruent to three modulo four those fibers are empty by the existing results in ParabolicFibers.

theorem BGS.Markoff.endgamePowerThreshold_le_prime (p : ℕ) [Fact (Nat.Prime p)] (delta : ℝ) (hdelta : delta ≤ 1 / 2) : ↑p ^ (1 / 2 + delta) ≤ ↑p

Every endgame power threshold with exponent at most one is bounded by p.

theorem BGS.Markoff.endgamePowerThreshold_le_rotationOrder_two (p : ℕ) [Fact (Nat.Prime p)] (delta : ℝ) (hdelta : delta ≤ 1 / 2) : ↑p ^ (1 / 2 + delta) ≤ ↑(rotationOrder 2)

The trace-2 rotation already meets the endgame power threshold.

theorem BGS.Markoff.endgamePowerThreshold_le_rotationOrder_neg_two (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (delta : ℝ) (hdelta : delta ≤ 1 / 2) : ↑p ^ (1 / 2 + delta) ≤ ↑(rotationOrder (-2))

The trace--2 rotation has order 2 * p, hence also meets the endgame threshold.

theorem BGS.Markoff.endgamePowerThreshold_le_rotationOrder_of_parabolicTrace (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (delta : ℝ) (hdelta : delta ≤ 1 / 2) (t : ZMod p) (ht : t = 2 ∨ t = -2) : ↑p ^ (1 / 2 + delta) ≤ ↑(rotationOrder t)

Unified parabolic branch: either normalized parabolic trace is already in the endgame large-order range.

theorem BGS.Markoff.normalizedRotationCycle_card_of_mem_fiber_two (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (hmod : p % 4 = 1) (x : NormalizedPoint (ZMod p)) (hx : x ∈ normalizedFiber1 2) : (normalizedRotationCycle 2 x).card = p

Every point on the normalized trace-2 fiber for p = 1 mod 4 has a rotation cycle of exactly p points.

theorem BGS.Markoff.normalizedRotationCycle_card_of_mem_fiber_neg_two (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (hmod : p % 4 = 1) (x : NormalizedPoint (ZMod p)) (hx : x ∈ normalizedFiber1 (-2)) : (normalizedRotationCycle (-2) x).card = 2 * p

Every point on the normalized trace--2 fiber for p = 1 mod 4 has a rotation cycle of exactly 2 * p points.

theorem BGS.Markoff.endgamePowerThreshold_le_parabolicFiberTwo_cycleCard (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (hmod : p % 4 = 1) (delta : ℝ) (hdelta : delta ≤ 1 / 2) (x : NormalizedPoint (ZMod p)) (hx : x ∈ normalizedFiber1 2) : ↑p ^ (1 / 2 + delta) ≤ ↑(normalizedRotationCycle 2 x).card

The exact trace-2 cycle through any fiber point meets the endgame power threshold.

theorem BGS.Markoff.endgamePowerThreshold_le_parabolicFiberNegTwo_cycleCard (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (hmod : p % 4 = 1) (delta : ℝ) (hdelta : delta ≤ 1 / 2) (x : NormalizedPoint (ZMod p)) (hx : x ∈ normalizedFiber1 (-2)) : ↑p ^ (1 / 2 + delta) ≤ ↑(normalizedRotationCycle (-2) x).card

The exact trace--2 cycle through any fiber point meets the endgame power threshold.