Endgame and cage wrappers at the unified coarse support cutoff #
The geometric endgame is unchanged. This module feeds it the simultaneous
tenth-moment estimates proved in CoarseSupportTail, so every non-cubic
support condition follows from the single hypothesis 2^756 < p.
theorem
BGS.Markoff.exists_coarse_sameComponent_maximalRotation_of_large_firstCoordinate
{p : ℕ}
[Fact (Nat.Prime p)]
[Invertible 3]
(hp : 2 ^ 756 < p)
(x : NormalizedMarkoffSurface (ZMod p))
(hlarge : ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u1))
:
∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent x y ∧ rotationOrder (↑y).u2 = p - 1
Above the unified support cutoff, a large first-coordinate rotation reaches a maximal split rotation.
theorem
BGS.Markoff.exists_coarse_sameComponent_splitCage_of_large_firstCoordinate
{p : ℕ}
[Fact (Nat.Prime p)]
[Invertible 3]
(hp : 2 ^ 756 < p)
(x : NormalizedMarkoffSurface (ZMod p))
(hlarge : ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u1))
:
∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent x y ∧ IsInSplitCage p y
First-coordinate form of the coarse large-order-to-cage endgame.
theorem
BGS.Markoff.exists_coarse_sameComponent_splitCage_of_some_largeCoordinate
{p : ℕ}
[Fact (Nat.Prime p)]
[Invertible 3]
(hp : 2 ^ 756 < p)
(x : NormalizedMarkoffSurface (ZMod p))
(hlarge :
↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u1) ∨ ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u2) ∨ ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u3))
:
∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent x y ∧ IsInSplitCage p y
If one coordinate rotation is large, the point reaches the split cage.
theorem
BGS.Markoff.coarse_splitCage_connected
{p : ℕ}
[Fact (Nat.Prime p)]
[Invertible 3]
(hp : 2 ^ 756 < p)
(x y : NormalizedMarkoffSurface (ZMod p))
(hx : IsInSplitCage p x)
(hy : IsInSplitCage p y)
:
The selected split cage is connected above the unified support cutoff.
theorem
BGS.Markoff.coarse_sameNormalizedComponent_of_largeOrder_to_splitCage
{p : ℕ}
[Fact (Nat.Prime p)]
[Invertible 3]
(hp : 2 ^ 756 < p)
(base x : NormalizedMarkoffSurface (ZMod p))
(hbase : IsInSplitCage p base)
(hlarge :
↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u1) ∨ ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u2) ∨ ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u3))
:
SameNormalizedComponent base x
A large-order point lies in the component of any chosen cage base point.