Large order in any coordinate reaches a maximal rotation

This packages the first-coordinate endgame with the normalized coordinate permutations and the Markoff-component relation.

theorem BGS.Markoff.endgame_three_ne_zero_zmod_of_prime_ne_three (p : ℕ) [Fact (Nat.Prime p)] (hpThree : p ≠ 3) : 3 ≠ 0

Three is nonzero in a prime residue field of characteristic different from three.

theorem BGS.Markoff.exists_threshold_sameComponent_maximalRotation_of_large_firstCoordinate (splitCoefficient : ℕ) (hSplitWeil : WeightedSplitTraceWeilBoundAssumption splitCoefficient) (nonsplitCoefficient : ℕ) (hNonsplitWeil : SeededNonsplitTraceWeilBoundAssumption nonsplitCoefficient) {δ : ℝ} (hδ : 0 < δ) : ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ [inst : Fact (Nat.Prime p)] (hpThree : p ≠ 3) (x : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (1 / 2 + δ) ≤ ↑(rotationOrder (↑x).u1) → ∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent x y ∧ rotationOrder (↑y).u2 = p - 1

A large first-coordinate rotation reaches a same-component point with maximal second rotation.

theorem BGS.Markoff.exists_threshold_sameComponent_maximalRotation_of_some_largeCoordinate (splitCoefficient : ℕ) (hSplitWeil : WeightedSplitTraceWeilBoundAssumption splitCoefficient) (nonsplitCoefficient : ℕ) (hNonsplitWeil : SeededNonsplitTraceWeilBoundAssumption nonsplitCoefficient) {δ : ℝ} (hδ : 0 < δ) : ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ [inst : Fact (Nat.Prime p)] (hpThree : p ≠ 3) (x : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (1 / 2 + δ) ≤ ↑(rotationOrder (↑x).u1) ∨ ↑p ^ (1 / 2 + δ) ≤ ↑(rotationOrder (↑x).u2) ∨ ↑p ^ (1 / 2 + δ) ≤ ↑(rotationOrder (↑x).u3) → ∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent x y ∧ rotationOrder (↑y).u2 = p - 1

Published Proposition 10: if any coordinate rotation is large, the point is connected to a point with a maximal split rotation.