(U1) P2: quintics with all first derivatives in X^3 T_1
  [ok] (U1) {G in T_5 : S_1 o G in X^3 T_1} = X^4 T_1 (dimension 3, spanned by X^5, X^4Y, X^4Z)
(A2) Lemma TQ on the pure-secant orbits with the heavy germ at [Y] (F = X^6, alpha = u^5, ell = u, u(X)u(Y) != 0)
  [ok] (A2) [X] reduced + nG4 at [Y] with long axis x = 0: B has length 5 and D_3 = nu_3(B) has dimension 5
  [ok] (A2)   u = x + y + z: c = 720 != 0, rank 2, eps_X <= 2, eps_Y <= 5 (ds = stabilization), bound 27 + 2(eps_X + eps_Y) = 41 <= 41
  [ok] (A2)   u = x + 2*y - z: c = 720 != 0, rank 2, eps_X <= 2, eps_Y <= 5 (ds = stabilization), bound 27 + 2(eps_X + eps_Y) = 41 <= 41
  [ok] (A2) curv2 at [X] in direction Z + fat point at [Y]: B has length 5 and D_3 = nu_3(B) has dimension 5
  [ok] (A2)   u = x + y + z: c = 720 != 0, rank 2, eps_X <= 3, eps_Y <= 4 (ds = stabilization), bound 27 + 2(eps_X + eps_Y) = 41 <= 41
  [ok] (A2)   u = x + 2*y - z: c = 720 != 0, rank 2, eps_X <= 3, eps_Y <= 4 (ds = stabilization), bound 27 + 2(eps_X + eps_Y) = 41 <= 41
(S3) rank lemma: rank of u o K modulo D_3 equals 1 + sigma_X (F = X^6, l(B) = 5)
  [ok] (S3) nG4 at X (long axis y=0) + point [1:1:1]: dim K = 8, rank 3 = 1 + sigma_X = 3
  [ok] (S3) L5a (yz, y^3, z^3) at X: dim K = 8, rank 3 = 1 + sigma_X = 3
  [ok] (S3) L5b (y^2, yz^2, z^3) at X: dim K = 8, rank 3 = 1 + sigma_X = 3
  [ok] (S3) L5c (y^2, xyz + z^3, z^4) at X (kappa = 1): dim K = 8, rank 3 = 1 + sigma_X = 3
  [ok] (S3) fat at X + curv2 at Y (direction Z): dim K = 8, rank 3 = 1 + sigma_X = 3
  [ok] (S3) G5 (yz, xy^2 - z^3) + m^4 at X: dim K = 7, rank 2 = 1 + sigma_X = 2
  [ok] (S3) X reduced + nG4 at Y: dim K = 7, rank 2 = 1 + sigma_X = 2
(S4) binary tangent F = X^5 Y, Gamma' = V(z, y^2) at X; alpha = x^5 + x^4 y, ell = y (P on the line z = 0)
  [ok] (S4) nG4 at X with long axis y = 0 (Gamma' not along it) + point [1:1:1]: c != 0, rank 1, eps = [5, 1] = e_p, TQ bound 39 <= 39
  [ok] (S4) G5 (yz, xy^2 - z^3): Gamma' along the line z = 0 (length 2): c != 0, rank 1, eps = [5] = e_p, TQ bound 37 <= 39
  [ok] (S4) nG4 at X with long axis z = 0 (Gamma' along it): B meets z = 0 in length 3: no m-primary pencil found (eps_X infinite), as predicted
(S5) pure tangent F = X^6, G5 germs containing Gamma' = V(z, y^2): eps_X on sampled embeddings
  [ok] (S5) G5 (uw, u^2 - w^3): rank 2, eps_X <= [7], TQ bound 41 (information)
  [ok] (S5) G5 (uw, w^2 - u^3): rank 2, eps_X <= [7], TQ bound 41 (information)
  [ok] (S5) G5 ((u-w)w, (u-w)^2 - w^3): rank 2, eps_X <= [7], TQ bound 41 (information)
(S6) nG4 alone (l(B) = 4), F = X^6: rank of [15, Lemma D.3]
  [ok] (S6) long axis z = 0: X^2M^2, X^2LM, XL^3 lie in K for D_3 = nu_3(nG4) + any cubic, and their x-derivatives are independent modulo nu_3(nG4) (U)
  [ok] (S6)   long axis z = 0, random extra cubic 0: B of length 4, rank 3 >= 3
  [ok] (S6)   long axis z = 0, random extra cubic 1: B of length 4, rank 3 >= 3
  [ok] (S6)   long axis z = 0, random extra cubic 2: B of length 4, rank 3 >= 3
  [ok] (S6)   long axis z = 0: accepted samples 3 of 3
  [ok] (S6) long axis y = 0: X^2M^2, X^2LM, XL^3 lie in K for D_3 = nu_3(nG4) + any cubic, and their x-derivatives are independent modulo nu_3(nG4) (U)
  [ok] (S6)   long axis y = 0, random extra cubic 0: B of length 4, rank 3 >= 3
  [ok] (S6)   long axis y = 0, random extra cubic 1: B of length 4, rank 3 >= 3
  [ok] (S6)   long axis y = 0, random extra cubic 2: B of length 4, rank 3 >= 3
  [ok] (S6)   long axis y = 0: accepted samples 3 of 3
(A7) binary tangent, nG4 + p with p on the line of Gamma': Lemma TQ with P = p
  [ok] (A7) p = Y: B of length 5, D_3 of dimension 5, P = alpha o F is a multiple of p
  [ok] (A7)   c = 120, rank 2, eps_X <= 5, eps_p <= 2, bound 27 + 2 eps_X + 2 eps_p = 41 <= 41
  [ok] (A7) p = X + Y: B of length 5, D_3 of dimension 5, P = alpha o F is a multiple of p
  [ok] (A7)   c = 120, rank 2, eps_X <= 5, eps_p <= 2, bound 27 + 2 eps_X + 2 eps_p = 41 <= 41
(U8) Lemma 10.5: e((h) + m b) for the model G5
  [ok] (U8) h = -b^3 + a^2 + a*b: a pencil of (h) + m*b of local colength 7 (ds) = 7 (stabilization) <= 7
  [ok] (U8) h = 2*b^3 - 2*a^2 + a*b: a pencil of (h) + m*b of local colength 7 (ds) = 7 (stabilization) <= 7
  [ok] (U8) h = -3/7*b^3 + 3/7*a^2 + a*b: a pencil of (h) + m*b of local colength 7 (ds) = 7 (stabilization) <= 7
  [ok] (U8) h = -b^3 + a^2: a pencil of (h) + m*b of local colength 7 (ds) = 7 (stabilization) <= 7
  [ok] (U8) h = a*b: a pencil of (h) + m*b of local colength 7 (ds) = 7 (stabilization) <= 7
39 checks, 0 failed
ALL CHECKS PASSED
