An explicit divisor-counting bound

The asymptotic divisor bound used by the original assembly hides a threshold in a little-oh argument. This file keeps the same elementary factorization proof but uses a concrete polynomial-versus-exponential estimate. Its specialization at k = 32 is the numerical input for explicit strong approximation.

theorem BGS.NumberTheory.pow_succ_le_self_pow_mul_two_pow (k : ℕ) (hk : 0 < k) (a : ℕ) : (a + 1) ^ k ≤ k ^ k * 2 ^ a

A completely explicit replacement for the polynomial-versus-exponential constant in DivisorBound.lean.

theorem BGS.NumberTheory.card_divisors_pow_le_explicit_constant_mul (k : ℕ) (hk : 0 < k) (n : ℕ) (hn : n ≠ 0) : n.divisors.card ^ k ≤ (k ^ k) ^ 2 ^ k * n

Explicit factorization bound for the divisor-counting function.

noncomputable def BGS.NumberTheory.explicitDivisorConstantData : { n : ℕ // n = (32 ^ 32) ^ 2 ^ 32 }

Sealed data for the closed factorization constant. The subtype equation lets downstream proofs rewrite the value without asking the kernel to repeatedly normalize its enormous exponentiation.

Equations

• BGS.NumberTheory.explicitDivisorConstantData = Classical.choice BGS.NumberTheory.explicitDivisorConstantData._proof_1

noncomputable def BGS.NumberTheory.explicitDivisorConstant : ℕ

The closed factorization constant used by the explicit Markoff proof.

Equations

• BGS.NumberTheory.explicitDivisorConstant = ↑BGS.NumberTheory.explicitDivisorConstantData

theorem BGS.NumberTheory.explicitDivisorConstant_eq : explicitDivisorConstant = (32 ^ 32) ^ 2 ^ 32

theorem BGS.NumberTheory.explicitDivisorConstant_pos : 0 < explicitDivisorConstant

theorem BGS.NumberTheory.explicitDivisorConstant_le_pow_thirtyTwo : explicitDivisorConstant ≤ explicitDivisorConstant ^ 32

theorem BGS.NumberTheory.card_divisors_le_rpow_one_div_sixteen (n : ℕ) (hn : explicitDivisorConstant ≤ n) : ↑n.divisors.card ≤ ↑n ^ (1 / 16)

Above the concrete constant, the divisor count is bounded by the sixteenth root.