Documentation

LeanPool.MarkoffModP.BGS.Markoff.ExplicitNumerics

Closed numerical bounds for explicit strong approximation #

All constants in this file are closed natural-number expressions. In particular, no witness is extracted from an eventual or asymptotic theorem.

The first explicit record is retained in a namespace for comparison.

source
@[irreducible]
noncomputable def BGS.Markoff.Legacy.explicitStrongApproximationCutoffData :
{ n : ℕ // n = NumberTheory.explicitDivisorConstant + 1 }

Sealed data for the deliberately conservative project cutoff.

Equations
Instances For
    source
    noncomputable def BGS.Markoff.Legacy.explicitStrongApproximationCutoff :
    ℕ

    The deliberately conservative project cutoff. It is not the primorial constant from arXiv:2308.07579.

    Equations
    Instances For
      source
      theorem BGS.Markoff.Legacy.explicitStrongApproximationCutoff_eq :
      explicitStrongApproximationCutoff = NumberTheory.explicitDivisorConstant + 1
      source
      theorem BGS.Markoff.Legacy.explicitCutoff_gt_one :
      1 < explicitStrongApproximationCutoff
      source
      theorem BGS.Markoff.Legacy.fixed_lt_rpow_one_div_thirtyTwo_of_explicitCutoff {p fixed : ℕ} (hp : explicitStrongApproximationCutoff ≤ p) (hfixed : fixed ^ 32 ≤ NumberTheory.explicitDivisorConstant) :
      ↑fixed < ↑p ^ (1 / 32)
      source
      theorem BGS.Markoff.Legacy.small_fixed_lt_rpow_one_div_thirtyTwo_of_explicitCutoff {p fixed : ℕ} (hp : explicitStrongApproximationCutoff ≤ p) (hfixed : fixed ≤ 100522) :
      ↑fixed < ↑p ^ (1 / 32)
      source
      theorem BGS.Markoff.Legacy.explicit_divisor_sum_le_three_mul_rpow {p : ℕ} (hp : explicitStrongApproximationCutoff ≤ p) :
      ↑((p - 1).divisors.card + (p + 1).divisors.card) ≤ 3 * ↑p ^ (1 / 16)

      Both divisor counts occurring in the all-divisors Corvaja--Zannier union bound are controlled by one sixteenth root of p.

      source
      theorem BGS.Markoff.Legacy.explicit_corvajaZannier_divisor_term_le {p : ℕ} (hp : explicitStrongApproximationCutoff ≤ p) :
      ↑(corvajaZannierCorollaryTwoSafeCoefficient * ((p - 1).divisors.card + (p + 1).divisors.card)) ≤ 144 * ↑p ^ (1 / 16)

      The coefficient-48 all-divisors term used by the middle game.

      Ninth-moment adaptive cutoff #

      source
      @[irreducible]
      def BGS.Markoff.explicitDivisorMomentConstantData :
      { n : ℕ // n = 2 ^ 9 * (9 ^ 9) ^ 2 ^ 9 }

      The coefficient in the simultaneous ninth-moment bound for the divisor counts of p - 1 and p + 1.

      Instances For
        source
        def BGS.Markoff.explicitDivisorMomentConstant :
        ℕ

        The explicit constant bounding the divisor moment in the numerical argument.

        Equations
        Instances For
          source
          theorem BGS.Markoff.explicitDivisorMomentConstant_eq :
          explicitDivisorMomentConstant = 2 ^ 9 * (9 ^ 9) ^ 2 ^ 9
          source
          theorem BGS.Markoff.explicitDivisorMomentConstant_pos :
          0 < explicitDivisorMomentConstant
          source
          @[irreducible]
          noncomputable def BGS.Markoff.explicitStrongApproximationCutoffData :
          { n : ℕ // n = 2 ^ 9 * (48 ^ 3 + 1) ^ 18 * explicitDivisorMomentConstant ^ 8 + 1 }

          Sealed data for the improved project cutoff.

          Equations
          Instances For
            source
            noncomputable def BGS.Markoff.explicitStrongApproximationCutoff :
            ℕ

            The explicit project cutoff. It is deliberately different from the primorial constant in arXiv:2308.07579.

            Equations
            Instances For
              source
              theorem BGS.Markoff.explicitStrongApproximationCutoff_eq :
              explicitStrongApproximationCutoff = 2 ^ 9 * (48 ^ 3 + 1) ^ 18 * explicitDivisorMomentConstant ^ 8 + 1
              source
              theorem BGS.Markoff.explicitCutoff_gt_one :
              1 < explicitStrongApproximationCutoff
              source
              theorem BGS.Markoff.explicitCutoff_constant_lt {p : ℕ} (hp : explicitStrongApproximationCutoff ≤ p) :
              2 ^ 9 * (48 ^ 3 + 1) ^ 18 * explicitDivisorMomentConstant ^ 8 < p
              source
              theorem BGS.Markoff.explicit_divisor_sum_pow_nine_le {p : ℕ} (hp : 2 ≤ p) :
              ((p - 1).divisors.card + (p + 1).divisors.card) ^ 9 ≤ explicitDivisorMomentConstant * p

              The elementary factorization estimate, specialized to the simultaneous ninth moment needed below.

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

              The complete coefficient-48 divisor term lies below the sixth root of p. This is the linear middle-game estimate used up to order p^(5/6).

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

              The weighted square of the simultaneous divisor count lies below the one-third power needed by the primitive endgame.

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

              The simultaneous divisor count itself remains below the eighth root of p; this sharper unweighted estimate is retained for the cage.

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

              Every fixed coefficient used by the explicit proof is also below the eighth root of p.