Documentation

LeanPool.MarkoffModP.BGS.NumberTheory.JointMaximalDivisorCertificate

Exact certificate at the paper's terminal obstruction #

The published maximal-divisor computation stops at the reduced integer

(863#)(53#)(13#)(7#)(5#) 3^3 2^5.

Its central divisor-lattice coefficient is the paper's exact value C₉₃(n). The paper treats the two neighboring maximal-divisor counts independently and therefore uses the square envelope 4 C^2. The joint p - 1, p + 1 moment instead supplies C^2 + 3J, where the displayed integer J is an exact tenth-root upper certificate.

All comparisons below are closed integer computations checked by Lean.

source
def BGS.NumberTheory.publishedTerminalReducedInteger :
ℕ

The reduced integer responsible for the published cutoff.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def BGS.NumberTheory.publishedTerminalCentralCoefficient :
    ℕ

    The exact value C₉₃(n) reported in the paper.

    Equations
    Instances For
      source
      def BGS.NumberTheory.publishedTerminalJointProductEnvelope :
      ℕ

      A tenth-root upper certificate for the joint neighboring divisor count.

      Equations
      Instances For
        source
        def BGS.NumberTheory.publishedTerminalJointSquareEnvelope :
        ℕ

        The new squared-sum envelope C^2 + 3J.

        Equations
        Instances For
          source
          theorem BGS.NumberTheory.publishedTerminalJointProductEnvelope_certificate :
          2 ^ 457 * (publishedTerminalReducedInteger + 1) ^ 2 ≤ publishedTerminalJointProductEnvelope ^ 10

          The displayed J really dominates the joint tenth-moment radicand. The slightly looser (n + 1)^2 form avoids any hidden square-root rounding.

          source
          theorem BGS.NumberTheory.publishedTerminalJointSquareEnvelope_succeeds :
          3 ^ 8 * publishedTerminalJointSquareEnvelope ^ 4 ≤ 32 * (publishedTerminalReducedInteger + 2)

          The new envelope makes the paper's first-interval obstruction empty at the exact reduced integer that caused the published algorithm to stop.

          source
          theorem BGS.NumberTheory.publishedTerminalIndependentSquareEnvelope_fails :
          32 * (publishedTerminalReducedInteger + 2) < 3 ^ 8 * (4 * publishedTerminalCentralCoefficient ^ 2) ^ 4

          In contrast, the paper's independent envelope 4C^2 fails at this same integer. This records that the improvement is structural, not a re-rounding of the published computation.