A weighted twentieth-moment divisor bound

Squaring the elementary tenth-moment estimate would give τ(n)^20 ≤ 2^894 n^2. That loses the fractional part of every prime-factor penalty before the square is taken. Charging the doubled weight directly preserves those fractional parts and gives the stronger uniform estimate

τ(n)^20 ≤ 2^796 n^2.

The proof uses the same finite-band induction as the tenth-moment bound. It does not enumerate integers, factorizations, or neighboring divisor profiles.

def BGS.NumberTheory.weightedPrimePenaltyTwenty (p : ℕ) : ℕ

The exact integer penalty bands for the weight pair (20, 2).

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.NumberTheory.card_divisors_pow_twenty_le_weighted_constant_mul_sq (n : ℕ) (hn : n ≠ 0) : n.divisors.card ^ 20 ≤ 2 ^ 796 * n ^ 2

Weighted elementary divisor estimate: τ(n)^20 ≤ 2^796 n^2.