Solving Diophantine equations completely: reduction, lattices and certificates

Written by GPT-6 Astra (OpenAI) in Codex, Ultra setting, October 2026. Self-checked by the writing AI. Public domain (CC0).

A large effective bound and a list of small solutions answer different questions. The bound limits every possible solution; the list records what a finite search found. A complete resolution connects them by a proved reduction and an exhaustive search over the resulting range. This lesson builds that connection for two exponential equations, and gives an exact three-logarithm lattice certificate.

We use Two logarithms II: explicit lower bounds, Theorem 7.1, for the initial analytic estimate, and Powers of 2 and 3, Theorem 11.3 and equation (11.13), for Legendre's criterion and rational logarithm intervals. The first equation also reproduces Theorem 11.4 there. The lattice arguments, reduction lemmas, finite searches and their certification are proved below.

1. From an equation to a finite certificate

Suppose an equation yields a nonzero logarithmic form \(\Lambda=b_1\log\alpha_1+\cdots+b_r\log\alpha_r\) and an upper bound that decreases exponentially in a size parameter \(X\). An explicit lower bound for \(|\Lambda|\) first gives \(X\le X_0\). The inequality may make \(X_0\) too large for direct enumeration. A continued-fraction calculation or a lattice calculation can then give a much stronger lower bound for this particular form, throughout the finite coefficient range. Comparing the two bounds reduces \(X\). Finally one checks every remaining possibility using exact arithmetic.

Each transition has its own mathematical obligation. The logarithmic form must be nonzero; the analytic theorem's heights, degree and coefficient parameter must be correct; the reduction must apply to every possible coefficient vector; and the last search must exhaust the proved range. Numerical precision also belongs in the proof: a decimal that appears positive does not certify a strict inequality.

For two logarithms, division by one of them leads to \(|m-n\theta|\). If \(m/n=a/b\) in lowest terms and

then \(b\le n\), so Legendre's criterion makes \(a/b\) a convergent of \(\theta\). Writing \(m=ga,n=gb\) gives

Thus a lower bound for the reduced convergent's error also bounds the original error. This common factor is essential when using convergents to enumerate all possibilities.

An additive term changes the problem to \(u\theta-v+\mu\). The distance-to-integers argument in the next section handles it. With three or more logarithms, an integer lattice records several coefficients at once.

2. An inhomogeneous continued-fraction reduction

For a real number \(x\), let \(\|x\|=\min_{k\in\mathbb Z}|x-k|\). Choosing nearest integers proves \(\|x+y\|\le\|x\|+\|y\|\), and, for an integer \(u\), \(\|ux\|\le |u|\|x\|\). These inequalities are useful even when the nearest integers are not known individually.

Lemma 21.1 (Baker–Davenport reduction). Let \(M\ge1\) and \(q\ge1\) be integers, \(\theta,\mu\) real, \(A>0\), and \(B>1\). Put

If \(\epsilon>0\), there are no integers \(u,v,w\) satisfying

Proof. Multiplication by \(q\), invariance under integer translation, and the preceding triangle inequality give

Consequently \(\epsilon<qAB^{-w}\). Taking logarithms and dividing by the positive number \(\log B\) gives the strict opposite of the last inequality in (21.2). \(\square\)

In practice \(q\) is a convergent denominator of an irrational \(\theta\), since this tends to make \(\|q\theta\|\) small. The common choice \(q>6M\) is a search rule, not a hypothesis used by this proof and not a guarantee that \(\epsilon>0\). Certified intervals must establish that strict positivity. The argument also proves the endpoint exclusion in (21.2), because the small-linear-form inequality is strict. The author version of Dujella and Pethő, Generalization of a theorem of Baker and Davenport, Lemma 5(a), gives the familiar convergent formulation.

3. What an LLL certificate proves

Let \(z_1,\ldots,z_n\) be linearly independent integer vectors in \(\mathbb R^n\). Their lattice is \(\Gamma=\sum_i\mathbb Zz_i\). Define the Gram–Schmidt vectors and coefficients by

The vectors \(z_i^*\) are mutually orthogonal: taking the inner product with an earlier \(z_j^*\) cancels exactly its projection term. Induction also gives equality of the first \(i\) spans. All entries in (21.3) are rational and can be checked exactly.

A basis is LLL reduced with parameter \(3/4\) if

Proposition 21.2 (the shortest-vector guarantee). An LLL reduced basis satisfies

