== Theorem 3 (K=3) part sym
  [OK] p_j x_j = r tau g_j (s=1)
  [OK] p_j x_j = r tau g_j (s=-1)
  [OK] sum p_j = 1
  [OK] qu = (1-q)v = tau
  [OK] 2 sqrt3 (1-q)^2 tau = sqrt3 * Ttilde(u)
  [OK] d/du u^5/(1+u^2)^3 = u^4(5-u^2)/(1+u^2)^4
  [OK] c^2 + d^2 = 1
  [OK] t = a2/(r + a1) for a1 = r c(t), a2 = r d(t)
  [OK] c'(t) = -4t/(1+t^2)^2, d'(t) = 2(1-t^2)/(1+t^2)^2
  [OK] max_{x>eta} (x-eta)/x^4 = 27/(256 eta^3) at x = 4 eta/3
  [OK] phi'(m) = -3m^2 - 3m sqrt(1-m^2)
  [OK] phi(1/sqrt2) = 0
  [OK] cumulants k3..k6
  [OK] two-coordinate value E|c chi1 + s d chi2| = 2 tau max{c, d, [s=1](1-q)(c+d)} (800 exact cases)
  [OK] E|chi_1+...+chi_k| = 2k(1-q)^(k-1) tau for q < 1/k, k <= 6 (exact)
  [OK] tail-bound identity (2000 exact cases)
== part sym: PASS [3s]
== Theorem 3 (K=3) part cover
  U_- < u3: True;  U_+ = 12/5 < u4 = sqrt(3+2sqrt3), q(U_+) = 25/169: True
  T8 >= sqrt2 - 1: True
  one-coordinate cells: 2704 cells, inside region: True, cover [U-,U+]x[0,A_S]: True (2770 leaves)
  sign +1: 58 files, 69871 boxes; cover [U-,U+]x[0,T8]x[A_S,1]: True (85295) [3s]
  sign -1: 29 files, 12104 boxes; cover [U-,U+]x[0,T8]x[A_S,1]: True (15284) [0s]
== part cover: PASS [5s]
== Theorem 3 (K=3) part cells
  k3/one/o03.json: 240 cells, failed 0 (file 'failed' field: [])
  k3/one/o04.json: 241 cells, failed 0 (file 'failed' field: [])
  k3/one/o02.json: 240 cells, failed 0 (file 'failed' field: [])
  k3/one/o05.json: 246 cells, failed 0 (file 'failed' field: [])
  k3/one/o01.json: 253 cells, failed 0 (file 'failed' field: [])
  k3/one/o06.json: 252 cells, failed 0 (file 'failed' field: [])
  k3/one/o00.json: 268 cells, failed 0 (file 'failed' field: [])
  k3/one/o07.json: 260 cells, failed 0 (file 'failed' field: [])
  k3/one/o08.json: 294 cells, failed 0 (file 'failed' field: [])
  k3/one/o09.json: 410 cells, failed 0 (file 'failed' field: [])
  one-coordinate cells: 2704/2704 pass [1s]
== part cells: PASS [1s]
== Theorem 3 (K=3) part bits
  P_f == 0 for 2 functions; mu3 | P_f != 0 for 6; mu0 | P_f != 0 for 0; failures: 0
  equality cases as claimed (P==0: +-OR3 [2]; mu3|P: +-OR2 [6]; no zero in [qL,q3)): True
  outside the interval the claim fails: P_OR2(q3+1e-3) = -0.0130240 < 0: True
