Punctured transitivity from the maximal-divisor frontier #
The maximal-orbit argument now uses the same maximal-divisor count in both places where the published proof used all divisors:
- counting points whose first two rotation orders are small;
- the Corvaja--Zannier union that forces an order increase.
This is the idea-level endpoint. A separate arithmetic certificate can
discharge its two explicit inequalities using the joint p - 1, p + 1
square envelope.
theorem
BGS.Markoff.puncturedMarkoffTransitiveAt_of_maximalDivisor_frontier
(p : ℕ)
[Fact (Nat.Prime p)]
[Invertible 3]
(hpThree : 3 < p)
(c : PuncturedMarkoffSurface (ZMod p))
(hcube :
∀ (d : ℕ),
0 < d →
p ≤ 2 * (2 + d * maximalDivisorCountSum p (d + 1)) ^ 2 →
(corvajaZannierCorollaryTwoSafeCoefficient * maximalDivisorCountSum p (d + 1)) ^ 3 < d)
(hlinear :
∀ (d : ℕ), ↑d < ↑p ^ (5 / 6) → corvajaZannierCorollaryTwoSafeCoefficient * maximalDivisorCountSum p (d + 1) * d < p)
(hlarge :
∀ (z : NormalizedMarkoffSurface (ZMod p)),
↑p ^ (5 / 6) ≤ ↑(maximalCoordinateRotationOrder ↑z) →
SameNormalizedComponent (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c)) z)
:
The finite maximal-orbit argument with maximal-divisor counts at both small-order and middle-game boundaries.