Weighted certificate-free coarse-support surjectivity

This module feeds the weighted twentieth moment for the neighboring divisor counts into the Euler-seven coarse-support obstruction. It improves the tenth-moment checkpoint without changing the geometric frontier and without introducing a divisor table or a finite maximal-divisor certificate.

def BGS.Markoff.weightedCoarseSupportStrongApproximationOpenCutoff : ℕ

Open cutoff supplied by the weighted twentieth moment and the Euler-seven obstruction.

def BGS.Markoff.weightedCoarseSupportStrongApproximationCutoff : ℕ

Closed version of weightedCoarseSupportStrongApproximationOpenCutoff.

Equations

• BGS.Markoff.weightedCoarseSupportStrongApproximationCutoff = BGS.Markoff.weightedCoarseSupportStrongApproximationOpenCutoff + 1

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

The weighted joint twentieth moment rules out the final Euler-seven obstruction above the exact weighted cutoff.

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

The weighted cutoff dominates the support-only threshold used by the coarse endgame and cage arguments.

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

Natural Markoff reduction is surjective above the weighted certificate-free cutoff.

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

Closed-cutoff form used by the public Comparator theorem.