S1 r_(m+1)/r_m = (x+1)(1+1/x)^x/(e(x+1/2)) with m! = Gamma(x+1/2): True
S2 (x+1/2)/(x+1) = 1 - y, y = 1/(2x+2), so ln(ratio) < 0 iff x ln(1+1/x) < 1 + ln(1-y): True
S3 y(3/2) = 1/5 and y decreases in x, so y in (0, 1/5] for m >= 1: True
S4 Pade: h(t) = t(6+t)/(6+4t) - ln(1+t) has h(0) = 0 and h' = 4t^3/((6+4t)^2(1+t)): True
S5 x * pade(1/x) = 1 - 3/(6x+4) = 1 - y/(1-2y/3): True
S6 g(y) = ln(1-y) + y/(1-2y/3) has g(0) = 0 and g' = (y/3)(1-4y/3)/((1-y)(1-2y/3)^2): True
S7 ln(2 sqrt(l) e^-l)'' = -1/(2 l^2) < 0, critical point l = 1/2: True
S8 (ln f_m)' = (m+1/2)/l - 1: True
I1 (sanity) Pade bound h(t) > 0 certified at t = i/1000, i = 1..20000: 0 failures
I2 (sanity) g(y) > 0 certified at y = i/10000, i = 1..2000: 0 failures
I3 r_1 = 0.8198325579 < 0.82; f_0(0.32) = 0.8215438532 > 0.82; f_0(0.74) = 0.8208578181 > 0.82; 1 - e^-0.42 = 0.3429531802 > 0.3429: True
E1 s in [0.001, 0.42], 4,000 points, k with ks <= 12: argmax has ks >= 1 at 0 points; A(s) <= 0.82 at 0; min of A(s) - max_(1 <= ks <= 12) ratio = 0.0164446
E2 max |q A(s)^2/((1-q)s) - M(q)^2| = 2.5e-29 (so APC(s(q)) gives R(q) <= M(q), i.e. C0)
E3 (info, outside the claim) s = 0.5: A(s) = 0.85776388 at ks = 0.5
E3 (info, outside the claim) s = 0.8: A(s) = 0.81721965 at ks = 1.6
E3 (info, outside the claim) s = 1.2: A(s) = 0.80950838 at ks = 2.4
RESULT: ALL CHECKS PASSED

real	0m15.732s
user	0m15.687s
sys	0m0.044s
