Endgame wrappers for the elementary preliminary route #
The geometry and incidence estimates are the already proved explicit endgame and cage theorems. This file supplies them with the smaller preliminary-route numerical certificates.
theorem
BGS.Markoff.exists_preliminary_sameComponent_maximalRotation_of_large_firstCoordinate
{p : ℕ}
[Fact (Nat.Prime p)]
[Invertible 3]
(hp : preliminaryStrongApproximationCutoff ≤ p)
(x : NormalizedMarkoffSurface (ZMod p))
(hlarge : ↑p ^ (5 / 6) ≤ ↑(rotationOrder (↑x).u1))
:
∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent x y ∧ rotationOrder (↑y).u2 = p - 1
At the elementary preliminary cutoff, a large first-coordinate rotation reaches a maximal split rotation.
theorem
BGS.Markoff.exists_preliminary_sameComponent_splitCage_of_large_firstCoordinate
{p : ℕ}
[Fact (Nat.Prime p)]
[Invertible 3]
(hp : preliminaryStrongApproximationCutoff ≤ 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 preliminary large-order-to-cage endgame.
theorem
BGS.Markoff.exists_preliminary_sameComponent_splitCage_of_some_largeCoordinate
{p : ℕ}
[Fact (Nat.Prime p)]
[Invertible 3]
(hp : preliminaryStrongApproximationCutoff ≤ 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.preliminary_splitCage_connected
{p : ℕ}
[Fact (Nat.Prime p)]
[Invertible 3]
(hp : preliminaryStrongApproximationCutoff ≤ p)
(x y : NormalizedMarkoffSurface (ZMod p))
(hx : IsInSplitCage p x)
(hy : IsInSplitCage p y)
:
The selected split cage is connected at the preliminary cutoff.
theorem
BGS.Markoff.preliminary_sameNormalizedComponent_of_largeOrder_to_splitCage
{p : ℕ}
[Fact (Nat.Prime p)]
[Invertible 3]
(hp : preliminaryStrongApproximationCutoff ≤ 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.