A.35 addendum: RQ-A MAIN_RESULT_U9 write-up checks (RQ-AUD own code)
PASS T C(q5) = g(2 ln 5/4) (|diff| < 1e-70)
PASS T C(q6) = g(5 s(q6)) = g(6 s(q6)) (|diff| < 1e-70)
   c = [0.79788456080286535588 +/- 1.09e-22]  C(q5) = [0.85510045547081924572 +/- 1.49e-21]  C(q6) = [0.85598448917381538818 +/- 2.37e-21]
PASS T truncation c = 0.7978845608...
PASS T truncation C(q5) = 0.8551004554...
PASS T truncation C(q6) = 0.8559844891...
PASS T truncation C(q5) - c = 0.0572158946...
PASS T truncation C(q6) - c = 0.0580999283...
PASS T truncation 2(C(q5) - c) = 0.1144317...
PASS T truncation 2(C(q6) - c) = 0.1161998...
PASS T 0.114431 < 2(C(q5) - c) (Corollary 2, abstract)
PASS T Remark 3: c = 0.797885 (rounded)
PASS S lower Mills: beta' - w beta + 1 = 2/(1+w^2)^2
PASS S beta' = (1-w^2)/(1+w^2)^2
PASS S B' = -(w^4+3w^2+6)/(w^2(w^2+3)^2)
PASS S w B = (w^2+2)/(w^2+3)
PASS S B' - w B + 1 = -6/(w^2(w^2+3)^2)
PASS S (1+w^2) B - w = 2/(w(w^2+3))
PASS S w B < 1 (so 0 < w M < 1): 1 - w B = 1/(w^2+3)
PASS S w beta > 0 and (1+w^2) beta - w = 0
PASS S (f''/c)' = w M (w^2+3) - (w^2+2) using M' = w M - 1 only
PASS S f' = c M' and f'' = c (M + w M') = c((1+w^2) M - w)
PASS S comparison: (r e^{-w^2/2})' = (beta' - w beta + 1) e^{-w^2/2} for r = beta - M
PASS S f(0) = int_{-oo}^0 (|t| - c) e^{-t^2/2} dt = 0
PASS S f'(0) = h(0) + 0 f(0) = -c, and c M(0) = 1
PASS R E|G+a| = 2 phi(a) + a (2 Phi(a) - 1) at a = 7/10 (exact integrals)
   E|G+x| series: -x**8/2688 + x**6/240 - x**4/24 + x**2/2 + 1
PASS R E|G+x| = c (1 + x^2/2 - x^4/24 + O(x^6))
   D(x) series / phi(0): x**2*(x**2 - 10)/120
PASS R D(x) = phi(0) (-x^2/12 + O(x^4))
   x =  0.05: derivative (Richardson) -8.30922014769601e-5  formula -8.30922014769601e-5  phi(0)(-x^2/12) -8.3112975e-5  rel diff 1.95e-32
   x =   0.2: derivative (Richardson) -0.00132450730924244  formula -0.00132450730924244  phi(0)(-x^2/12) -0.0013298076  rel diff 1.01e-33
   x =   0.5: derivative (Richardson) -0.00810806440244586  formula -0.00810806440244586  phi(0)(-x^2/12) -0.0083112975  rel diff 2.31e-34
   x =   1.0: derivative (Richardson) -0.0301959000289254  formula -0.0301959000289254  phi(0)(-x^2/12) -0.03324519  rel diff 9.23e-35
   x =  1.54: derivative (Richardson) -0.0634777969347614  formula -0.0634777969347614  phi(0)(-x^2/12) -0.078844293  rel diff 1.68e-35
   x =  -1.0: derivative (Richardson) -0.0301959000289254  formula -0.0301959000289254  phi(0)(-x^2/12) -0.03324519  rel diff 9.23e-35
   x =   3.0: derivative (Richardson) -0.15417786397574  formula -0.15417786397574  phi(0)(-x^2/12) -0.29920671  rel diff 1.71e-36
PASS R derivative of E|Z_{K_eps}| at eps = 0 equals -c/2 + (E|G+x| - c)/x^2 (rel diff < 1e-15 at 7 points)
ALL CHECKS PASSED  (4.8 s)
