Coarse automatic linear tail

The simultaneous tenth-moment bound makes the linear middle-game condition automatic at a cutoff far below the paper scale. No divisor-table tuning is used here.

theorem BGS.Markoff.twentyFour_mul_lt_rpow_one_div_six_of_tenthMoment {p T : ℕ} (hp : 24 ^ 15 * 2 ^ 687 < p) (hmoment : T ^ 10 ≤ 2 ^ 458 * p) : ↑(24 * T) < ↑p ^ (1 / 6)

A tenth-moment estimate and the clean coefficient threshold 24^15 * 2^687 < p imply 24*T < p^(1/6).

The exponent choice is exact: (24^15 * 2^687)^4 = 24^60 * (2^458)^6.

theorem BGS.Markoff.preliminary_twentyFour_mul_divisorSum_lt_rpow_one_div_six_of_coarseBound {p : ℕ} (hp : 24 ^ 15 * 2 ^ 687 < p) : ↑(24 * ((p - 1).divisors.card + (p + 1).divisors.card)) < ↑p ^ (1 / 6)

Apply the generic tail estimate to the simultaneous divisor count T = τ(p-1) + τ(p+1).

theorem BGS.Markoff.twentyFour_mul_mul_lt_of_le_of_lt_fiveSixths {p T M d : ℕ} (hpPos : 0 < p) (hT : ↑(24 * T) < ↑p ^ (1 / 6)) (hM : M ≤ T) (hd : ↑d < ↑p ^ (5 / 6)) : 24 * M * d < p

Once 24*T < p^(1/6), every M ≤ T and every d < p^(5/6) satisfy the linear middle-game inequality.

theorem BGS.Markoff.preliminary_twentyFour_mul_mul_lt_of_coarseBound {p M d : ℕ} (hp : 24 ^ 15 * 2 ^ 687 < p) (hM : M ≤ (p - 1).divisors.card + (p + 1).divisors.card) (hd : ↑d < ↑p ^ (5 / 6)) : 24 * M * d < p

Coarse all-divisor specialization: the linear branch is automatic for any M bounded by the simultaneous divisor count.

theorem BGS.Markoff.maximalDivisorCountSum_linear_lt_of_coarseBound {p d : ℕ} (hp : 24 ^ 15 * 2 ^ 687 < p) (hd : ↑d < ↑p ^ (5 / 6)) : 24 * maximalDivisorCountSum p (d + 1) * d < p

In particular, the maximal-divisor coefficient in the Euler-seven frontier satisfies the linear branch automatically above the coarse tail.