# Verificateur cone unaire, partie 2 : A4 = x2**4 (A4 = partie de f4 sans x1).
# Lancer : python3 verify_hc4_unary_2.py   (aucun argument)
exec(open(__file__.replace('verify_hc4_unary_2.py', 'unary_core.py')).read())
say("=" * 72)
say("Cone unaire, partie 2 : A4 = x2**4, directions (x3, x4) libres pour A4")
say("=" * 72)
R = RV
s0 = dict(ZERO_A4, a14=1)
say("\n[V1] x1 * C(x3,x4) (a15..a18) est un cube parfait")
for e in [-R['a16'] ** 2 + 3 * R['a15'] * R['a17'], R['a16'] * R['a17'] - 9 * R['a15'] * R['a18'], -R['a17'] ** 2 + 3 * R['a16'] * R['a18']]:
    check("V1 covariant hessien nul : %s" % e, implied(s0, e, tot=(9,)))
s1 = dict(s0, a15=0, a16=0, a17=0)
leaf_dead_x4("V1 C = x3**3 (a18 = 1)", dict(s1, a18=1))
s2 = dict(s1, a18=0)
check("V2 x1 x2 Q(x3,x4) carre parfait", implied(s2, R['a20'] ** 2 - 4 * R['a19'] * R['a21'], tot=(9,)))
s2 = dict(s2, a19=0, a20=0)
leaf_dead_x4("V2 Q = x3**2 (a21 = 1)", dict(s2, a21=1))
s3 = dict(s2, a21=0, a22=0)          # forme lineaire x1 x2**2 (a22 x4 + a23 x3) normalisee
leaf_dead_x4("V3 x1 x2**2 x3 (a23 = 1)", dict(s3, a23=1))
s4 = dict(s3, a23=0)
check("V4 x1**2 Q(x3,x4) carre parfait", implied(s4, R['a26'] ** 2 - 4 * R['a25'] * R['a27'], tot=(9, 8, 7)))
s4 = dict(s4, a25=0, a26=0)
leaf_dead_x4("V4 a27 = 1, a31 = 0", dict(s4, a27=1, a31=0), tot=(9, 8, 7, 6), kmax=7)
leaf_incoherent("V4 a27 = 1, a31 = 1", dict(s4, a27=1, a31=1))
s5 = dict(s4, a27=0, a28=0)
leaf_dead_x4("V5 x1**2 x2 x3 (a29 = 1)", dict(s5, a29=1))
s6 = dict(s5, 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("V6 cubique en (x3,x4) cube parfait : %s" % e, implied(s6, e, tot=(9, 8, 7)))
s6 = dict(s6, b0=0, b1=0, b2=0)
leaf_dead_x4("V6 b3 = 1, a31 = 0", dict(s6, b3=1, a31=0), tot=(9, 8, 7, 6), kmax=7)
leaf_incoherent("V6 b3 = 1, a31 = 1", dict(s6, b3=1, a31=1), tot=(9, 8, 7, 6, 5), kmax=8)
s7 = dict(s6, b3=0)
check("V7 x2 Q(x3,x4) carre parfait", implied(s7, R['b5'] ** 2 - 4 * R['b4'] * R['b6'], tot=(9, 8, 7)))
s7 = dict(s7, b4=0, b5=0)
leaf_dead_x4("V7 b6 = 1, a31 = 0", dict(s7, b6=1, a31=0), tot=(9, 8, 7, 6), kmax=7)
leaf_incoherent("V7 b6 = 1, a31 = 1", dict(s7, b6=1, a31=1), tot=(9, 8, 7, 6, 5), kmax=8)
leaf_zquad("V8 b6 = 0", dict(s7, b6=0), {'b10': 1, 'b12': 1, 'b11': 0})
bilan()