(U1) arithmetic
  [ok] Macaulay 1^<6> = 1 (D_7 = C F, S_1 o F in D_6 of dim 1, so F is a power)
  [ok] Macaulay 4^<3> = 5 ([15, Lemma A.11]: dim D_3' <= 5)
  [ok] Macaulay 3^<4> = 3 (H(4) = 3 -> H(5) <= 3)
  [ok] Macaulay 2^<5> = 2 (H(5) = 2 -> H(6) <= 2)
    configurations of B: 19
    excess (+D.3) fails in the worst case: (4, 'red', ['fat3'], 43, 39)
    excess (+D.3) fails in the worst case: (4, 'curv3', ['red'], 42, 41)
    excess (+D.3) fails in the worst case: (4, 'fat3', ['red'], 42, 41)
    excess (+D.3) fails in the worst case: (4, 'curv4', [], 43, 43)
    excess (+D.3) fails in the worst case: (4, 'gor4', [], 43, 43)
    excess (+D.3) fails in the worst case: (4, 'ng4', [], 42, 42)
  [ok] the configurations where excess (+D.3) can exceed 41 are exactly E1..E6
  [ok] E2, E3, E4 fail only with a point q of weight 3 (q^5 in D_5)
  [ok] E1, E5, E6 fail for every flag (bounds [43, 43, 42])
(U2) rank condition of Lemma D.3 on representatives of the local types at [X]
    fat3 (n=3), D_3 = X^2T_1 + C(Y^3): rank 3
  [ok] D.3 rank >= 3 for fat3 (n=3), D_3 = X^2T_1 + C(Y^3)
    fat3 (n=3), D_3 = X^2T_1 + C(Y^2Z + XYZ): rank 3
  [ok] D.3 rank >= 3 for fat3 (n=3), D_3 = X^2T_1 + C(Y^2Z + XYZ)
    fat3 + [Y] (n=4): dim D_3 = 4, rank 3
  [ok] fat3 + [Y] (n=4): D_3 = nu_3(B) has dim 4 and the D.3 rank is 3
    ng4 = (u^2,uw,w^3) (n=4): dim D_3 = 4, rank 3
  [ok] ng4 = (u^2,uw,w^3) (n=4): D_3 = nu_3(B) has dim 4 and the D.3 rank is 3
    curv4 (w - u^2, u^4) (n=4): dim D_3 = 4, rank 2
  [ok] curv4 (w - u^2, u^4) (n=4): D_3 = nu_3(B) has dim 4 and the D.3 rank is 2
    gor4 (u^2, w^2) (n=4): dim D_3 = 4, rank 2
  [ok] gor4 (u^2, w^2) (n=4): D_3 = nu_3(B) has dim 4 and the D.3 rank is 2
(U3) weak-ideal certificates (chart (u,w,rho) at a point v of B; e(K_v) <= colength of an explicit triple)
    E1 (1,1)     triple [6*r^5 + 7*u^4 + 3*u*r^3 - u*r^2 + 5*u*r - 3*w, 3*r^5 - 3*u^4 + 4*u*r^3 - 3*u*r^2 + 4*u*r - 9*w, 6*r^5 + 5*u^4 + 8*u*r^3 - 2*u*r^2 - 9*u*r]: colength 9 (ds), 9 (stabilization)
  [ok] E1 (1,1): certified colength (ds = stabilization)
    E1 (2,1)     triple [8*r^5 + 7*u^4 - 7*u*r^3 + 2*u^2*r + 9*u*r^2, 4*r^5 - 5*u^4 + u*r^3 + 4*u^2*r + 5*u*r^2 - 5*w, -6*r^5 + 3*u^4 + 7*u*r^3 + 9*u^2*r + 6*u*r^2 - 9*w]: colength 12 (ds), 12 (stabilization)
  [ok] E1 (2,1): certified colength (ds = stabilization)
    E1 (2,2)     triple [-6*r^5 - 2*u^4 - 8*u^2*r^2 - 9*u*r^3 + 7*u^2*r - 3*w, -5*r^5 - 4*u^4 - 7*u^2*r^2 - 7*u*r^3 + 3*u^2*r - 4*w, 7*r^5 - 8*u^4 + 2*u^2*r^2 + 2*u*r^3 - 3*u^2*r + 6*w]: colength 14 (ds), 14 (stabilization)
  [ok] E1 (2,2): certified colength (ds = stabilization)
    E1 (3,1)     triple [r^5 - 2*u^3*r + 7*u*r^3 - 2*u*r^2 - 6*w, -r^5 + u^4 + 9*u^3*r + 5*u*r^3 + 7*u*r^2 - 3*w, 4*r^5 - 2*u^4 - 7*u^3*r + 2*u*r^2 + 4*w]: colength 13 (ds), 13 (stabilization)
  [ok] E1 (3,1): certified colength (ds = stabilization)
    E2 X, j4=1   triple [6*r^5 + 7*u*r^3 + 7*u^3 + 2*u*r^2 + 8*u*r + 3*w, 4*r^5 + 6*u*r^3 - u^3 + 7*u*r^2 + u*r - 2*w, -4*r^5 - 8*u*r^3 - 5*u^3 - 3*u*r^2 + 7*u*r - 3*w]: colength 8 (ds), 8 (stabilization)
  [ok] E2 X, j4=1: certified colength (ds = stabilization)
    E2 X, j4=2   triple [-8*r^5 + 7*u*r^3 + 8*u^3 + 3*u^2*r + 5*u*r^2 - 5*w, r^5 + 9*u*r^3 + 8*u^3 + 6*u^2*r - 9*u*r^2 - 4*w, -4*r^5 - 9*u*r^3 + 9*u^3 - 6*u^2*r + 3*u*r^2 - 2*w]: colength 11 (ds), 11 (stabilization)
  [ok] E2 X, j4=2: certified colength (ds = stabilization)
    E2 q         triple [-8*r^3 + 4*u + w, -4*r^3 + 2*u - 9*w, 2*r^3 + 6*u - w]: colength 3 (ds), 3 (stabilization)
  [ok] E2 q: certified colength (ds = stabilization)
    E6 h=u       triple [4*r^5 + 9*u*w*r^2 - 5*u*r^3 + w*r^3 - 4*u*r^2 - 7*u^2 + w^2 + 2*u*r, 6*r^5 + 9*u*w*r^2 - 6*u*r^3 + 5*w*r^3 - 7*u*r^2 + 6*u^2 - 3*w^2 + 2*u*r, -7*r^5 + u*w*r^2 - 9*u*r^3 - 5*w*r^3 + 8*u*r^2 - 4*u^2 + 6*w^2 + 2*u*r]: colength 14 (ds), 14 (stabilization)
  [ok] E6 h=u: certified colength (ds = stabilization)
    E6 h=u+w     triple [-3*r^5 - 7*u*w*r^2 + 2*u*r^3 + 8*w*r^3 + u*r^2 + w*r^2 - 4*u^2 - 5*w^2 + 6*u*r + 6*w*r, 5*r^5 + 9*u*w*r^2 + 6*w*r^3 - 6*u*r^2 - 6*w*r^2 - 2*u^2 - 6*w^2 - 2*u*r - 2*w*r, -5*r^5 + 6*u*w*r^2 - w*r^3 + 5*u*r^2 + 5*w*r^2 + 8*u^2 - 7*w^2 + 3*u*r + 3*w*r]: colength 14 (ds), 14 (stabilization)
  [ok] E6 h=u+w: certified colength (ds = stabilization)
    totals 27 + sum: {'E1 (1,1)': 36, 'E1 (2,1)': 39, 'E1 (2,2)': 41, 'E1 (3,1)': 40, 'E2 j4=1': 38, 'E2 j4=2': 41, 'E6 h=u': 41, 'E6 h=u+w': 41}
  [ok] all weak-ideal totals of E1 (except (3,2)), E2, E6 (h with linear part) are <= 41
    residual R1 E1 (3,2)              colength of a random triple 17 (information only)
    residual R2 fat q (X adds 5)      colength of a random triple 10 (information only)
    residual R3 fat X (q adds 3)      colength of a random triple 13 (information only)
    residual R5 h=uw, B5=<uw,u>       colength of a random triple 18 (information only)
    residual R5 h=uw, B5=<uw,u+w>     colength of a random triple 18 (information only)
(S) the weak-ideal formula on actual graded data (random triples of I*)
    E1 (2,2): H = [1, 3, 6, 4, 3, 2, 1, 1], local lengths of random triples of I*: [41, 41] (formula 41)
  [ok] E1 (2,2): H correct and random triples of I* give the formula value 41
    R1 (3,2): H = [1, 3, 6, 4, 3, 2, 1, 1], local lengths of random triples of I*: [44, 44] (formula 44)
  [ok] R1 (3,2): H correct and random triples of I* give the formula value 44
    E2 (j4=2): H = [1, 3, 6, 4, 3, 2, 1, 1], local lengths of random triples of I*: [41, 41] (formula 41)
  [ok] E2 (j4=2): H correct and random triples of I* give the formula value 41
    E6 (h = u): H = [1, 3, 6, 4, 3, 2, 1, 1], local lengths of random triples of I*: [41, 41] (formula 41)
  [ok] E6 (h = u): H correct and random triples of I* give the formula value 41
27 checks, 0 failed
ALL CHECKS PASSED
