Euler-seven nonparabolic complement frontier

This is the complement-maximal argument with the exact paired Euler-characteristic middle-game condition 189 * M^3 < d.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_nonparabolicComplement_eulerSevenPairedMaximalDivisor_frontier (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpThree : 3 < p) (c : PuncturedMarkoffSurface (ZMod p)) (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) (hsign : ∀ (s : EvenSign) (x : PuncturedMarkoffSurface (ZMod p)), s • x ∈ puncturedComponentComplementFinset p c ↔ x ∈ puncturedComponentComplementFinset p c) (hfour : 4 ∣ (puncturedComponentComplementFinset p c).card) : PuncturedMarkoffTransitiveAt p

Complement-maximal frontier with the exact Euler-seven paired Corvaja--Zannier coefficient. The sign-invariance and factor-four inputs remain explicit.