Root-free Euler-seven split-cage square-envelope frontier #
For M = maximalDivisorCountSum p (d + 1), a certificate M^2 ≤ S
reduces the exact Euler-seven cube branch to
35721 * S^4 < 8 * p,
because 35721 = 189^2. The linear branch is independently reduced to
24^2 * S * d^2 < p^2.
theorem
BGS.Markoff.puncturedMarkoffTransitiveAt_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)
:
The exact Euler-seven split-cage endpoint in root-free square-envelope form. The split-cage base, half-threshold comparison, and large-order orbit bridge remain explicit inputs.