Certificate-free coarse-support surjectivity

The Euler-seven complement argument reduces the last global obstruction to 35721 * S^4 < 8 * p. Taking S to be the square of the simultaneous divisor count and combining this obstruction with the elementary tenth moment gives an unconditional cutoff without a divisor table.

def BGS.Markoff.coarseSupportStrongApproximationOpenCutoff : ℕ

The exact open cutoff supplied by the Euler-seven obstruction and the joint tenth moment for the two neighboring divisor counts.

def BGS.Markoff.coarseSupportStrongApproximationCutoff : ℕ

Closed version of coarseSupportStrongApproximationOpenCutoff.

Equations

• BGS.Markoff.coarseSupportStrongApproximationCutoff = BGS.Markoff.coarseSupportStrongApproximationOpenCutoff + 1

theorem BGS.Markoff.preliminary_35721_mul_divisorSum_pow_eight_lt {p : ℕ} (hpOdd : Odd p) (hp : coarseSupportStrongApproximationOpenCutoff < p) : 35721 * ((p - 1).divisors.card + (p + 1).divisors.card) ^ 8 < 8 * p

The joint tenth moment rules out the final Euler-seven obstruction above the exact coarse-support cutoff.

theorem BGS.Markoff.maximalDivisorCountSum_sq_le_divisorSum_sq (p d : ℕ) : maximalDivisorCountSum p (d + 1) ^ 2 ≤ ((p - 1).divisors.card + (p + 1).divisors.card) ^ 2

Every joint maximal-divisor square count is bounded by the square of the simultaneous all-divisor count.

theorem BGS.Markoff.twoPow756_lt_of_coarseSupportOpenCutoff_lt {p : ℕ} (hp : coarseSupportStrongApproximationOpenCutoff < p) : 2 ^ 756 < p

The exact cutoff dominates the support-only threshold required by the coarse endgame and cage arguments.

theorem BGS.Markoff.markoffReduction_surjective_of_coarseSupportOpenCutoff (p : ℕ) (hpPrime : Nat.Prime p) (hp : coarseSupportStrongApproximationOpenCutoff < p) : Function.Surjective (markoffReduction p)

Natural Markoff reduction is surjective above the exact certificate-free coarse-support cutoff.

theorem BGS.Markoff.markoffReduction_surjective_of_coarseSupportBound (p : ℕ) (hpPrime : Nat.Prime p) (hp : coarseSupportStrongApproximationCutoff ≤ p) : Function.Surjective (markoffReduction p)

Closed-cutoff form used by the public Comparator theorem.