For any basis, the possibly stronger certified bound \(\|x\|_2^2\ge\min_jd_j\) holds.

Proof. Write \(x=\sum_i k_i z_i\), with integers \(k_i\), and let \(j\) be the largest index with \(k_j\ne0\). Projection on the orthogonal complement of the first \(j-1\) basis vectors sends \(x\) to \(k_jz_j^*\). Hence \(\|x\|_2^2\ge k_j^2d_j\ge d_j\), proving the assertion for an arbitrary basis. Conditions (21.4) give \(d_i\ge d_{i-1}/2\). Thus \(d_j\ge2^{-(j-1)}d_1\ge2^{-(n-1)}\|z_1\|_2^2\), which proves (21.5). \(\square\)

This is the guarantee of Lenstra, Lenstra and Lovász, Factoring polynomials with rational coefficients, Proposition (1.11). The computed first vector is an upper bound for the shortest length; (21.5) supplies the lower bound needed below.

Proposition 21.3 (exact reduction terminates). Integer row operations consisting of size reductions and adjacent swaps produce a basis satisfying (21.4) in finitely many steps.

Proof. Work at an index \(k\), initially two. In decreasing order of \(j=k-1,\ldots,1\), replace \(z_k\) by \(z_k-rz_j\), where \(r\) is a nearest integer to the current \(\mu_{kj}\). This makes \(|\mu_{kj}|\le1/2\); later reductions with smaller indices do not change it. The operation preserves the integer lattice, and its inverse adds \(rz_j\). If the adjacent inequality in (21.4) holds, increase \(k\). Otherwise exchange \(z_{k-1},z_k\) and restart at \(\max\{2,k-1\}\). Terminate when \(k=n+1\). At each stage the earlier prefix is reduced; hence termination gives all of (21.4).

Here is a decreasing integer that proves termination. Put

The determinant identity follows by the triangular Gram–Schmidt change of basis, whose determinant is one. Each \(D_i\) is a positive integer. Size reductions preserve every prefix lattice and hence every \(D_i\). A swap at \(k\) preserves every factor except \(D_{k-1}\). Projecting the new \((k-1)\)-st vector on the orthogonal complement of the first \(k-2\) vectors shows that the ratio of the new factor to the old is

Thus each swap reduces the positive integer \(\mathcal P\) by a factor below \(3/4\). There are finitely many swaps. Between swaps the index increases after finitely many size reductions, so the entire algorithm terminates. For \(n=1\) there is nothing to do. \(\square\)

For a certificate, record the integer change-of-basis matrix as well as the output basis. A determinant of \(\pm1\) and the exact basis identity certify equality of lattices. Exact values of the rational \(\mu_{ij}\) and \(d_i\) then certify (21.4). No floating-point claim of “LLL reduced” is needed.

4. A lattice lower bound for a logarithmic form

Lemma 21.4 (de Weger-type reduction). Let \(\alpha_j>0\), \(C>0\), \(X_0\ge0\), and \(b_j\in\mathbb Z\) with \(|b_j|\le X_0\), not all zero. Set \(\Lambda=\sum_jb_j\log\alpha_j\). Let \(A_C\) be the integer matrix whose first \(n-1\) rows are the corresponding rows of the identity matrix and whose last row is \((\lfloor C\log\alpha_1\rfloor,\ldots, \lfloor C\log\alpha_n\rfloor)\). Suppose \(A_C\) is nonsingular and every nonzero vector of \(\Gamma=A_C\mathbb Z^n\) has Euclidean norm at least \(l_0\). If \(l_0^2>(n-1)X_0^2\), then

Proof. The vector \(A_Cb\) is nonzero by nonsingularity. Its first \(n-1\) coordinates are \(b_1,\ldots,b_{n-1}\); write its last coordinate as \(s\). Thus \(l_0^2\le\|A_Cb\|_2^2\le(n-1)X_0^2+s^2\), giving the square-root lower bound for \(|s|\). On the other hand,

The ordinary triangle inequality now proves (21.7). \(\square\)

The determinant of \(A_C\) is \(\lfloor C\log\alpha_n\rfloor\). Thus \(\alpha_n\ne1\) alone does not certify nonsingularity for an arbitrarily small \(C\); check the actual integer. Also, the right side of (21.7) must be positive before it gives useful information. The sufficient condition is \(l_0^2>(n^2+n-1)X_0^2\).

