Euler-seven frontier with all support tails discharged

At 2^756 < p, the simultaneous tenth-moment estimate now supplies the linear middle game, primitive endgame, cage connectivity, split-cage base, and half-order comparison. The only remaining arithmetic certificate is a square envelope for the joint maximal-divisor count together with its exact Euler-seven cubic inequality.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_eulerSevenSquareEnvelope_coarseSupport (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpSupport : 2 ^ 756 < p) (squareEnvelope : ℕ → ℕ) (hcount : ∀ (d : ℕ), maximalDivisorCountSum p (d + 1) ^ 2 ≤ squareEnvelope d) (hcubic : ∀ (d : ℕ), 35721 * squareEnvelope d ^ 4 < 8 * p) : PuncturedMarkoffTransitiveAt p

Punctured transitivity above the unified support cutoff. All non-cubic arithmetic and all endgame/cage hypotheses have been discharged.

theorem BGS.Markoff.markoffReduction_surjective_of_eulerSevenSquareEnvelope_coarseSupport (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpSupport : 2 ^ 756 < p) (squareEnvelope : ℕ → ℕ) (hcount : ∀ (d : ℕ), maximalDivisorCountSum p (d + 1) ^ 2 ≤ squareEnvelope d) (hcubic : ∀ (d : ℕ), 35721 * squareEnvelope d ^ 4 < 8 * p) : Function.Surjective (markoffReduction p)

Natural Markoff reduction is surjective under the same support-closed Euler-seven square-envelope certificate.