== Theorem 2 (K=2) 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 sqrt2 (1-q)^1 tau = sqrt2 * Ttilde(u)
  [OK] d/du u^3/(1+u^2)^2 = u^2(3-u^2)/(1+u^2)^3
  [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 [2s]
== Theorem 2 (K=2) part cover
  U_- < u0: True;  U_+ > u3: True
  T8 >= sqrt2 - 1: True
  one-coordinate cells: 784 cells, inside region: True, cover [U-,U+]x[0,A_S]: True (1010 leaves)
  sign +1: 58 files, 38631 boxes; cover [U-,U+]x[0,T8]x[A_S,1]: True (54829) [1s]
  sign -1: 56 files, 16884 boxes; cover [U-,U+]x[0,T8]x[A_S,1]: True (20808) [1s]
== part cover: PASS [3s]
== Theorem 2 (K=2) part cells
  cover_k2/one_B.json: 334 cells, failed 0 (file 'failed' field: [])
  cover_k2/one_A.json: 450 cells, failed 0 (file 'failed' field: [])
  one-coordinate cells: 784/784 pass [0s]
== part cells: PASS [0s]
== Theorem 2 (K=2) part bits
  P_f == 0 for 6 functions; mu3 | P_f != 0 for 2; mu0 | P_f != 0 for 6; failures: 0
  equality cases as claimed (P==0: +-OR2 [6]; mu3|P: +-OR3 [2]; mu0|P: +-dictators [6]): True
  outside the interval the claim fails: P_OR3(q3-1e-3) = -0.0131040 < 0: True; P_dictator(q0+1e-3) = -0.0113057 < 0: True
== part bits: PASS [0s]
== Theorem 2 (K=2) part boxes
  cover2c/b00_m.json s=-1: 310 boxes, failed 0 [1s]
  cover2c/b01_m.json s=-1: 327 boxes, failed 0 [1s]
  cover2c/b02_m.json s=-1: 340 boxes, failed 0 [1s]
  cover2c/b03_m.json s=-1: 356 boxes, failed 0 [1s]
  cover2c/b04_m.json s=-1: 372 boxes, failed 0 [1s]
  cover2c/b00_p.json s=+1: 693 boxes, failed 0 [2s]
  cover2c/b05_m.json s=-1: 384 boxes, failed 0 [1s]
  cover2c/b01_p.json s=+1: 758 boxes, failed 0 [2s]
  cover2c/b02_p.json s=+1: 840 boxes, failed 0 [3s]
  cover2c/b03_p.json s=+1: 975 boxes, failed 0 [3s]
  cover2c/b06_m.json s=-1: 396 boxes, failed 0 [1s]
  cover2c/b07_m.json s=-1: 406 boxes, failed 0 [1s]
  cover2c/b08_m.json s=-1: 420 boxes, failed 0 [1s]
  cover2c/b04_p.json s=+1: 1175 boxes, failed 0 [3s]
  cover2c/b09_m.json s=-1: 431 boxes, failed 0 [1s]
  cover2c/b05_p.json s=+1: 1598 boxes, failed 0 [5s]
  cover2c/b10_m.json s=-1: 438 boxes, failed 0 [2s]
  cover2c/s00_m.json s=-1: 431 boxes, failed 0 [1s]
  cover2c/b09a_p.json s=+1: 929 boxes, failed 0 [4s]
  cover2c/b06_p.json s=+1: 2080 boxes, failed 0 [6s]
  cover2c/b09b_p.json s=+1: 973 boxes, failed 0 [5s]
  cover2c/s01_m.json s=-1: 445 boxes, failed 0 [1s]
  cover2c/s00_p.json s=+1: 621 boxes, failed 0 [2s]
  cover2c/b10a_p.json s=+1: 1045 boxes, failed 0 [5s]
  cover2c/s01_p.json s=+1: 651 boxes, failed 0 [2s]
  cover2c/s02_m.json s=-1: 428 boxes, failed 0 [1s]
  cover2c/s03_m.json s=-1: 408 boxes, failed 0 [1s]
  cover2c/s02_p.json s=+1: 602 boxes, failed 0 [2s]
  cover2c/s03_p.json s=+1: 560 boxes, failed 0 [1s]
  cover2c/s04_m.json s=-1: 392 boxes, failed 0 [1s]
  cover2c/s05_m.json s=-1: 379 boxes, failed 0 [1s]
  cover2c/b07_p.json s=+1: 3022 boxes, failed 0 [9s]
  cover2c/s04_p.json s=+1: 523 boxes, failed 0 [1s]
  cover2c/s05_p.json s=+1: 502 boxes, failed 0 [1s]
  cover2c/s06_m.json s=-1: 363 boxes, failed 0 [1s]
  cover2c/s06_p.json s=+1: 476 boxes, failed 0 [1s]
  cover2c/b10b_p.json s=+1: 1095 boxes, failed 0 [6s]
  cover2c/s07_m.json s=-1: 352 boxes, failed 0 [1s]
  cover2c/s08_m.json s=-1: 340 boxes, failed 0 [1s]
  cover2c/s07_p.json s=+1: 453 boxes, failed 0 [1s]
  cover2c/s09_m.json s=-1: 324 boxes, failed 0 [1s]
  cover2c/s08_p.json s=+1: 429 boxes, failed 0 [1s]
  cover2c/s10_m.json s=-1: 316 boxes, failed 0 [1s]
  cover2c/s09_p.json s=+1: 406 boxes, failed 0 [1s]
  cover2c/s10_p.json s=+1: 385 boxes, failed 0 [1s]
  cover2c/s11_m.json s=-1: 307 boxes, failed 0 [1s]
  cover2c/s11_p.json s=+1: 374 boxes, failed 0 [1s]
  cover2c/s12_m.json s=-1: 295 boxes, failed 0 [1s]
  cover2c/s12_p.json s=+1: 356 boxes, failed 0 [1s]
  cover2c/s13_m.json s=-1: 279 boxes, failed 0 [1s]
  cover2c/s13_p.json s=+1: 333 boxes, failed 0 [1s]
  cover2c/s14_m.json s=-1: 275 boxes, failed 0 [1s]
  cover2c/s14_p.json s=+1: 328 boxes, failed 0 [1s]
  cover2c/s15_m.json s=-1: 272 boxes, failed 0 [1s]
  cover2c/s15_p.json s=+1: 321 boxes, failed 0 [1s]
  cover2c/s16_m.json s=-1: 268 boxes, failed 0 [1s]
  cover2c/s16_p.json s=+1: 318 boxes, failed 0 [1s]
  cover2c/s17_m.json s=-1: 263 boxes, failed 0 [1s]
  cover2c/s17_p.json s=+1: 313 boxes, failed 0 [1s]
  cover2c/s18_m.json s=-1: 257 boxes, failed 0 [1s]
  cover2c/s19_m.json s=-1: 252 boxes, failed 0 [1s]
  cover2c/s18_p.json s=+1: 306 boxes, failed 0 [1s]
  cover2c/s19_p.json s=+1: 301 boxes, failed 0 [1s]
  cover2c/s20_m.json s=-1: 243 boxes, failed 0 [1s]
  cover2c/s20_p.json s=+1: 300 boxes, failed 0 [1s]
  cover2c/s21_m.json s=-1: 241 boxes, failed 0 [1s]
  cover2c/s22_m.json s=-1: 235 boxes, failed 0 [1s]
  cover2c/s21_p.json s=+1: 297 boxes, failed 0 [1s]
  cover2c/s23_m.json s=-1: 234 boxes, failed 0 [1s]
  cover2c/s22_p.json s=+1: 294 boxes, failed 0 [1s]
  cover2c/s23_p.json s=+1: 300 boxes, failed 0 [1s]
  cover2c/s24_m.json s=-1: 232 boxes, failed 0 [1s]
  cover2c/s24_p.json s=+1: 301 boxes, failed 0 [1s]
  cover2c/s25_m.json s=-1: 229 boxes, failed 0 [1s]
  cover2c/s26_m.json s=-1: 227 boxes, failed 0 [1s]
  cover2c/s25_p.json s=+1: 304 boxes, failed 0 [1s]
  cover2c/s27_m.json s=-1: 225 boxes, failed 0 [1s]
  cover2c/s26_p.json s=+1: 301 boxes, failed 0 [1s]
  cover2c/s27_p.json s=+1: 301 boxes, failed 0 [1s]
  cover2c/s28_m.json s=-1: 226 boxes, failed 0 [1s]
  cover2c/s28_p.json s=+1: 303 boxes, failed 0 [1s]
  cover2c/s29_m.json s=-1: 229 boxes, failed 0 [1s]
  cover2c/s30_m.json s=-1: 230 boxes, failed 0 [1s]
  cover2c/s29_p.json s=+1: 307 boxes, failed 0 [1s]
  cover2c/s31_m.json s=-1: 225 boxes, failed 0 [1s]
  cover2c/s30_p.json s=+1: 308 boxes, failed 0 [1s]
  cover2c/s31_p.json s=+1: 308 boxes, failed 0 [1s]
  cover2c/s32_m.json s=-1: 229 boxes, failed 0 [1s]
  cover2c/s33_m.json s=-1: 228 boxes, failed 0 [1s]
  cover2c/s32_p.json s=+1: 310 boxes, failed 0 [1s]
  cover2c/s34_m.json s=-1: 228 boxes, failed 0 [1s]
  cover2c/s35_m.json s=-1: 232 boxes, failed 0 [1s]
  cover2c/s33_p.json s=+1: 321 boxes, failed 0 [1s]
  cover2c/s34_p.json s=+1: 329 boxes, failed 0 [1s]
  cover2c/s36_m.json s=-1: 235 boxes, failed 0 [1s]
  cover2c/s35_p.json s=+1: 339 boxes, failed 0 [1s]
  cover2c/s37_m.json s=-1: 239 boxes, failed 0 [1s]
  cover2c/s36_p.json s=+1: 362 boxes, failed 0 [1s]
  cover2c/s38_m.json s=-1: 245 boxes, failed 0 [1s]
  cover2c/s39_m.json s=-1: 251 boxes, failed 0 [1s]
  cover2c/s37_p.json s=+1: 378 boxes, failed 0 [1s]
  cover2c/s40_m.json s=-1: 265 boxes, failed 0 [1s]
  cover2c/s38_p.json s=+1: 396 boxes, failed 0 [1s]
  cover2c/s39_p.json s=+1: 417 boxes, failed 0 [1s]
  cover2c/s41_m.json s=-1: 272 boxes, failed 0 [1s]
  cover2c/s42_m.json s=-1: 278 boxes, failed 0 [1s]
  cover2c/s40_p.json s=+1: 447 boxes, failed 0 [1s]
  cover2c/s43_m.json s=-1: 283 boxes, failed 0 [1s]
  cover2c/s41_p.json s=+1: 476 boxes, failed 0 [1s]
  cover2c/s44_m.json s=-1: 297 boxes, failed 0 [1s]
  cover2c/b08_p.json s=+1: 5828 boxes, failed 0 [19s]
  cover2c/s42_p.json s=+1: 503 boxes, failed 0 [2s]
  cover2c/s43_p.json s=+1: 544 boxes, failed 0 [2s]
  cover2c/s44_p.json s=+1: 616 boxes, failed 0 [2s]
  counts (sign, kind): {(-1, 'lp'): 15331, (-1, 'ncA'): 288, (-1, 'ncB'): 958, (-1, 'small'): 307, (1, 'lp'): 33479, (1, 'ms'): 1189, (1, 'ncA'): 1680, (1, 'ncB'): 1909, (1, 'small'): 374}
  failures (sign, kind): {}
  boxes: 55515/55515 pass [23s]
== part boxes: PASS [23s]
T2 RESULT: ALL PARTS PASS {'sym': True, 'cover': True, 'cells': True, 'bits': True, 'boxes': True}
exit 0 elapsed 29 s
