Euler-seven square-envelope reduction surjectivity

This separate façade converts the exact split-cage transitivity endpoint to surjectivity of natural Markoff reduction using the canonical equivalence.

theorem BGS.Markoff.markoffReduction_surjective_of_splitCage_eulerSevenSquareEnvelope_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)) (squareEnvelope : ℕ → ℕ) (hsquare : ∀ (d : ℕ), maximalDivisorCountSum p (d + 1) ^ 2 ≤ squareEnvelope d) (hglobal : ∀ (d : ℕ), 35721 * squareEnvelope d ^ 4 < 8 * p) (hlinear : ∀ (d : ℕ), ↑d < ↑p ^ (5 / 6) → 24 ^ 2 * squareEnvelope d * d ^ 2 < p ^ 2) (hlarge : ∀ (z : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (5 / 6) ≤ ↑(maximalCoordinateRotationOrder ↑z) → SameNormalizedComponent (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c)) z) : Function.Surjective (markoffReduction p)

Natural Markoff reduction is surjective under the exact Euler-seven split-cage square-envelope hypotheses.