Corollary 21.5 (combining the two directions). Suppose in addition that \(0<|\Lambda|<A\exp(-\lambda X)\), with \(A,\lambda>0\), and that the right side \(E\) of (21.7) is positive. Then

Proof. We have \(0<E/C\le|\Lambda|<A\exp(-\lambda X)\). Take logarithms and rearrange. \(\square\)

The small upper bound comes from the original Diophantine equation. A bound \(|b_j|\le X_0\) by itself does not imply a smaller bound for the coefficients. The lattice supplies a lower bound for the linear form, which must be compared with that additional upper bound.

5. Two complete exponential resolutions

All exponents in this section are positive integers. We resolve

The first calculation reproduces the earlier continued-fraction certificate; the second uses the same steps with different exact data. In both cases unique prime factorization ensures that the two powers are unequal and that their logarithmic form is nonzero.

5.1. The powers of two and three

Theorem 21.6. All solutions of the first inequality in (21.9) are

There are no solutions with \(n\ge6\).

Proof: initial bound. For \(n\ge4\), the argument of Theorem 11.4 gives \(m\ge6\), \(n<m\), and

For completeness, \(2^m\ge3^4-20=61\); if \(n\ge m\), then \(3^n-2^m\ge3^m-2^m>20\). For positive \(x,y\), integration gives \(|\log x-\log y|\le |x-y|/\min(x,y)\). Apply this with \(x=2^m,y=3^n\) and use \(20/2^m\le5/16\). The resulting constant is \(20/(1-5/16)=320/11<30\).

Theorem 7.1 with field degree one, height parameters \(a_1=1,a_2=\log3\), and coefficients \(m,-n\), gives

Indeed \(h(2)=\log2<1\), \(h(3)=\log3>1\), and the theorem's coefficient parameter is \(m/\log3+n<2m\). For \(x\ge10^7\), set

The rational bounds \(\log2>69/100,\ \log3<11/10,\ \log(2\cdot10^7)<17,\ \log30<4\) give \(F_3(10^7)>33356>0\). Also \(\log(2x)/x\) decreases there, and hence

The maximum in (21.11) equals \(\log(2x)\) on this range. Therefore \(m<10^7\).

Proof: reduction. For \(n\ge6\),

The last inequality holds at six because \((69/100)(3^6-20)>40\cdot6\). The quantity \((3^n-20)/n\) increases: the numerator of its successive difference is \((2n-1)3^n+20>0\). Legendre therefore applies to \(a/b=m/n\) in lowest terms, and the reduced numerator satisfies \(a<10^7\).

The table lists every eligible convergent and the first excluded one. The sign is that of \(p_j\log2-q_j\log3\), and each integer \(L_j\) satisfies \(10^8|p_j\log2-q_j\log3|>L_j\).

All rows before the last have \(L_j\ge1\), and subsequent numerators are larger still. Multiplication by the common factor \(g\ge1\) does not decrease the error. Thus

Together with the upper bound \(20/(3^n-20)\), this gives \(3^n<2000000020\). Since \(3^{20}=3486784401\), every solution has \(n\le19\). Cases below six are checked separately below.

For \(6\le n\le19\), let \(k=\lfloor\log_2(3^n)\rfloor\). The following exact integers give the distances to the powers on either side of \(3^n\).

Every distance exceeds twenty. Every other power is farther away, so this excludes the whole range. For \(1\le n\le5\), enumerate every positive \(m\) with \(2^m\le3^n+20\), which is a finite integer test. The successful values are exactly (21.10). Their signed differences \(2^m-3^n\), in the order shown, are

The full small-exponent search, including its excluded entries, is recorded in the certificate. This proves the theorem. \(\square\)

5.2. The powers of two and five

Theorem 21.7. All solutions of the second inequality in (21.9) are

There are no solutions with \(n\ge4\).

Proof: initial bound. Suppose first that \(n\ge3\). Then \(2^m\ge125-20=105\), so \(m\ge7\). If \(n\ge m\), then \(5^n-2^m\ge5^m-2^m>20\), a contradiction. Put \(\Lambda=m\log2-n\log5\ne0\). Integration as above gives

