Nonparabolic coordinates outside the endgame component

At the exponent used by the explicit route, a normalized parabolic trace has rotation order at least p ^ (5 / 6). Consequently, once every point at that threshold is connected to a fixed base point, every point outside the base component has nonparabolic coordinates.

theorem BGS.Markoff.first_two_nonparabolic_of_not_sameComponent_of_endgame_large_connected {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hpTwo : p ≠ 2) (base z : NormalizedMarkoffSurface (ZMod p)) (hlarge : ∀ (y : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (5 / 6) ≤ ↑(maximalCoordinateRotationOrder ↑y) → SameNormalizedComponent base y) (hnot : ¬SameNormalizedComponent base z) : (↑z).u1 ^ 2 ≠ 4 ∧ (↑z).u2 ^ 2 ≠ 4

A point outside a component containing every endgame-large point has nonparabolic first and second coordinates.