Part U1: Lemma F functional for R = Y^2 (Xi = X^2 Y^2 / 2)
  ok   x^2 o Xi = Y^2; eps(x^2 rho) = <rho, Y^2> for the six quadratic monomials; eps(l w) = 0 for l in S_1 and the six monomials w spanning {cubics without x^2-terms, [x y^2] = 0}; control: eps(x * x y^2) != 0
Part U2: Corollary F'': y^5 and binary quintics vanishing at [Y]
  ok   y^5 o (Y^7 + general tails) = 2520 Y^2 + T_{<=1}; y^5 o (general element of degree <= 6) in T_{<=1}; T_5 o (Y^7 + tails) in T_{<=1} for T_5 = y^4 z + 3 y^3 z^2 - 2 z^5
Part U3: (O1) with delta = 3 and z^2 | g: explicit Lemma F operators (all tails symbolic)
  ok   Z3a (g = z^3, e != 0): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2: True; u_3 o D_5 in C Y^2: True; pi(u_3) = z^3
  ok   Z3b (g = z^3, e = 0 != d, a2 != 0): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2: True; u_3 o D_5 in C Y^2: True; pi(u_3) = z^3
  ok   Z3c (g = z^3, e = 0 != d, a2 = 0), Z^2-coefficient = L(be, ga): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2 + (-8/35*d^2*be + 12*be*b4 + 60*ga*b5) Z^2: True; u_3 o D_5 in C Y^2: True; pi(u_3) = be*y*z^2 + ga*z^3
      Z3c: u = (-d*be)/105*y^4 + (-be*b3 - 2*ga*b4)/(4*d)*y^3*z + be*y*z^2 + ga*z^3
  ok   Z3c: the remaining condition -8/35*d^2*be + 12*be*b4 + 60*ga*b5 = 0 is one homogeneous linear equation in (be, ga): True, so it has a nonzero solution for every value of the tails; pi(u_3) = be*y*z^2 + ga*z^3 depends injectively on (be, ga): True
  ok   Z3d: z o B5 in D_4 for B5 in <Y^5, Y^4 Z, Y^3 Z^2, Y^2 Z^3> (and conversely by integration)
  ok   Z3d (g = z^3, B6 = 0, D_5 = <Y^5, Y^4 Z>): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2: True; u_3 o D_5 in C Y^2: True; pi(u_3) = z^3
  ok   Z3d (g = z^3, B6 = 0, D_5 = <Y^5, Y^3 Z^2 + Y^4 Z>): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2: True; u_3 o D_5 in C Y^2: True; pi(u_3) = z^3
  ok   G2a (g = z^2 y, A, B != 0): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2: True; u_3 o D_5 in C Y^2: True; pi(u_3) = y*z^2
  ok   G2b (g = z^2 y, A != 0 = B, a4 != 0): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2: True; u_3 o D_5 in C Y^2: True; pi(u_3) = y*z^2
  ok   G2b (g = z^2 y, A != 0 = B, a4 != 0) is empty: (z^2 - (A/105) y^3) o Phi has degree <= 3 and cubic part 12 a4 XZ^2 + (binary cubic), identically in the tails; closedness puts it in D_3 = bT_3 + C XY^2, which has no XZ^2, so a4 = 0
  ok   G2b' (g = z^2 y, A != 0 = B, a4 = 0), Z^2-coefficient = L(be, ga): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2 + (-8/35*A^2*be + 12*be*b4 + 60*ga*b5) Z^2: True; u_3 o D_5 in C Y^2: True; pi(u_3) = be*y*z^2 + ga*z^3
      G2b': u = (-A*be)/105*y^4 + (-be*b3 - 2*ga*b4)/(4*A)*y^3*z + be*y*z^2 + ga*z^3
  ok   G2b': the remaining condition -8/35*A^2*be + 12*be*b4 + 60*ga*b5 = 0 is one homogeneous linear equation in (be, ga): True, so it has a nonzero solution for every value of the tails; pi(u_3) = be*y*z^2 + ga*z^3 depends injectively on (be, ga): True
  ok   G2c (g = z^2 y, A = 0 != B, a1 != 0): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2: True; u_3 o D_5 in C Y^2: True; pi(u_3) = y*z^2
  ok   G2c' (g = z^2 y, A = 0 != B, a1 = 0), YZ-coefficient = L(be, ga): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2 + (12*be*b2 + 12*ga*b3) Y*Z: True; u_3 o D_5 in C Y^2: True; pi(u_3) = be*y^2*z + ga*y*z^2
      G2c': u = (-be*b3 - 2*ga*b4)/(60*B)*z^4 + be*y^2*z + ga*y*z^2
  ok   G2c': the remaining condition 12*be*b2 + 12*ga*b3 = 0 is one homogeneous linear equation in (be, ga): True, so it has a nonzero solution for every value of the tails; pi(u_3) = be*y^2*z + ga*y*z^2 depends injectively on (be, ga): True
  ok   G2d: z o B5 in D_4 for B5 in <Y^5, Y^4 Z, Y^3 Z^2, Z^5> (and conversely)
  ok   G2d (g = z^2 y, B6 = 0, D_5 = <Y^5, Y^4*Z>): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2: True; u_3 o D_5 in C Y^2: True; pi(u_3) = y*z^2
  ok   G2d (g = z^2 y, B6 = 0, D_5 = <Y^5, Z^5>): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2: True; u_3 o D_5 in C Y^2: True; pi(u_3) = y*z^2
  ok   G2d (g = z^2 y, B6 = 0, D_5 = <Y^5, Y^4*Z + Z^5>): g kills D_4, D_5: True; S_1 o D_5 in D_4: True; z o B6 in D_5, no Y^6, Y^5 Z: True; A_4 in D_4: True; u o Phi: deg >= 3 parts zero: True, deg 2 part in C Y^2: True; u_3 o D_5 in C Y^2: True; pi(u_3) = y*z^2
  ok   B6 with z o B6 killed by g: g = z^3 gives <Y^4 Z^2, Y^3 Z^3> ([Y^4*Z^2, Y^3*Z^3]); g = z^2 y gives <Y^4 Z^2, Z^6> ([Y^4*Z^2, Z^6])
time 0.2 s
ALL CHECKS PASSED
