Joint divisor bounds for neighboring even integers

For an odd natural number p, the two torus orders p - 1 and p + 1 have gcd exactly two. Consequently their divisor counts are not independent:

τ(p - 1) τ(p + 1) = 2 τ((p^2 - 1) / 2).

Combining this identity with the elementary tenth-moment divisor bound gives a joint estimate with one copy, rather than two copies, of the prime-factor penalty. This is the arithmetic input for improving the maximal-divisor cutoff.

theorem BGS.NumberTheory.card_divisors_pred_mul_card_divisors_succ_of_odd {p : ℕ} (hp : Odd p) : (p - 1).divisors.card * (p + 1).divisors.card = 2 * ((p ^ 2 - 1) / 2).divisors.card

Exact joint divisor-count identity for the neighboring torus orders.

theorem BGS.NumberTheory.card_divisors_pred_mul_card_divisors_succ_pow_ten_le {p : ℕ} (hp : Odd p) (hpTwo : 2 < p) : ((p - 1).divisors.card * (p + 1).divisors.card) ^ 10 ≤ 2 ^ 456 * (p ^ 2 - 1)

The product of the two neighboring divisor counts has a single prime-penalty factor in its tenth moment.

def BGS.NumberTheory.neighboringDivisorSumMomentConstant : ℕ

Joint tenth-moment constant for the sum of the neighboring divisor counts. The leading term is the one-number prime penalty; the smaller correction pays for the transition between the balanced and dominant cases.

Equations

• BGS.NumberTheory.neighboringDivisorSumMomentConstant = 2 ^ 447 + 2 ^ 429

theorem BGS.NumberTheory.neighboringDivisorSumMomentConstant_eq : neighboringDivisorSumMomentConstant = 2 ^ 429 * 262145

Split point used to combine the product moment with the two individual moments. It is chosen so that both resulting integer inequalities hold.

theorem BGS.NumberTheory.card_divisors_pred_mul_card_divisors_succ_pow_five_le {p : ℕ} (hp : Odd p) (hpTwo : 2 < p) : ((p - 1).divisors.card * (p + 1).divisors.card) ^ 5 ≤ 2 ^ 228 * p

Square-root form of the joint product moment.

theorem BGS.NumberTheory.card_divisors_pred_add_card_divisors_succ_pow_ten_le {p : ℕ} (hp : Odd p) (hpLarge : 794039 ≤ p) : ((p - 1).divisors.card + (p + 1).divisors.card) ^ 10 ≤ neighboringDivisorSumMomentConstant * p

A joint tenth moment for the sum of the neighboring divisor counts.

The usual power-of-a-sum inequality loses a factor of (2^9). Here comparable counts are controlled by the product moment, while in the dominant case the larger individual count controls the sum.

theorem BGS.NumberTheory.add_sq_le_sq_add_three_mul_of_le_of_mul_le {a b C J : ℕ} (ha : a ≤ C) (hb : b ≤ C) (hab : a * b ≤ J) : (a + b) ^ 2 ≤ C ^ 2 + 3 * J

If two nonnegative counts are individually at most C and their product is at most J, their squared sum is bounded by C^2 + 3J. This is the elementary inequality that replaces the paper's independent 4C^2 bound.

theorem BGS.NumberTheory.add_sq_le_sq_add_three_mul_of_pow_ten_envelope {a b C J K : ℕ} (ha : a ≤ C) (hb : b ≤ C) (hmoment : (a * b) ^ 10 ≤ K) (henvelope : K ≤ J ^ 10) : (a + b) ^ 2 ≤ C ^ 2 + 3 * J

Convert a certified tenth-moment envelope into the joint squared-sum bound used by the improved maximal-divisor algorithm.