Part A: exact constants
  ok    A1  t^4 - 10t^2 + 1 has no rational root and no factorisation into two integer quadratics   [required a^2 in {12, 8}: not squares]
  ok    A2  s = sqrt2 + sqrt3 satisfies s^4 - 10 s^2 + 1 = 0
  ok    A3  sqrt2 = (s^3 - 9s)/2 and sqrt3 = (11s - s^3)/2, so Q(s) = Q(sqrt2, sqrt3)
        => [Q(sqrt2,sqrt3):Q] = 4; it is spanned by 1, sqrt2, sqrt3, sqrt6, which are therefore a Q-basis;
           in particular 1, sqrt2, sqrt3 are linearly independent over Q (used in Theorem A).
  ok    A4  X^6 - 2 is Eisenstein at 2, hence irreducible; 1, theta, ..., theta^5 are Q-independent
  ok    A5  theta = 2^(1/6) in the arithmetic: theta^6 = 2
  ok    A6  Theorem D: Pf(lambda) = l12 l34 - l13 l24 + l14 l23 = theta^5   [QT('0', '0', '0', '0', '0', '1')]
  ok    A7  Theorem D: det(lambda) = Pf^2 = theta^10 = 2 theta^4
  ok    A8  Theorem D: det A(x) = theta^10 (x1x2x3x4)^2 at 5 random integer points (A = D lambda D)
Part B: finite identities
  ok    B1  Jacobi identity, symbolic lambda, n = 3, all coordinate triples
  ok    B1  Jacobi identity, symbolic lambda, n = 4, all coordinate triples
  ok    B1  Jacobi identity, symbolic lambda, n = 5, all coordinate triples
  ok    B2  Jacobi identity, symbolic lambda, n = 3, on 4 random polynomial triples
  ok    B3  Jacobi identity for the brackets of Theorems A and D on random polynomial triples
  ok    B4  Lemma 2.2(a): {x^a, x^b} = lambda(a,b) x^(a+b), symbolic lambda, n = 3,4,5, 45 random pairs
  ok    B5  Lemma 2.3(b), n = 3: lambda k_lambda = 0 with k_lambda = (l23, l31, l12) (symbolic)
  ok    B6  Lemma 2.3(b), n = 3: lambda(a,b) = k_lambda . (a x b) on all 9 basis pairs (both sides bilinear)
  ok    B7  Remark 6.1: {f,g} dx^dy^dz = df^dg^kappa, kappa = l23 yz dx + l31 zx dy + l12 xy dz (5 random pairs)
  ok    B8  Proposition 6.2: {x,phi}{y,z} + {y,phi}{z,x} + {z,phi}{x,y} = 0 (symbolic lambda, 3 random phi)
  ok    B9  Proposition 6.2: phi * bracket is Poisson for phi = x + 2y - z and phi = x^2 + yz (symbolic lambda)
  ok    B10 Example 4.1: {x^2 y^3 z, x} = 0 for (a,b,c) = (1,2,3); {xz, y} = 0 for (1,1,sqrt2)
Part C: Lemma 3.1, the top coefficient of {p,q}
  ok    C   Theorem A bracket, graded lex order: coefficient identity on 60 random pairs (59 with independent leading exponents, where LE{p,q} = LE p + LE q)
  ok    C   Theorem A bracket, lex order: coefficient identity on 60 random pairs (53 with independent leading exponents, where LE{p,q} = LE p + LE q)
  ok    C   Theorem A bracket, graded reverse lex order: coefficient identity on 60 random pairs (57 with independent leading exponents, where LE{p,q} = LE p + LE q)
  ok    C   CONTROL Theorem A bracket, control (not compatible with addition): the identity fails for some pairs   [59 failures in 60 pairs]
  ok    C   Theorem D bracket, graded lex order: coefficient identity on 60 random pairs (59 with independent leading exponents, where LE{p,q} = LE p + LE q)
  ok    C   Theorem D bracket, lex order: coefficient identity on 60 random pairs (56 with independent leading exponents, where LE{p,q} = LE p + LE q)
  ok    C   Theorem D bracket, graded reverse lex order: coefficient identity on 60 random pairs (56 with independent leading exponents, where LE{p,q} = LE p + LE q)
  ok    C   CONTROL Theorem D bracket, control (not compatible with addition): the identity fails for some pairs   [42 failures in 60 pairs]
