== Theorem 4 part sym
  [OK] Lemma 9: kappa_1 = 0, kappa_2 = 1, kappa_j = d^[j odd] G_j(w) for j = 3..10 (log-MGF series)
  [OK] Lemma 10: set-partition formula N_n(e) = recursion of the text, n <= 10
  [OK] Lemma 10: N_n(0) = (n-1)!! (n even), 0 (n odd)
  [OK] Lemma 10: all N_n(e) are positive integers
  [OK] Lemma 10 at u = 5/2: mu_n(kappa) = E chi^n exactly for n <= 10
  [OK] Lemma 10 for M = (3/5) chi_1 + (4/5) chi_2 at u = 5/2: exact for n <= 10
  [OK] T = 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] (1-q4)/q4 = 3 + 2 sqrt3
  [OK] q4 is the root in (0,1) of g4 = 4q^2 - 8q + 1
  [OK] Lemma 4(iii): 4(1-q)^3 - 2 sqrt3 (1-q)^2 = 2(1-q)^2 (2(1-q) - sqrt3), zero at q4
  [OK] Corollary 2: (k/3)(3/4)^(k-3) = 1 at k = 4 and decreasing (k = 4..59, exact)
  [OK] |p2| = |p3| = 1; half-angle forms: rr^2 + bb^2 = 1, mm^2 + cm^2 = 1
  [OK] (P4) polynomials: h.p2 (1+t^2)(1+s^2) and h.p3 (1+t^2)(1+s^2)(1+z^2) as implemented
  [OK] s = r/(1+sqrt(1-r^2)) inverts r = 2s/(1+s^2) on [0,1]
  [OK] pi_w y_w = tau sum_i gamma_i (+-1)_i prod_{l!=i} Pr[w_l]  (k = 2, 3, 4, all atoms)
  [OK] Lemma 5: E|c chi1 + s d chi2| = 2 tau max{c, d, [s=1](1-q)(c+d)} (600 exact cases)
  [OK] Lemma 4: E|chi_1+...+chi_k| = 2k(1-q)^(k-1) tau for q < 1/k, k <= 6 (exact)
  [OK] one-coordinate identity E|a chi + y| = 2 tau a + 2 R_a(y) - (1-2q) y (2000 exact cases)
  [OK] Lemma 26 identity |y+z| - |y| - sgn(y) z = 2(-sgn(y) z - |y|)_+ <= 2(|z|-|y|)_+ (exact)
  [OK] max_{x>eta} (x-eta)/x^4 = 27/(256 eta^3) at x = 4 eta/3
  [OK] Lemma 12: phi'(m) = -3m^2 - 3m sqrt(1-m^2), phi(1/sqrt2) = 0
  [OK] Lemma 11 (even power sums, exact random cases): p4 <= m^2, p_j >= rho^(j-2), p_j <= m^(j-4) p4
== part sym: PASS [98s]
== Theorem 4 part cover
  sqrt5 < U_-: True;  q(U_-) = 25/169: True;  U_+ >= u4: True;  U_- > u3: True;  T8 >= sqrt2-1: True;  S3 (144/169)^2 > 5/4 > A_S: True
  one-coordinate cells: 288 cells, inside [U-,U+]x[0,A_S]: True, cover it: True (311)
  sign +1: 18 files, 941 boxes, inside region: True; cover [U-,U+]x[0,T8]x[A_S,1]: True (1817) [0s]
  sign -1: 15 files, 480 boxes, inside region: True; cover [U-,U+]x[0,T8]x[A_S,1]: True (480) [0s]
== part cover: PASS [0s]
== Theorem 4 part cells
  k3b/one_2.json: region ['127/50', '127123/50000', '0', '7/20'], 64 cells, failed 0 (file 'failed' field: [])
  k3b/one_0.json: region ['12/5', '247/100', '0', '7/20'], 98 cells, failed 0 (file 'failed' field: [])
  k3b/one_1.json: region ['247/100', '127/50', '0', '7/20'], 126 cells, failed 0 (file 'failed' field: [])
  degrees of passing cells: {10: 288}
  one-coordinate cells: 288/288 pass [0s]
== part cells: PASS [0s]
== Theorem 4 part bits
  g4 = 4q^2-8q+1 irreducible (disc 48), q_U < q4- < q4 < q4+ < q_L, g4(q4-) > 0 > g4(q4+): True
  n=3: 256 functions, 39 distinct H_f; H_f == 0 for 2, g4 | H_f != 0 for 0; sign proofs failed: 0 (on [q_U, q_L]); equality lists as claimed: True [0s]
  n=4: 65536 functions, 1630 distinct H_f; H_f == 0 for 8, g4 | H_f != 0 for 2; sign proofs failed: 0 (on [q4-, q_L]); equality lists as claimed: True [1s]
  H_OR1234 = -4(1-q)^4 g4(q): True
== part bits: PASS [1s]
== Theorem 4 part boxes
    200/1421 boxes [1s], failures so far 0
    400/1421 boxes [3s], failures so far 0
    600/1421 boxes [5s], failures so far 0
    800/1421 boxes [7s], failures so far 0
    1000/1421 boxes [9s], failures so far 0
    1200/1421 boxes [11s], failures so far 0
    1400/1421 boxes [13s], failures so far 0
  counts (sign, kind): {(-1, 'lpv'): 480, (1, 'lpv'): 626, (1, 'ms5'): 302, (1, 'ncA'): 13}
  failures (sign, kind): {}
  verified objects: {'deg6': 2845, 'minus_SG': 146, 'minus_TC': 182, 'ncA_testA': 13, 'plus_A3': 123, 'plus_TC': 689, 'plus_TCS': 210, 'sub_A4': 301, 'vcert': 2845, 'vertices': 16544}
  slowest boxes: [('0.9s', 'b5_12_1.json', 26, 'ms5'), ('0.9s', 'sub13_c_1.json', 11, 'ms5'), ('0.9s', 'sub13_c_1.json', 12, 'ms5')]
  boxes: 1421/1421 pass [14s]
== part boxes: PASS [14s]
T4 RESULT: ALL PARTS PASS {'sym': True, 'cover': True, 'cells': True, 'bits': True, 'boxes': True}
