Iterating the middle-game escape to the cage #
noncomputable def
BGS.Markoff.maximalCoordinateRotationOrder
{R : Type u_1}
[CommRing R]
(x : NormalizedPoint R)
:
Maximum of the three coordinate rotation orders.
Equations
Instances For
theorem
BGS.Markoff.rotationOrder_first_le_maximalCoordinateRotationOrder
{R : Type u_1}
[CommRing R]
(x : NormalizedPoint R)
:
theorem
BGS.Markoff.rotationOrder_second_le_maximalCoordinateRotationOrder
{R : Type u_1}
[CommRing R]
(x : NormalizedPoint R)
:
theorem
BGS.Markoff.rotationOrder_third_le_maximalCoordinateRotationOrder
{R : Type u_1}
[CommRing R]
(x : NormalizedPoint R)
:
theorem
BGS.Markoff.exists_sameNormalizedComponent_firstRotation_eq_maximal
{R : Type u_1}
[CommRing R]
[Invertible 3]
(x : NormalizedMarkoffSurface R)
:
∃ (y : NormalizedMarkoffSurface R),
SameNormalizedComponent x y ∧ rotationOrder (↑y).u1 = maximalCoordinateRotationOrder ↑x
A coordinate permutation puts a coordinate of maximum rotation order first.
theorem
BGS.Markoff.exists_sameNormalizedComponent_maximalOrder_increase_of_middleRange
(p : ℕ)
[Fact (Nat.Prime p)]
[Invertible 3]
[Fintype (quadraticFiniteField p)]
(hpTwo : p ≠ 2)
{δ : ℝ}
(hδ : 0 < δ)
(hδQuarter : δ ≤ 1 / 4)
(hfour : 4 < ↑p ^ δ)
(hsize :
∀ (currentOrder : ℕ),
↑p ^ δ < ↑currentOrder →
↑currentOrder < ↑p ^ (1 - δ) →
(corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 3 < currentOrder ∧ corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card) * currentOrder < p)
(hBound : WeightedTraceTorsionIntersectionBound p (quadraticFiniteField p))
(x : NormalizedMarkoffSurface (ZMod p))
(hlower : ↑p ^ δ < ↑(maximalCoordinateRotationOrder ↑x))
(hbelow : ↑(maximalCoordinateRotationOrder ↑x) < ↑p ^ (1 / 2 + δ))
:
∃ (y : NormalizedMarkoffSurface (ZMod p)),
SameNormalizedComponent x y ∧ maximalCoordinateRotationOrder ↑x < maximalCoordinateRotationOrder ↑y
One genuine middle-game step strictly increases the maximum coordinate order.
theorem
BGS.Markoff.exists_sameNormalizedComponent_maximalOrder_increase_of_directBounds
(p : ℕ)
[Fact (Nat.Prime p)]
[Invertible 3]
[Fintype (quadraticFiniteField p)]
(hpTwo : p ≠ 2)
{δ : ℝ}
(hδ : δ ≤ 1 / 2)
(hBound : WeightedTraceTorsionIntersectionBound p (quadraticFiniteField p))
(x : NormalizedMarkoffSurface (ZMod p))
(hbelow : ↑(maximalCoordinateRotationOrder ↑x) < ↑p ^ (1 / 2 + δ))
(hcube :
(corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 3 < maximalCoordinateRotationOrder ↑x)
(hlinear :
corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card) * maximalCoordinateRotationOrder ↑x < p)
:
∃ (y : NormalizedMarkoffSurface (ZMod p)),
SameNormalizedComponent x y ∧ maximalCoordinateRotationOrder ↑x < maximalCoordinateRotationOrder ↑y
One middle-game step strictly increases the maximum coordinate order when the two
Corvaja--Zannier size inequalities are supplied directly. Unlike
exists_sameNormalizedComponent_maximalOrder_increase_of_middleRange, this interface does not
require a fixed lower power threshold for the current order.
theorem
BGS.Markoff.exists_threshold_middleGame_reaches_endgame
(hBound :
∀ (p : ℕ) [inst : Fact (Nat.Prime p)] [inst_1 : Fintype (quadraticFiniteField p)],
WeightedTraceTorsionIntersectionBound p (quadraticFiniteField p))
{δ : ℝ}
(hδ : 0 < δ)
(hδQuarter : δ ≤ 1 / 4)
:
∃ (threshold : ℕ),
∀ (p : ℕ),
threshold ≤ p →
∀ [inst : Fact (Nat.Prime p)] (hpThree : p ≠ 3) (x : NormalizedMarkoffSurface (ZMod p)),
↑p ^ δ < ↑(maximalCoordinateRotationOrder ↑x) →
∃ (y : NormalizedMarkoffSurface (ZMod p)),
SameNormalizedComponent x y ∧ ↑p ^ (1 / 2 + δ) ≤ ↑(maximalCoordinateRotationOrder ↑y)
Repeated weighted-trace escape steps reach the real endgame threshold.
theorem
BGS.Markoff.exists_threshold_middleGame_to_splitCage
(hBound :
∀ (p : ℕ) [inst : Fact (Nat.Prime p)] [inst_1 : Fintype (quadraticFiniteField p)],
WeightedTraceTorsionIntersectionBound p (quadraticFiniteField p))
(splitCoefficient : ℕ)
(hSplitWeil : WeightedSplitTraceWeilBoundAssumption splitCoefficient)
(nonsplitCoefficient : ℕ)
(hNonsplitWeil : SeededNonsplitTraceWeilBoundAssumption nonsplitCoefficient)
{δ : ℝ}
(hδ : 0 < δ)
(hδQuarter : δ ≤ 1 / 4)
:
∃ (threshold : ℕ),
∀ (p : ℕ),
threshold ≤ p →
∀ [inst : Fact (Nat.Prime p)] (hpThree : p ≠ 3) (x : NormalizedMarkoffSurface (ZMod p)),
↑p ^ δ < ↑(maximalCoordinateRotationOrder ↑x) →
∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent x y ∧ IsInSplitCage p y
The weighted-trace middle-game bound, followed by the completed endgame, lands every point above the opening threshold in the selected split cage.