(D) the graded data (U for the five cubics and nu_4(B), checked at three (alpha, beta))
  [ok] alpha = 1, beta = 0: B has Hilbert polynomial 5 and support [X]; the five cubics are independent and lie in I_B, so I*_3 = (I_B)_3; dim D_3 = 5 and X^3, X^2Y, X^2Z in D_3; dim nu_4(B) = 5 with X^4, X^3Y, X^3Z in nu_4(B)
  [ok] alpha = 2, beta = -3: B has Hilbert polynomial 5 and support [X]; the five cubics are independent and lie in I_B, so I*_3 = (I_B)_3; dim D_3 = 5 and X^3, X^2Y, X^2Z in D_3; dim nu_4(B) = 5 with X^4, X^3Y, X^3Z in nu_4(B)
  [ok] alpha = -1, beta = 2: B has Hilbert polynomial 5 and support [X]; the five cubics are independent and lie in I_B, so I*_3 = (I_B)_3; dim D_3 = 5 and X^3, X^2Y, X^2Z in D_3; dim nu_4(B) = 5 with X^4, X^3Y, X^3Z in nu_4(B)
(A38) a general D_4: X^3Z not in D_4 (h has an x^3 z term)
  [ok] (A38) alpha = 1, beta = 0, h = x^3z: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: True, X^3Z in D_4: False; a triple of L_def (attempt 0) with independent cubic parts has certified local length 38 = 27 + 11 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A38) alpha = 1, beta = 0, h = x^3z+x^3y: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: False, X^3Z in D_4: False; a triple of L_def (attempt 0) with independent cubic parts has certified local length 38 = 27 + 11 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A38) alpha = 2, beta = -3, h = x^3z: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: True, X^3Z in D_4: False; a triple of L_def (attempt 0) with independent cubic parts has certified local length 38 = 27 + 11 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A38) alpha = 2, beta = -3, h = x^3z+x^3y: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: False, X^3Z in D_4: False; a triple of L_def (attempt 0) with independent cubic parts has certified local length 38 = 27 + 11 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A38) alpha = -1, beta = 2, h = x^3z: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: True, X^3Z in D_4: False; a triple of L_def (attempt 0) with independent cubic parts has certified local length 38 = 27 + 11 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A38) alpha = -1, beta = 2, h = x^3z+x^3y: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: False, X^3Z in D_4: False; a triple of L_def (attempt 0) with independent cubic parts has certified local length 38 = 27 + 11 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
(A41) X^3Z in D_4, X^3Y not in D_4 (h has an x^3 y term and no x^3 z term)
  [ok] (A41) alpha = 1, beta = 0, h = x^3y: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: False, X^3Z in D_4: True; a triple of L_def (attempt 0) with independent cubic parts has certified local length 41 = 27 + 14 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A41) alpha = 1, beta = 0, h = x^3y+x^2z^2: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: False, X^3Z in D_4: True; a triple of L_def (attempt 0) with independent cubic parts has certified local length 41 = 27 + 14 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A41) alpha = 1, beta = 0, h = x^3y-2xz^3: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: False, X^3Z in D_4: True; a triple of L_def (attempt 0) with independent cubic parts has certified local length 41 = 27 + 14 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A41) alpha = 2, beta = -3, h = x^3y: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: False, X^3Z in D_4: True; a triple of L_def (attempt 0) with independent cubic parts has certified local length 41 = 27 + 14 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A41) alpha = 2, beta = -3, h = x^3y+x^2z^2: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: False, X^3Z in D_4: True; a triple of L_def (attempt 0) with independent cubic parts has certified local length 41 = 27 + 14 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A41) alpha = 2, beta = -3, h = x^3y-2xz^3: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: False, X^3Z in D_4: True; a triple of L_def (attempt 0) with independent cubic parts has certified local length 41 = 27 + 14 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A41) alpha = -1, beta = 2, h = x^3y: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: False, X^3Z in D_4: True; a triple of L_def (attempt 0) with independent cubic parts has certified local length 41 = 27 + 14 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A41) alpha = -1, beta = 2, h = x^3y+x^2z^2: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: False, X^3Z in D_4: True; a triple of L_def (attempt 0) with independent cubic parts has certified local length 41 = 27 + 14 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
  [ok] (A41) alpha = -1, beta = 2, h = x^3y-2xz^3: dim D_4 = 4, X^4 in D_4, X^3Y in D_4: False, X^3Z in D_4: True; a triple of L_def (attempt 0) with independent cubic parts has certified local length 41 = 27 + 14 (chart at [X]); M_Q closed with H and the triple in Ann(M_Q): True
(U42) X^3Y, X^3Z in D_4: e(L_def) >= 42 (all such D_4, all (alpha, beta))
  [ok] (U42) quartics orthogonal to X^4, X^3Y, X^3Z are the quartics without x^4, x^3y, x^3z: their chart restrictions lie in (eta, zeta)^2, so b_4 lies in (eta, zeta)^2 and rho b_4 in K'
  [ok] (U42) quintics orthogonal to X^5 (= I*_5): chart restrictions in (eta, zeta), so rho^2 b_5 lies in K'; rho^3 in K' (m^6)
  [ok] (U42) b_3 = b: the chart restrictions of the five cubics, (alpha, beta) symbolic, lie in K'
  [ok] (U42) the generators of K' are the minimal monomial generators; the complement of the Newton polyhedron lies in [0,3]^3 (rho^3, eta^2, zeta^3 in K'); 3! * covolume = 15 = 15
  [ok] (U42) an explicit parameter ideal J' in K' (three combinations of its generators) has local colength 15 = 15 at the origin n, and ((K')^2)_n = (J' K')_n (nested ideals of equal local colength 39 = 39): J'_n is a reduction of K'_n, so e(K'_n) = e(J'_n) = 15
  [ok] (U42) the equality is local only: in QQ[rho, eta, zeta] the colengths of J', J' K', (K')^2 are 21, 45, 39 (local: 15, 39, 39), and rho^6 lies in (K')^2 but not in J' K'
    hence K_[X](L_def) lies in K', e(K_[X](L_def)) >= e(K') = 15, and e(L_def) = 27 + e(K_[X]) >= 42 (Proposition prop:WM(a))
(S42) the special D_4 = <X^4, X^3Y, X^3Z, X^2Z^2>
  [ok] (S42) alpha = 1, beta = 0: D_4 lies in nu_4(B) with S_1 o D_4 in D_3; random triples of L_def: certified local length 42 = 42
  [ok] (S42) alpha = 2, beta = -3: D_4 lies in nu_4(B) with S_1 o D_4 in D_3; random triples of L_def: certified local length 42 = 42
  [ok] (S42) alpha = -1, beta = 2: D_4 lies in nu_4(B) with S_1 o D_4 in D_3; random triples of L_def: certified local length 42 = 42
27 checks, 0 failed
ALL CHECKS PASSED