== part bits: PASS [0s]
== Theorem 3 (K=3) part boxes
  k3/cover2c/p03.json s=+1: 1133 boxes, failed 0 [6s]
  k3/cover2c/p02.json s=+1: 1161 boxes, failed 0 [6s]
  k3/cover2c/p05.json s=+1: 1117 boxes, failed 0 [6s]
  k3/cover2c/p04.json s=+1: 1122 boxes, failed 0 [6s]
  k3/cover2c/p07.json s=+1: 1108 boxes, failed 0 [6s]
  k3/cover2c/p01.json s=+1: 1182 boxes, failed 0 [6s]
  k3/cover2c/p06.json s=+1: 1111 boxes, failed 0 [6s]
  k3/cover2c/p00.json s=+1: 1223 boxes, failed 0 [8s]
  k3/cover2c/p13.json s=+1: 1053 boxes, failed 0 [5s]
  k3/cover2c/p12.json s=+1: 1058 boxes, failed 0 [5s]
  k3/cover2c/p14.json s=+1: 1024 boxes, failed 0 [5s]
  k3/cover2c/p08.json s=+1: 1118 boxes, failed 0 [6s]
  k3/cover2c/p10.json s=+1: 1093 boxes, failed 0 [6s]
  k3/cover2c/p09.json s=+1: 1111 boxes, failed 0 [6s]
  k3/cover2c/p11.json s=+1: 1064 boxes, failed 0 [6s]
  k3/cover2c/p15.json s=+1: 1020 boxes, failed 0 [5s]
  k3/cover2c/p17.json s=+1: 1028 boxes, failed 0 [5s]
  k3/cover2c/p18.json s=+1: 1032 boxes, failed 0 [5s]
  k3/cover2c/p16.json s=+1: 1025 boxes, failed 0 [5s]
  k3/cover2c/p19.json s=+1: 1039 boxes, failed 0 [5s]
  k3/cover2c/p21.json s=+1: 1055 boxes, failed 0 [5s]
  k3/cover2c/p20.json s=+1: 1051 boxes, failed 0 [5s]
  k3/cover2c/p22.json s=+1: 1060 boxes, failed 0 [5s]
  k3/cover2c/p23.json s=+1: 1068 boxes, failed 0 [5s]
  k3/cover2c/p24.json s=+1: 1062 boxes, failed 0 [6s]
  k3/cover2c/p26.json s=+1: 1065 boxes, failed 0 [5s]
  k3/cover2c/p25.json s=+1: 1067 boxes, failed 0 [6s]
  k3/cover2c/p27.json s=+1: 1066 boxes, failed 0 [5s]
  k3/cover2c/p28.json s=+1: 1068 boxes, failed 0 [6s]
  k3/cover2c/p29.json s=+1: 1058 boxes, failed 0 [6s]
  k3/cover2c/p30.json s=+1: 1061 boxes, failed 0 [6s]
  k3/cover2c/p31.json s=+1: 1067 boxes, failed 0 [6s]
  k3/cover2c/p33.json s=+1: 1084 boxes, failed 0 [6s]
  k3/cover2c/p32.json s=+1: 1075 boxes, failed 0 [6s]
  k3/cover2c/p34.json s=+1: 1094 boxes, failed 0 [6s]
  k3/cover2c/p35.json s=+1: 1098 boxes, failed 0 [6s]
  k3/cover2c/p36.json s=+1: 1107 boxes, failed 0 [6s]
  k3/cover2c/p37.json s=+1: 1120 boxes, failed 0 [6s]
  k3/cover2c/p38.json s=+1: 1127 boxes, failed 0 [7s]
  k3/cover2c/p39.json s=+1: 1140 boxes, failed 0 [7s]
  k3/cover2c/p40.json s=+1: 1160 boxes, failed 0 [7s]
  k3/cover2c/p41.json s=+1: 1175 boxes, failed 0 [7s]
  k3/cover2c/p42.json s=+1: 1193 boxes, failed 0 [7s]
  k3/cover2c/p43.json s=+1: 1222 boxes, failed 0 [7s]
  k3/cover2c/p44.json s=+1: 1247 boxes, failed 0 [8s]
  k3/cover2c/p45.json s=+1: 1274 boxes, failed 0 [7s]
  k3/cover2c/p46.json s=+1: 1308 boxes, failed 0 [7s]
  k3/cover2c/p47.json s=+1: 1352 boxes, failed 0 [7s]
  k3/cover2c/p48.json s=+1: 1391 boxes, failed 0 [7s]
  k3/cover2c/p49.json s=+1: 1435 boxes, failed 0 [8s]
  k3/cover2c/p50.json s=+1: 1483 boxes, failed 0 [8s]
  k3/cover2c/p51.json s=+1: 1534 boxes, failed 0 [8s]
  k3/cover2c/p52.json s=+1: 1597 boxes, failed 0 [9s]
  k3/cover2c/p53.json s=+1: 1649 boxes, failed 0 [9s]
  k3/cover2c/m00.json s=-1: 491 boxes, failed 0 [2s]
  k3/cover2c/m01.json s=-1: 475 boxes, failed 0 [2s]
  k3/cover2c/p54.json s=+1: 1715 boxes, failed 0 [9s]
  k3/cover2c/m02.json s=-1: 468 boxes, failed 0 [2s]
  k3/cover2c/m03.json s=-1: 456 boxes, failed 0 [1s]
  k3/cover2c/m04.json s=-1: 445 boxes, failed 0 [1s]
  k3/cover2c/m05.json s=-1: 437 boxes, failed 0 [1s]
  k3/cover2c/m06.json s=-1: 435 boxes, failed 0 [1s]
  k3/cover2c/m08.json s=-1: 421 boxes, failed 0 [1s]
  k3/cover2c/m07.json s=-1: 426 boxes, failed 0 [1s]
  k3/cover2c/m09.json s=-1: 419 boxes, failed 0 [1s]
  k3/cover2c/m10.json s=-1: 416 boxes, failed 0 [1s]
  k3/cover2c/p55.json s=+1: 1805 boxes, failed 0 [10s]
  k3/cover2c/m11.json s=-1: 411 boxes, failed 0 [1s]
  k3/cover2c/m12.json s=-1: 408 boxes, failed 0 [1s]
  k3/cover2c/m13.json s=-1: 405 boxes, failed 0 [1s]
  k3/cover2c/m14.json s=-1: 402 boxes, failed 0 [1s]
  k3/cover2c/m15.json s=-1: 398 boxes, failed 0 [1s]
  k3/cover2c/m16.json s=-1: 399 boxes, failed 0 [1s]
  k3/cover2c/m17.json s=-1: 395 boxes, failed 0 [1s]
  k3/cover2c/m18.json s=-1: 390 boxes, failed 0 [1s]
  k3/cover2c/m20.json s=-1: 388 boxes, failed 0 [1s]
  k3/cover2c/m19.json s=-1: 388 boxes, failed 0 [1s]
  k3/cover2c/m21.json s=-1: 395 boxes, failed 0 [1s]
  k3/cover2c/m22.json s=-1: 397 boxes, failed 0 [1s]
  k3/cover2c/m23.json s=-1: 398 boxes, failed 0 [1s]
  k3/cover2c/m24.json s=-1: 402 boxes, failed 0 [1s]
  k3/cover2c/m25.json s=-1: 405 boxes, failed 0 [1s]
  k3/cover2c/m26.json s=-1: 407 boxes, failed 0 [1s]
  k3/cover2c/m27.json s=-1: 411 boxes, failed 0 [1s]
  k3/cover2c/m28.json s=-1: 416 boxes, failed 0 [1s]
  k3/cover2c/p56.json s=+1: 1913 boxes, failed 0 [11s]
  k3/cover2c/p57.json s=+1: 2003 boxes, failed 0 [11s]
  counts (sign, kind): {(-1, 'lp'): 11613, (-1, 'ncB'): 232, (-1, 'small'): 259, (1, 'lp'): 45720, (1, 'ms'): 21232, (1, 'ncA'): 1097, (1, 'ncB'): 1205, (1, 'small'): 617}
  failures (sign, kind): {}
  boxes: 81975/81975 pass [54s]
== part boxes: PASS [54s]
T3 RESULT: ALL PARTS PASS {'sym': True, 'cover': True, 'cells': True, 'bits': True, 'boxes': True}
exit 0 elapsed 62 s
