Euler-seven split-cage frontier with automatic linear tail

Above 24^15 * 2^687, the tenth-moment estimate discharges the full linear middle-game family. Only the square-envelope cube obstruction remains.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_splitCage_eulerSevenSquareEnvelope_coarseLinearTail (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpSeven : 7 ≤ p) (hpLinearTail : 24 ^ 15 * 2 ^ 687 < p) (c : PuncturedMarkoffSurface (ZMod p)) (hbase : IsInSplitCage p (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c))) (hhalfThreshold : ↑p ^ (5 / 6) ≤ ↑((p - 1) / 2)) (squareEnvelope : ℕ → ℕ) (hsquare : ∀ (d : ℕ), maximalDivisorCountSum p (d + 1) ^ 2 ≤ squareEnvelope d) (hglobal : ∀ (d : ℕ), 35721 * squareEnvelope d ^ 4 < 8 * p) (hlarge : ∀ (z : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (5 / 6) ≤ ↑(maximalCoordinateRotationOrder ↑z) → SameNormalizedComponent (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c)) z) : PuncturedMarkoffTransitiveAt p

Split-cage transitivity with no separate linear-table hypothesis.

theorem BGS.Markoff.markoffReduction_surjective_of_splitCage_eulerSevenSquareEnvelope_coarseLinearTail (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpSeven : 7 ≤ p) (hpLinearTail : 24 ^ 15 * 2 ^ 687 < p) (c : PuncturedMarkoffSurface (ZMod p)) (hbase : IsInSplitCage p (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c))) (hhalfThreshold : ↑p ^ (5 / 6) ≤ ↑((p - 1) / 2)) (squareEnvelope : ℕ → ℕ) (hsquare : ∀ (d : ℕ), maximalDivisorCountSum p (d + 1) ^ 2 ≤ squareEnvelope d) (hglobal : ∀ (d : ℕ), 35721 * squareEnvelope d ^ 4 < 8 * p) (hlarge : ∀ (z : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (5 / 6) ≤ ↑(maximalCoordinateRotationOrder ↑z) → SameNormalizedComponent (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c)) z) : Function.Surjective (markoffReduction p)

Natural Markoff reduction surjectivity with the same automatic linear tail and no separate linear-table hypothesis.