Part D: commuting monomial pairs with linearly independent exponents
  ok    D   n = 3, degree <= 6, (a,b,c) = (1, sqrt2, sqrt3)   Theorem A, rho = 3: 0 pairs (expected 0)
  ok    D   n = 3, degree <= 6, (a,b,c) = (1, 2, 3)           rho = 1: 191 pairs (expected 191)   [first: ((0, 0, 1), (2, 3, 0))]
  ok    D   n = 3, degree <= 6, (a,b,c) = (1, 1, sqrt2)       rho = 2, n = (1,0,-1): 86 pairs (expected 86)   [first: ((0, 1, 0), (1, 0, 1))]
  ok    D   n = 3, degree <= 6, (a,b,c) = (1, sqrt2, -1-sqrt2) rho = 2, n = (1,1,1): 0 pairs (expected 0)
  ok    D   n = 3, degree <= 6, (a,b,c) = (sqrt2, -2, 1)      rho = 2, n = (1,2,0): 0 pairs (expected 0)
  ok    D   n = 4, degree <= 4, Theorem D bracket: 0 pairs (expected 0)
  ok    D   n = 4, degree <= 4, CONTROL all lambda_ij = 1: 156 pairs (expected 156)
Part E: Theorem B (dimension three)
  ok    E1  Theorem B, rho = 2: 578 primitive relation vectors n in [-4,4]^3: criterion = bounded search (exponents <= 4) in all cases   [402 with a system]
  ok    E2  Theorem B, rho = 2: the witnesses of the proof are in N^3, independent and lambda-orthogonal (402 cases)
  ok    E3  Theorem B, rho = 1: for all 578 primitive kernel vectors in [-4,4]^3 the pair of the proof is a system
Part F: Proposition 4.2(b) (rational constants, n = 4, nondegenerate)
  ok    F   all 13312 nondegenerate integer lambda with entries in [-2,2]: the two monomials of the proof commute and have independent exponents
Part G: centralizers in bounded degree, certified modulo p (sanity checks, not used in proofs)
  ok    G0  modulus: R2^2 = 2, R3^2 = 3, RT^6 = 2 mod P
  ok    G   Theorem A: f = x+y+z, deg g <= 10: centralizer = polynomials in f (dim 11, certified)   [0.1s]
  ok    G   Theorem A: f = xy+z^2+x, deg g <= 10: centralizer = polynomials in f (dim 6, certified)   [0.0s]
  ok    G   Theorem A: f = x+yz, deg g <= 10: centralizer = polynomials in f (dim 6, certified)   [0.0s]
  ok    G   Theorem A: f = x^2y+z^3+y, deg g <= 10: centralizer = polynomials in f (dim 4, certified)   [0.0s]
  ok    G   Theorem A: f = xyz+x+y+z, deg g <= 10: centralizer = polynomials in f (dim 4, certified)   [0.1s]
  ok    G   Theorem A: f = x^2y^3z (a monomial), deg g <= 18: centralizer = polynomials in f (dim 4, certified)   [0.1s]
  ok    G   Theorem D: f = x1+x2+x3+x4, deg g <= 7: centralizer = polynomials in f (dim 8, certified)   [0.1s]
  ok    G   Theorem D: f = x1x2+x3+x4^2, deg g <= 7: centralizer = polynomials in f (dim 4, certified)   [0.0s]
  ok    G   CONTROL (1,2,3): f = x+y+z, deg g <= 10: kernel mod P has dim 16 > 11 = number of powers of f   [0.1s]
  ok    G   CONTROL (1,1,sqrt2): f = y, deg g <= 10: kernel mod P has dim 36 > 11 = number of powers of f   [0.0s]
  ok    G   CONTROL n=4, all lambda_ij = 1: f = x3+x2x4, deg g <= 7: kernel mod P has dim 20 > 4 = number of powers of f   [0.0s]
TOTAL failures: 0
running time: 3 s
