OK   [Q] sum_{j>=1} 4^-j/((j+1)!)^2 < 0.0643  = 0.064263511
OK   [Q] arcsin(0.0643) < 0.07  0.0644333
OK   [T1] 1 - 2 eps_-(5) - (1+eps_+(5))/(20 pi) > 0.81  = 0.813334
OK   [T1'] e^10 > 520 pi  22026.47 vs 1633.63
OK   [T2] 1 - (1+eps_-(60))/2 - (1+eps_+(60))/sqrt(120 pi) > 0.44  = 0.444987
OK   zone (A): 1 - eps_-(5) > 0 (bound increases in |u|)  
OK   [T3] delta_1(60) < 0.0186  = 0.0185033
OK   [T3] delta(60) < 0.0095  = 0.00942376
OK   [T3] 60 lambda(60) < 0.5709  = 0.5708046
OK   [T3] (120/119) lambda(60) < 0.0097  = 0.00959335
OK   [T3] -ln(1 - delta(60)) <= lambda(60)  
OK   [T3'] 60 - pi/4 - lambda(60) > 18 pi  59.20509 > 56.54867
OK   [T3''] 20 pi > 60  
OK   [T4] (120/119) 60 lambda(60) 20pi/(20pi - 0.0097) < 0.576  = 0.5756902
OK   [T5'] 20 pi - 1/(20 pi) > 60  62.815938
OK   [T5''] ln(40 pi^2)/2 - 1/(20 pi) > 0  2.97325
OK   discs disjoint: 2 pi - pi/4 > 2 rho_10  
OK   [T5'''] e^0.4 (0.4 + 0.08) < 1  (t - t^2 e^t/2 increasing on [0, 0.4])  0.716076
OK   [T5] sigma_+ < 0.0161 at m=10  = 0.0160481
OK   [T5] (2 pi m)|E| bound < 0.5641 at m = 10  = 0.5640733
OK   [T5] (2 pi m)|u-1| bound > 0.9837 at m = 10  = 0.9837165
OK   [T5] sigma_+ < 2 pi (uniqueness of the zero of u - 1)  
OK   v(10) > 0  = 2.48917
OK   [T6] 100 G(10) > 0.3196  = 0.3196708
OK   [T6'] 1/(4 pi^2 m^2) <= 0.0003 at m = 10  = 0.0002533
OK   [T6''] arcsin x <= 1.0001 x on [0, 0.0003] (arcsin x <= x/sqrt(1-x^2))  
OK   [T6'''] ln(44 pi^2) > 2  = 6.07365
OK   2 * 1.0001/(4 pi^2) <= 0.0507  = 0.0506657
OK   0.3196 - 0.0507 > 0  
OK   Lemma 3.2(b): 2y - ln(2 sqrt(2) pi y) > 0 at y = 20 pi  
OK   [T7] ln(2 pi (20.25 pi + 3.0193))/2 - 3.0193 < 0  = -0.000734845
OK   pi_- = 3.14159265358979 < pi  
OK   Lemma 3.6: 20 pi - 1/(20 pi) > 20 pi_- - 0.016  
OK   Lemma 3.6: 3.0193 + 1/(20 pi) < 3.0353  
OK   Lemma 3.6: arg b* < 0.04829  arg b* = 0.0482830496
OK   per-m: localisation (2 pi m)(120/119) lambda(2 pi m - 0.0097) < 1, Rouche U < Lo, arg-gap > 0 for 3038 values of m in [10, 1e15]  max loc = 0.57481, min(Lo-U) = 0.419643, min m^2*gap = 0.273406
OK   m^2 G(m) increasing on m = 10..3000 (interval-certified consecutive comparisons)  
OK   true gaps arg F_m - arg F_{m+1} >= G(m) for m = 10..59 (rigorous enclosures of F_m)  gap/G(m) in [1.0185, 1.1125]

ALL RIGOROUS CHECKS PASSED (38 checks; 2.1s)
