# Verificateur cone unaire, partie 3 : A4 = 0 (f4 = x1 A3 + x1**2 A2 + x1**3 A1).
# Lancer : python3 verify_hc4_unary_3.py   (aucun argument)
exec(open(__file__.replace('verify_hc4_unary_3.py', 'unary_core.py')).read())
say("=" * 72)
say("Cone unaire, partie 3 : A4 = 0")
say("=" * 72)
R = RV
s0 = dict(ZERO_A4)
A3v = forms(lambda v, e: v[0] == 'a' and e[0] == 1)
check("W0 det Hess A3 = 0 (A3 cubique ternaire : cone)", all(implied(s0, g, tot=(9,)) for g in hess_coeffs(A3v) if g != 0))
Z3 = dict(s0, **{v: 0 for v, e in A3v})
say("\n[W1] A3 binaire en (x2, x3)")
for name, extra in [("x2**3 + x3**3", {'a24': 1, 'a18': 1}), ("x2**2 x3", {'a23': 1})]:
    inc, fin = peel(dict(Z3, **extra))
    check("W1 A3 = %s : peel coherent" % name, not inc)
    leaf_incoherent("W1 A3 = %s, a31 = 1" % name, dict(fin, a31=1))
    leaf_dead_x4("W1 A3 = %s, a31 = 0" % name, dict(fin, a31=0))
say("\n[W2] A3 = x2**3")
t0 = dict(Z3, a24=1)
check("W2 x1**2 Q(x3,x4) carre parfait", implied(t0, R['a26'] ** 2 - 4 * R['a25'] * R['a27'], tot=(9, 8, 7)))
t0 = dict(t0, a25=0, a26=0)
leaf_dead_x4("W2 a27 = 1", dict(t0, a27=1), tot=(9, 8, 7, 6), kmax=7)
t1 = dict(t0, a27=0, a28=0)
leaf_dead_x4("W2 a29 = 1", dict(t1, a29=1), tot=(9, 8, 7, 6), kmax=7)
t2 = dict(t1, a29=0)
for e in [-R['b1'] ** 2 + 3 * R['b0'] * R['b2'], R['b1'] * R['b2'] - 9 * R['b0'] * R['b3'], -R['b2'] ** 2 + 3 * R['b1'] * R['b3']]:
    check("W2 cubique en (x3,x4) cube parfait : %s" % e, implied(t2, e, tot=(9, 8, 7)))
t2 = dict(t2, b0=0, b1=0, b2=0)
leaf_dead_x4("W2 b3 = 1", dict(t2, b3=1), tot=(9, 8, 7, 6), kmax=7)
t3 = dict(t2, b3=0)
check("W2 x2 Q(x3,x4) carre parfait", implied(t3, R['b5'] ** 2 - 4 * R['b4'] * R['b6'], tot=(9, 8, 7)))
t3 = dict(t3, b4=0, b5=0)
leaf_dead_x4("W2 b6 = 1", dict(t3, b6=1), tot=(9, 8, 7, 6), kmax=7)
leaf_zquad("W2 b6 = 0", dict(t3, b6=0), {'b10': 1, 'b12': 1, 'b11': 0})

say("\n[W3] A3 = 0")
A2v = forms(lambda v, e: v[0] == 'a' and e[0] == 2)
u0 = dict(Z3)
det2 = (-R['a27'] * R['a28'] ** 2 + R['a26'] * R['a28'] * R['a29'] - R['a25'] * R['a29'] ** 2 - R['a26'] ** 2 * R['a30'] + 4 * R['a25'] * R['a27'] * R['a30'])
check("W3 det A2 = 0 (forme quadratique de x1**2 A2)", implied(u0, det2, tot=(9,)))
Z2 = dict(u0, **{v: 0 for v, e in A2v})
inc, fin = peel(dict(Z2, a29=1, a30=0))
leaf_incoherent("W3 A2 = x2 x3, a31 = 1", dict(fin, a31=1))
leaf_dead_x4("W3 A2 = x2 x3, a31 = 0", dict(fin, a31=0))
w0 = dict(Z2, a30=1)
for e in [-R['b1'] ** 2 + 3 * R['b0'] * R['b2'], R['b1'] * R['b2'] - 9 * R['b0'] * R['b3'], -R['b2'] ** 2 + 3 * R['b1'] * R['b3']]:
    check("W3 A2 = x2**2 : cubique en (x3,x4) cube parfait : %s" % e, implied(w0, e, tot=(9, 8, 7)))
