Elementary numerical certificates for the paper's preliminary route

The published preliminary argument uses Nicolas' explicit divisor bound to obtain the threshold 10^532. Here we formalize the same all-divisors Corvaja--Zannier route using a completely elementary tenth-moment estimate. The resulting cutoff is somewhat larger, but every numerical input is checked inside Lean.

def BGS.Markoff.preliminaryDivisorMomentConstant : ℕ

The simultaneous tenth-moment constant for the divisor counts of p - 1 and p + 1.

Equations

• BGS.Markoff.preliminaryDivisorMomentConstant = 2 ^ 457

theorem BGS.Markoff.preliminaryDivisorMomentConstant_eq : preliminaryDivisorMomentConstant = 2 ^ 457

theorem BGS.Markoff.preliminaryDivisorMomentConstant_pos : 0 < preliminaryDivisorMomentConstant

@[irreducible]

def BGS.Markoff.preliminaryStrongApproximationCutoffData : { n : ℕ // n = 2 ^ 1833 * (48 ^ 3 + 1) ^ 10 + 1 }

Sealed data for the elementary preliminary-route cutoff.

def BGS.Markoff.preliminaryStrongApproximationCutoff : ℕ

A fully elementary replacement for the paper's 10^532 threshold.

Equations

• BGS.Markoff.preliminaryStrongApproximationCutoff = ↑BGS.Markoff.preliminaryStrongApproximationCutoffData

theorem BGS.Markoff.preliminaryStrongApproximationCutoff_eq : preliminaryStrongApproximationCutoff = 2 ^ 1833 * (48 ^ 3 + 1) ^ 10 + 1

theorem BGS.Markoff.preliminaryCutoff_gt_one : 1 < preliminaryStrongApproximationCutoff

theorem BGS.Markoff.preliminaryCutoff_constant_lt {p : ℕ} (hp : preliminaryStrongApproximationCutoff ≤ p) : 2 ^ 1833 * (48 ^ 3 + 1) ^ 10 < p

theorem BGS.Markoff.preliminary_divisor_sum_pow_ten_le {p : ℕ} (hp : 2 ≤ p) : ((p - 1).divisors.card + (p + 1).divisors.card) ^ 10 ≤ preliminaryDivisorMomentConstant * p

The two divisor counts needed by the preliminary route satisfy one simultaneous tenth-moment estimate.

theorem BGS.Markoff.preliminary_divisor_sum_lt_rpow_one_div_eight {p : ℕ} (hp : preliminaryStrongApproximationCutoff ≤ p) : ↑((p - 1).divisors.card + (p + 1).divisors.card) < ↑p ^ (1 / 8)

The simultaneous divisor count is smaller than the eighth root of p.

theorem BGS.Markoff.preliminary_corvajaZannier_divisor_term_lt_rpow_one_div_six {p : ℕ} (hp : preliminaryStrongApproximationCutoff ≤ p) : ↑(corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) < ↑p ^ (1 / 6)

The coefficient-48 all-divisors term is smaller than the sixth root of p, as required by the preliminary middle game.

theorem BGS.Markoff.preliminary_weighted_divisor_sum_sq_lt_rpow_one_div_three {p : ℕ} (hp : preliminaryStrongApproximationCutoff ≤ p) : ↑(68 * ((p - 1).divisors.card + (p + 1).divisors.card) ^ 2) < ↑p ^ (1 / 3)

The weighted divisor square is smaller than the one-third power needed by the primitive-trace endgame.

theorem BGS.Markoff.preliminary_small_fixed_lt_rpow_one_div_eight {p fixed : ℕ} (hp : preliminaryStrongApproximationCutoff ≤ p) (hfixed : fixed ≤ 100522) : ↑fixed < ↑p ^ (1 / 8)

Every fixed coefficient used in the cage is smaller than the eighth root of p.

theorem BGS.Markoff.preliminary_middleGame_corvajaZannier_linearBound {p currentOrder : ℕ} (hp : preliminaryStrongApproximationCutoff ≤ p) (hUpper : ↑currentOrder < ↑p ^ (5 / 6)) : corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card) * currentOrder < p

Assembly-facing preliminary middle-game certificate.

theorem BGS.Markoff.preliminary_endgamePrimitiveTrace_explicitInequality {p orbitExponent coefficient : ℕ} (hp : preliminaryStrongApproximationCutoff ≤ p) (horbit : ↑orbitExponent ≤ 2 * ↑p ^ (1 / 6)) (hcoefficient : coefficient ≤ 34) : ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p

Preliminary primitive-trace inclusion--exclusion certificate.

theorem BGS.Markoff.preliminary_endgamePrimitiveTrace_explicitInequality_of_card_sub_one {p orbitExponent orbitOrder coefficient : ℕ} (hp : preliminaryStrongApproximationCutoff ≤ p) (hmul : orbitExponent * orbitOrder = p - 1) (horder : ↑p ^ (5 / 6) ≤ ↑orbitOrder) (hcoefficient : coefficient ≤ 34) : ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p

theorem BGS.Markoff.preliminary_endgamePrimitiveTrace_explicitInequality_of_card_add_one {p orbitExponent orbitOrder coefficient : ℕ} (hp : preliminaryStrongApproximationCutoff ≤ p) (hmul : orbitExponent * orbitOrder = p + 1) (horder : ↑p ^ (5 / 6) ≤ ↑orbitOrder) (hcoefficient : coefficient ≤ 34) : ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p

theorem BGS.Markoff.preliminary_four_lt_rpow_five_div_six {p : ℕ} (hp : preliminaryStrongApproximationCutoff ≤ p) : 4 < ↑p ^ (5 / 6)

theorem BGS.Markoff.preliminary_cageWitness_explicitInequality {p coefficient : ℕ} (hp : preliminaryStrongApproximationCutoff ≤ p) (hcoefficient : coefficient ≤ 100522) : ↑(p - 1).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p

Preliminary cage inequality with the existing point-count coefficient.

theorem BGS.Markoff.preliminary_lowOrder_divisorSensitive_cube {p d : ℕ} (hp : preliminaryStrongApproximationCutoff ≤ p) (hdPos : 0 < d) (hpLe : p ≤ 2 * (2 + d * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 2) : (corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 3 < d

The low-order Corvaja--Zannier cube contradiction, now driven by the elementary tenth moment.