Split-cage Euler-seven nonparabolic complement frontier

The split-cage base discharges the even-sign inputs, while the middle game uses the exact paired coefficient 189.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_splitCage_eulerSevenPairedMaximalDivisor_complement_frontier (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpSeven : 7 ≤ p) (c : PuncturedMarkoffSurface (ZMod p)) (hbase : IsInSplitCage p (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c))) (hhalfThreshold : ↑p ^ (5 / 6) ≤ ↑((p - 1) / 2)) (hcube : ∀ (d : ℕ), 0 < d → 8 * p ≤ (d * maximalDivisorCountSum p (d + 1)) ^ 2 → 189 * maximalDivisorCountSum p (d + 1) ^ 3 < d) (hlinear : ∀ (d : ℕ), ↑d < ↑p ^ (5 / 6) → 24 * maximalDivisorCountSum p (d + 1) * d < p) (hlarge : ∀ (z : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (5 / 6) ≤ ↑(maximalCoordinateRotationOrder ↑z) → SameNormalizedComponent (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c)) z) : PuncturedMarkoffTransitiveAt p

Exact Euler-seven nonparabolic complement frontier with the even-sign invariance and factor-four hypotheses discharged by a split-cage base.