w0 = dict(w0, b0=0, b1=0, b2=0)
leaf_dead_x4("W3 A2 = x2**2, b3 = 1, a31 = 0", dict(w0, b3=1, a31=0), tot=(9, 8, 7, 6), kmax=7)
leaf_incoherent("W3 A2 = x2**2, b3 = 1, a31 = 1", dict(w0, b3=1, a31=1), tot=(9, 8, 7, 6, 5), kmax=8)
w1 = dict(w0, b3=0)
check("W3 A2 = x2**2 : x2 Q(x3,x4) carre parfait", implied(w1, R['b5'] ** 2 - 4 * R['b4'] * R['b6'], tot=(9, 8, 7)))
w1 = dict(w1, b4=0, b5=0)
leaf_dead_x4("W3 A2 = x2**2, b6 = 1, a31 = 0", dict(w1, b6=1, a31=0), tot=(9, 8, 7, 6), kmax=7)
leaf_incoherent("W3 A2 = x2**2, b6 = 1, a31 = 1", dict(w1, b6=1, a31=1), tot=(9, 8, 7, 6, 5), kmax=8)
leaf_zquad("W3 A2 = x2**2, b6 = 0", dict(w1, b6=0), {'b10': 1, 'b12': 1, 'b11': 0})

say("\n[W4] A2 = 0 : f4 = x1**3 l(u), l normalisee a x2 ou 0")
Bu = forms(lambda v, e: v[0] == 'b' and e[0] == 0)
for a33 in [0, 1]:
    v0 = dict(Z2, a30=0, a31=0, a32=0, a33=a33)
    check("W4 a33 = %d : det Hess B_u = 0 (B_u cubique ternaire : cone)" % a33,
          all(implied(v0, g, tot=(9, 8, 7, 6)) for g in hess_coeffs(Bu) if g != 0))
v0 = dict(Z2, a30=0, a31=0, a32=0, a33=0)
for name, extra in [("x2**3 + x3**3", {'b9': 1, 'b3': 1}), ("x2**2 x3", {'b8': 1, 'b9': 0, 'b3': 0})]:
    sb = dict(v0, **{v: 0 for v, e in Bu})
    sb.update(extra)
    leaf_dead_x4("W4 a33 = 0, B_u = %s" % name, sb, tot=(9, 8, 7, 6, 5), kmax=8)
sb = dict(v0, **{v: 0 for v, e in Bu})
sb['b9'] = 1
check("W4 a33 = 0, B_u = x2**3 : x1 Q(x3,x4) carre parfait", implied(sb, R['b11'] ** 2 - 4 * R['b10'] * R['b12'], tot=(9, 8, 7, 6, 5)))
leaf_dead_x4("W4 a33 = 0, B_u = x2**3, b12 = 1", dict(sb, b10=0, b11=0, b12=1), tot=(9, 8, 7, 6, 5), kmax=8)
leaf_dead_x4("W4 a33 = 0, B_u = x2**3, b12 = 0", dict(sb, b10=0, b11=0, b12=0), tot=(9, 8, 7, 6, 5), kmax=8)
sb0 = dict(v0, **{v: 0 for v, e in Bu})
detQ = (-R['b12'] * R['b13'] ** 2 + R['b11'] * R['b13'] * R['b14'] - R['b10'] * R['b14'] ** 2 - R['b11'] ** 2 * R['b15'] + 4 * R['b10'] * R['b12'] * R['b15'])
check("W4 a33 = 0, B_u = 0 : det Q = 0 (Q = coefficient de x1 dans f, quadratique en u)", implied(sb0, detQ, tot=(9, 8, 7, 6, 5)))
pen = dict(sb0, b10=0, b11=0, b13=0, b14=0)
check("W4 a33 = 0, B_u = 0, Q de rang 2 : incoherent", implied_c(dict(pen, b12=1, b15=1), RING(1)) )
check("W4 a33 = 0, B_u = 0, Q = x2**2 : c0 = c1 = c2 = 0 (f lineaire en (x3,x4))",
      all(implied_c(dict(pen, b12=0, b15=1), R[v]) for v in ['c0', 'c1', 'c2']))
leaf_dead_x4("W4 a33 = 0, B_u = 0, Q = 0", dict(pen, b12=0, b15=0), tot=(9, 8, 7, 6, 5), kmax=8)
w5 = dict(Z2, a30=0, a31=0, a32=0, a33=1, **{v: 0 for v, e in Bu})
leaf_incoherent("W5 a33 = 1, B_u = x3**3 + x4**3", dict(w5, b0=1, b3=1), tot=(9, 8, 7, 6, 5, 4, 3), kmax=10)
leaf_incoherent("W5 a33 = 1, B_u = x3**2 x4", dict(w5, b2=1), tot=(9, 8, 7, 6, 5, 4, 3), kmax=10)
w6 = dict(Z2, a30=0, a31=0, a32=0, a33=1, b0=0, b1=0, b2=0, b4=0, b5=0, b7=0)
leaf_dead_x4("W6 a33 = 1, B_u en (x2,x3), b10 = 0", dict(w6, b10=0), tot=(9, 8, 7, 6, 5), kmax=8)
leaf_zquad("W6 a33 = 1, B_u en (x2,x3), b10 = 1", dict(w6, b10=1), {'b11': 0, 'b12': 1}, tot=(9, 8, 7, 6, 5, 4, 3), kmax=10)
bilan()