The middle inequality uses \(20/2^m\le5/32\). Apply Theorem 7.1 with \(D=1\), \(a_1=1\), \(a_2=\log5\). The height conditions hold, and \(B'=m/\log5+n<2m\). Consequently

This implies \(m<2\cdot10^7\). To check the entire excluded interval, define \(F_5(x)=x\log2-21600\log5\log^2(2x)-\log24\). Use \(\log5<17/10\), \(\log(4\cdot10^7)<18\) and \(\log24<4\). At \(x=2\cdot10^7\) these give

As before, \(\log(2x)/x\) decreases, so the derivative remains positive. The maximum in (21.16) is \(\log(2x)\) throughout this interval. Thus (21.16) is impossible there.

Proof: reduction. For \(n\ge4\),

At four the last inequality follows from \((69/100)(5^4-20)>40\cdot4\). The numerator of the successive difference of \((5^n-20)/n\) is \((4n-1)5^n+20>0\), so the inequality persists. The reduced fraction \(a/b=m/n\) is therefore a convergent of \(\log5/\log2\), with \(a<2\cdot10^7\).

The following table has the same meaning as before, with \(L_j<10^8|p_j\log2-q_j\log5|\).

The last numerator exceeds \(2\cdot10^7\); every earlier row has \(L_j\ge1\). The same common-factor argument gives \(|\Lambda|>10^{-8}\). Hence \(5^n<2000000020\), and

For \(4\le n\le13\), the exact nearest-power distances are:

All entries exceed twenty. For \(n=1,2,3\), check every \(m\ge1\) with \(2^m\le5^n+20\); the upper endpoints for \(m\) are respectively four, five and seven. The successful differences are

giving exactly (21.14). \(\square\)

5.3. Why the numerical tables are proofs

For a rational \(x>1\), put \(z=(x-1)/(x+1)\). The positive series and geometric remainder proved in (11.13) give

Use \(N=100\) for \(x=2,3,5\). Start the continued-fraction calculation with the interval

At each step both endpoints have the same integer part. Subtract that integer and invert the interval, reversing its endpoints. This certifies every partial quotient in the two tables.

The error interval for a row \(a,b\) is \([aL_N(2)-bU_N(p),aU_N(2)-bL_N(p)]\). It lies strictly on one side of zero. Multiplying its distance from zero by \(10^8\) and taking the integer part produces the printed \(L_j\). The recurrence \(p_j=a_jp_{j-1}+p_{j-2}\), \(q_j=a_jq_{j-1}+q_{j-2}\), with \((p_{-2},p_{-1})=(0,1)\) and \((q_{-2},q_{-1})=(1,0)\), gives all table entries. Their determinant identities \(|p_jq_{j-1}-p_{j-1}q_j|=1\) are also checked.

For the scalar logarithm bounds, (21.19) certifies \(69/100<\log2<7/10\), \(1<\log3<11/10\) and \(1<\log5<17/10\). Positive exponential partial sums give

These are finite rational comparisons. Also \(2x\ge2\cdot10^7>2^{20}\) at either initial endpoint, so \(\log(2x)>20(69/100)>10\). No floating-point estimate is used to certify these inequalities.

The equation certificate program reconstructs the intervals, convergents, analytic margins and final integer searches. Its machine-readable data include all successful and unsuccessful small-exponent tests. The preceding proofs explain why those finite tests settle (21.9) for arbitrarily large positive exponents.

6. A three-logarithm certificate from \(10^{20}\)

Consider

We first bound \(|\Lambda|\) uniformly on this coefficient range. Then we show precisely what follows if the equation under study also gives \(|\Lambda|<e^{-X}\).

Choose \(C=10^{70}\), and put \(N_p=\lfloor C\log p\rfloor\). The following expressions give each integer exactly, split into two blocks of decimal digits:

These floors are certified as follows. For \(p=2,3,5\), write \(p=2^k y\) with \(1\le y<2\). Use (21.19) with 240 terms for \(\log2\) and \(\log y\), and add \(k\) times the former interval to the latter. If \(y=1\), its interval is exactly zero. The resulting rational interval \([\ell_p,u_p]\) satisfies

Both endpoints are given as exact rational numbers in the lattice certificate data. The certified floors, rather than rounded decimal logarithms, are the integers used in the lattice.

Take the matrix

Its determinant is \(N_5>0\). For the reduction calculation we store its column generators as the rows of \(B=A_C^{\mathsf T}\). Integer row operations give the following reduced basis. Each displayed tuple is a row of \(Z\).

To certify that these vectors generate the original lattice, use the integer matrix \(U\) with the following rows.

Direct integer multiplication gives \(Z=UB\), and \(\det U=1\). Thus \(U\) and its inverse have integer entries and the two sets of rows generate exactly the same lattice. The inverse is integral because the adjugate identity expresses it as the integer adjugate divided by \(\det U=1\).

The rational Gram–Schmidt calculation (21.3) on \(Z\) satisfies all three inequalities \(|\mu_{ij}|\le1/2\) and both Lovász inequalities (21.4). The exact reduction program records the rational numerators and denominators for each of these checks. It also replays every integer row operation: there are 126 nonzero size reductions and 110 swaps. Each reduction preserves the integer potential (21.6), and each swap decreases it by a factor strictly below \(3/4\). These checks give both a reproducible construction and a certificate of the final basis. The final basis identity and inequalities alone are sufficient to use Proposition 21.2.

Proposition 21.8. Every coefficient vector in (21.20) satisfies

If, in addition, \(0<|\Lambda|<e^{-X}\), then

Proof. Proposition 21.2 with \(n=3\) permits

Let

Exact squaring gives

Therefore the square root in (21.7), minus the rounding error \(3X_0\), is at least \(E_0>0\). Lemma 21.4 now gives

which proves (21.22). If the additional upper bound holds and \(X\ge120\), then

a contradiction. For the last strict comparison, \(e>1+1+1/2+1/6=8/3\), and the integer comparison \(8^{120}>10^{48}3^{120}\) proves \((8/3)^{120}>10^{48}\). Thus \(X<120\), giving (21.23) because \(X\) is an integer. \(\square\)

The condition \(0<|\Lambda|<e^{-X}\) is an explicit assumption in the second conclusion. A coefficient bound alone cannot imply that all coefficients are small: for example \((b_1,b_2,b_3)=(10^{20},0,0)\) belongs to the initial box. For another Diophantine problem its own upper bound \(A e^{-\lambda X}\) can instead be inserted in (21.8).

The matrix construction and comparison of its last coordinate with the logarithmic form are the mechanism used in de Weger, Algorithms for Diophantine Equations, original doctoral thesis, Section 3.7, Lemma 3.7 and equation (3.23), printed pages 57–59. Here the horizontal scale is one, all rounding is downward, and Lemma 21.4 keeps the square-root expression explicit.

Figure 21.1. Left: exact distances from \(5^n\) to the adjacent powers of two for \(4\le n\le13\); the entire interval is excluded by Theorem 21.7. The horizontal dashed line is the allowed distance 20. Right: the proved lattice lower bound \(10^{-48}\) and the additional upper bound \(e^{-X}\), displayed on a logarithmic vertical scale. The sampled curve illustrates Proposition 21.8; the exclusion at integer \(X=120\) is proved by the exact comparison \(8^{120}>10^{48}3^{120}\), not by the plot. Figure program.

7. Exercises and complete solutions

1. Easy: the distance lemma. Prove Lemma 21.1 directly. Determine whether a convergent hypothesis, \(q>6M\), or a strict exclusion threshold for \(w\) is necessary.
2. Medium: a homogeneous certificate. Implement the continued-fraction reduction for \(m\log2-n\log3\) using rational arithmetic. Reproduce the convergents and the final range of Theorem 11.4. Explain why reducing \(m/n\) to lowest terms loses no solutions, and resolve the positive exponents with \(n<4\).
3. Medium: the lattice lemma. Prove (21.7). Identify the precise purpose of nonsingularity and give a sufficient condition for its right side to be positive.
4. Hard: an exact LLL reduction. For the form in (21.20), start from \(X_0=10^{20}\), choose \(C\), and certify a lattice lower bound. Assuming also \(0<|\Lambda|<e^{-X}\), reduce the coefficient range. Record enough exact information to reconstruct every rounding and every basis operation.

Solution 1. Let \(t\in\mathbb Z\) be nearest to \(q\theta\). The identity

has integer final term. Taking distance to the integers gives

Thus \(\epsilon<qAB^{-w}\). If \(w\ge\log(Aq/\epsilon)/\log B\), then \(qAB^{-w}\le\epsilon\), a contradiction. Neither a convergent nor \(q>6M\) was used. The endpoint is excluded because the original upper bound is strict. The essential numerical condition is \(\epsilon>0\); if it fails, this argument gives no exclusion.

Solution 2. Compute the two intervals (21.19) with \(N=100\). Apply integer-part extraction and reversed reciprocal intervals to their ratio. Starting from the four recurrence values in Section 5.3, the partial quotients through the first excluded numerator are

The last eligible numerator and denominator are \(301994,190537\); the next pair is \(16785921,10590737\), so its numerator violates the proved strict bound \(m<10^7\). The least printed \(L_j\) among eligible rows is six, which is more than needed for the uniform error \(10^{-8}\). For \(m=gp,n=gq\), the logarithmic form is \(g\) times the reduced error. Since \(g\ge1\), the uniform lower bound remains valid. The upper bound \(20/(3^n-20)\) then gives \(n\le19\). Exact integer comparisons for \(4\le n\le19\) yield only \((m,n)=(6,4),(8,5)\). For \(n=1,2,3\), enumerate \(1\le m\le \lfloor\log_2(3^n+20)\rfloor\), using integer bit lengths. The successful sets are respectively \(\{1,2,3,4\}\), \(\{1,2,3,4\}\) and \(\{3,4,5\}\), as in (21.10). The linked equation program implements these operations with integers and fractions and checks every printed convergent.

Solution 3. Put \(v=A_Cb\) and write its last coordinate as \(s=\sum b_j\lfloor C\log\alpha_j\rfloor\). Nonsingularity and \(b\ne0\) ensure \(v\ne0\), so

The hypothesis makes the resulting lower bound \(|s|\ge\sqrt{l_0^2-(n-1)X_0^2}\) real and positive. Each floor introduces an error less than one, hence \(|s-C\Lambda|\le nX_0\). Subtract this error using the triangle inequality to obtain (21.7). Its right side is positive exactly when \(l_0^2>(n^2+n-1)X_0^2\). The weaker displayed hypothesis in Lemma 21.4 is enough for the inequality, but may leave a nonpositive lower bound.

Solution 4. Choose \(C=10^{70}\). The 240-term intervals in Section 6 certify all three floors and hence the integer matrix \(A_C\). Execute size reductions using nearest integers to the exact Gram–Schmidt fractions, and swap only when the exact Lovász inequality fails. Carry the same row operations on the identity matrix to obtain \(U\). The program records 236 operations, including 110 swaps, and verifies every potential comparison. Its output is the displayed basis \(Z\) and \(\det U=1\). Check \(Z=UA_C^{\mathsf T}\), the three size inequalities, and the two Lovász inequalities. Proposition 21.2 gives \(l_0^2=\|z_1\|^2/4\). The exact square-root bracket in Proposition 21.8 then gives \(C|\Lambda|\ge103179593767043471534146>C10^{-48}\). The assumed upper bound rules out \(X\ge120\), since \(8^{120}>10^{48}3^{120}\) and \(e>8/3\). Thus the reduced integer bound is \(X\le119\). Without the additional upper bound the certified conclusion is \(|\Lambda|>10^{-48}\), not a smaller coefficient range.

8. What to retain with a complete resolution

A reproducible certificate has four connected parts:

1. The equation, domain, logarithmic form and proof of nonvanishing, followed by the exact analytic theorem, its parameters and the resulting initial bound.
2. Rational logarithm intervals, their remainder estimates, and either all required convergents or the integer lattice matrix, change of basis and rational Gram–Schmidt checks.
3. The comparison proving the reduced bound, with strict endpoints and common factors handled explicitly.
4. The exhaustive integer search range and its complete output, including the small cases excluded from earlier inequalities.

For the two equations, the certificate data contain all these finite checks and the proofs above supply the analytic implications. For the lattice example, the data also contain every elementary operation and the positive integer potential that decreases at swaps. All programs use the Python standard library for their proof checks. The figure uses numerical coordinates only to illustrate inequalities already proved exactly.

What this lesson uses from earlier lessons

Theorem 7.1 supplies the explicit two-logarithm lower bound with constant \(21600\). Theorem 11.3 supplies Legendre's criterion, and equation (11.13) supplies the rational logarithm intervals. These results are proved in the linked earlier lessons. Theorem 11.4 is reproduced here, including its finite reduction. No external citation replaces a reduction proof or a search exhaustiveness argument in this lesson.

Freely accessible sources

• A. Dujella and A. Pethő, Generalization of a theorem of Baker and Davenport, Lemma 5(a), author version.
• A. K. Lenstra, H. W. Lenstra, Jr., and L. Lovász, Factoring polynomials with rational coefficients, Section 1, especially Proposition (1.11), free university-hosted paper.
• B. M. M. de Weger, Algorithms for Diophantine Equations, original doctoral thesis (1988), Chapter 3, Section 3.7, free author-hosted chapter.