Explicit punctured transitivity

This file isolates the finite maximal-orbit argument used by the explicit punctured-transitivity proof. The only geometric input is a stated large-order-to-base-component hypothesis; the middle-game step is the proved Corvaja--Zannier escape theorem.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_maximalOrbit_frontier (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpThree : 3 < p) (c : PuncturedMarkoffSurface (ZMod p)) (hcube : ∀ (d : ℕ), 0 < d → p ≤ 2 * (2 + d * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 2 → (corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 3 < d) (hlinear : ∀ (d : ℕ), ↑d < ↑p ^ (5 / 6) → corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card) * d < p) (hlarge : ∀ (z : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (5 / 6) ≤ ↑(maximalCoordinateRotationOrder ↑z) → SameNormalizedComponent (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c)) z) : PuncturedMarkoffTransitiveAt p

The finite maximal-orbit argument at a fixed prime. The hypotheses expose exactly the three frontiers consumed by the argument: the divisor-sensitive count forces the cubic middle-game bound, the upper range supplies the linear bound, and large order connects to one base component.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_explicitCutoff (p : ℕ) (hpPrime : Nat.Prime p) (hp : explicitStrongApproximationCutoff ≤ p) : PuncturedMarkoffTransitiveAt p

Explicit punctured transitivity. The closed cutoff supplies all numerical estimates; the large-order route and cage connectivity are the pointwise explicit endgame theorems.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_concreteExplicitBound (p : ℕ) (hpPrime : Nat.Prime p) (hp : 2 ^ 9 * (48 ^ 3 + 1) ^ 18 * (2 ^ 9 * (9 ^ 9) ^ 2 ^ 9) ^ 8 + 1 ≤ p) : PuncturedMarkoffTransitiveAt p

Raw-expression form of the explicit endpoint. This displays the actual closed natural-number bound without requiring clients to unfold either sealed constant.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_preliminaryCutoff (p : ℕ) (hpPrime : Nat.Prime p) (hp : preliminaryStrongApproximationCutoff ≤ p) : PuncturedMarkoffTransitiveAt p

Elementary preliminary-route punctured transitivity. This is the paper's all-divisors Corvaja--Zannier route with the analytic Nicolas estimate replaced by the fully formalized elementary tenth-moment divisor bound.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_concretePreliminaryBound (p : ℕ) (hpPrime : Nat.Prime p) (hp : 2 ^ 1833 * (48 ^ 3 + 1) ^ 10 + 1 ≤ p) : PuncturedMarkoffTransitiveAt p

Raw-expression form of the elementary preliminary-route endpoint.