The finite denominator bound
An interval containing 𝑆
excludes rational numbers whose denominators are too small to occur
inside it. The Farey argument below makes this precise using a finite
totient prefix and a bound on its tail. It is independent of the period
and residue criteria.
Lemma 5.4 (Farey gap, fully general). For
integers 𝑎,𝑏,𝑐,𝑑,𝑟,𝑠 with 𝑏 >0, 𝑑 >0, 𝑏𝑐 −𝑎𝑑 =1 (i.e. 𝑎/𝑏 and 𝑐/𝑑 are unimodular Farey neighbours), and
𝑎𝑠 <𝑟𝑏, 𝑟𝑑 <𝑐𝑠 (i.e. 𝑟/𝑠 lies strictly between them): 𝑏 +𝑑 ≤𝑠.
Indeed, the two strict inequalities make 𝑐𝑠 −𝑑𝑟 and 𝑏𝑟 −𝑎𝑠 positive integers, and
𝑠=𝑏(𝑐𝑠−𝑑𝑟)+𝑑(𝑏𝑟−𝑎𝑠)≥𝑏+𝑑,
using 𝑏𝑐 −𝑎𝑑 =1. This also proves 𝑠 >0, which the formulation did not
need to assume separately. The lemma is the classical Stern–Brocot
denominator bound. The mediant (𝑎 +𝑐)/(𝑏 +𝑑) lies between the two
neighbours and is reduced: any common divisor of 𝑎 +𝑐 and 𝑏 +𝑑 divides 𝑏(𝑎 +𝑐) −𝑎(𝑏 +𝑑) =𝑏𝑐 −𝑎𝑑 =1. It attains
denominator 𝑏 +𝑑, so the general
interval bound is sharp. A particular tail interval still requires its
own endpoint and first-failure checks.
Proposition 5.5 (The Farey certificate at 𝐾 =240). For the window (𝑁,𝐾) =(1,240), put
𝑉=(240∑𝑟=1𝜑(1+𝑟)2240−𝑟)mod2240.
For every 𝑞 :ℕ with
0<𝑞≤𝑄0:=79639646646701375323355774875831053(≈7.96×1034),
(𝑞⋅𝑉)mod2240+243𝑞<2240.
This bound is
sharp: 𝑞 =𝑄0 +1 =79 639 646 646 701 375 323 355 774 875 831 054 is
the exact first failing denominator, obtained as the denominator of the
mediant of two explicit unimodular Farey neighbours.
Here “failing” means that this particular enclosure can no longer
exclude the denominator. It does not mean that the mediant equals 𝑆, or that another argument could not
exclude that denominator too. Sharpness concerns the finite interval
test, not a smallest possible denominator for the unknown value.
Theorem 5.6 (Denominator exclusion). For every
𝑝 ∈ℚ whose reduced
denominator is at most 𝑄0,
𝑆≠𝑝.
Equivalently: if 𝑆 is rational, its reduced denominator
exceeds 𝑄0 ≈7.96 ×1034.
Remark 5.7 (What this does and does not say). Theorem 5.6 is a complete,
unconditional finite fact: no rational of denominator at most 𝑄0 equals 𝑆. A single such bound does not exclude
arbitrarily large denominators. Proving unbounded exclusions by the same
mechanism would, however, establish irrationality. The question this
leaves is whether the first failing denominator (𝑏 +𝑑)(𝐾) at window 𝐾 is unbounded as 𝐾 →∞. An affirmative answer would
prove irrationality by Proposition 6.75, independently of the
certificate condition discussed after Proposition 5.3. The question is open;
it is neither claimed nor proved anywhere in the record.
Remark 5.8 (Earlier finite denominator bounds). The recorded
Farey computations gave bounds 4838, 222, approximately 2.49 ×1017 at 𝐾 =120, and 𝑄0 at 𝐾 =240. Each applies the finite mechanism
of Lemma 5.4 and
Proposition 5.5.
These values do not prove that the bounds are unbounded as 𝐾 increases.