The parabolic branch of the endgame #
The two parabolic fibers are affine lines. Their explicit rotation formulas make the second coordinate run through the whole base field, so in particular through the trace of a generator of the split torus.
theorem
BGS.Markoff.exists_iterate_parabolicTwoPoint_with_primitive_secondTrace
(p : ℕ)
[Fact (Nat.Prime p)]
(hpTwo : p ≠ 2)
(x : ↑(normalizedFiber1 2))
:
Every point of the trace-2 fiber reaches a primitive split trace in its second
coordinate.
theorem
BGS.Markoff.exists_iterate_parabolicNegTwoPoint_with_primitive_secondTrace
(p : ℕ)
[Fact (Nat.Prime p)]
(hpTwo : p ≠ 2)
(x : ↑(normalizedFiber1 (-2)))
:
Every point of the trace--2 fiber reaches a primitive split trace in its second
coordinate.
theorem
BGS.Markoff.exists_iterate_parabolicPoint_with_primitive_secondTrace
(p : ℕ)
[Fact (Nat.Prime p)]
(hpTwo : p ≠ 2)
(t : ZMod p)
(ht : t ^ 2 = 4)
(x : ↑(normalizedFiber1 t))
:
Unified parabolic branch.
theorem
BGS.Markoff.exists_iterate_parabolicPoint_with_maximal_secondRotation
(p : ℕ)
[Fact (Nat.Prime p)]
(hpFive : 5 ≤ p)
(t : ZMod p)
(ht : t ^ 2 = 4)
(x : ↑(normalizedFiber1 t))
:
∃ (n : ℕ), rotationOrder (normalizedRotate1^[n] ↑x).u2 = p - 1
For primes at least five, the primitive trace reached in the parabolic branch has maximal
split rotation order p - 1.
theorem
BGS.Markoff.exists_threshold_point_with_maximal_secondRotation
(splitCoefficient : ℕ)
(hSplitWeil : WeightedSplitTraceWeilBoundAssumption splitCoefficient)
(nonsplitCoefficient : ℕ)
(hNonsplitWeil : SeededNonsplitTraceWeilBoundAssumption nonsplitCoefficient)
{δ : ℝ}
(hδ : 0 < δ)
:
∃ (threshold : ℕ),
∀ (p : ℕ),
threshold ≤ p →
∀ [Fact (Nat.Prime p)] (t : ZMod p) (x : ↑(normalizedFiber1 t)),
↑p ^ (1 / 2 + δ) ≤ ↑(rotationOrder t) → ∃ (n : ℕ), rotationOrder (normalizedRotate1^[n] ↑x).u2 = p - 1
Full first-coordinate form of Proposition 10, including semisimple, parabolic, and the trace-zero exclusion.