====================================================================================================
[1] Theorem A
PASS  (a) 28 interpolation points (0, +-e_i, e_i + e_j)
PASS  (a) |2z - 2c|^2 = 4 f(z) + 2 on these points, hence identically
PASS  (a) 4R^2 = 4N + 2, so for integer z:  z in B <=> f(z) <= 158906
PASS  (b) |n|^2 = 10843, n primitive, 2 n.c = 9
PASS  (b) 2 * 10843 * 317813 = 6892092718 < 6892154361 = 83019^2
PASS  (b) hence every lattice point z of B has n.z >= -41504 (integer form of Cauchy-Schwarz)
PASS  (b) (consistency) the same test does not exclude the level h itself
      4|n|^4 rho^2 = 2932261647 = 10843 * 270429;  rho^2 = 270429/43372 ~ 6.235106
      coordinate intervals: [(136, 140), (174, 178), (-193, -189), (216, 220), (155, 159), (-6, -2)]
PASS  (c) rho^2 = 270429/43372
      method I  : 3125 tuples (z_1..z_5), 6 lattice points of B on the level
PASS  (c) method I gives exactly F_0..F_5
      method II : 15625 tuples (z_1..z_6), 6 lattice points of B on the level
PASS  (c) method II gives exactly F_0..F_5
      method III: Fincke-Pohst, squared distance of c to the level = 6891822289/43372, budget = 270429/43372; 6 lattice points
PASS  (c) method III: distance^2 = (h - n.c)^2/|n|^2 and budget = rho^2
PASS  (c) method III gives exactly F_0..F_5
PASS  (d) n.F_i = -41504 and f(F_i) = 158906 for all i (on the sphere)
      5x5 minors of (F_i - F_0), column k dropped (k = 1..6): [72, -92, -100, -114, 82, 2]
PASS  (e) minors = -2 (-1)^(k-1) n_k (so gcd 2 and the F_i span n^perp)
PASS  (e,f) Theorem A: the 6 points are affinely independent (a maximal minor of (F_i - F_0) is non-zero)
PASS  (e,f) Theorem A: gcd of the maximal minors of (F_i - F_0) = 2 (index 2 in n^perp cap Z^6; n primitive)
PASS  (e,f) Theorem A: w = sum lam_i F_i with sum lam_i = 3, all lam_i >= 0 and some lam_i non-integral
      barycentric coordinates of w: ['1/2', '1/2', '1/2', '1/2', '1/2', '1/2']
PASS  (e,f) Theorem A: n.w = 3 h and n.F_i = h
PASS  (e,f) Theorem A: (sanity) w + t F_j is not a sum of 3 + t of the F_i, t = 0..3, all j
PASS  (f) F_0 + ... + F_5 = 2w = (826, 1056, -1144, 1312, 944, -24)
PASS  (f) all barycentric coordinates of w equal 1/2
PASS  (g) f(0) = 0 and f(e_1..e_6) = 1,1,0,1,0,1: 0, e_1, ..., e_6 lie in B (spanning)
PASS  (control) with 158907 instead of 158906 the level n.z = h holds 14 lattice points, not 6
PASS  (control) for the ball of the same radius centred at 0 the bound fails; the level h - 1 holds 306 lattice points
====================================================================================================
[2] Padding with zeros: the same ball in Z^7 and Z^8
PASS  d = 7: level bound n'.z >= h on the lattice points of the ball
      d = 7: method I, 15625 tuples, 6 lattice points on the level
PASS  d = 7: the lattice points on n'.z = h are exactly (F_i, 0)
PASS  d = 7: method II (78125 tuples) agrees
PASS  d = 7: witness (w, 0) has all coordinates 1/2 w.r.t. the (F_i, 0)
PASS  d = 7: 0 and e_1..e_7 lie in the ball (spanning)
PASS  d = 8: level bound n'.z >= h on the lattice points of the ball
      d = 8: method I, 78125 tuples, 6 lattice points on the level
PASS  d = 8: the lattice points on n'.z = h are exactly (F_i, 0)
PASS  d = 8: method II (390625 tuples) agrees
PASS  d = 8: witness (w, 0) has all coordinates 1/2 w.r.t. the (F_i, 0)
PASS  d = 8: 0 and e_1..e_8 lie in the ball (spanning)
====================================================================================================
[3] Theorem 4': centre (0,1/2,0,0,1/2,0), R^2 = 51196593/2, i.e. |z|^2 - z_2 - z_5 <= 25598296
PASS  4R^2 = 4 * 25598296 + 2 and |n|^2 = 402222
PASS  level bound: lattice points of the ball have n.z >= -3208646
      method I: 25088 tuples, 6 lattice points on the level
PASS  the lattice points on n.z = -3208646 are exactly the six listed points
PASS  method II (175616 tuples) agrees
PASS  Theorem 4': the 6 points are affinely independent (a maximal minor of (F_i - F_0) is non-zero)
PASS  Theorem 4': gcd of the maximal minors of (F_i - F_0) = 2 (index 2 in n^perp cap Z^6; n primitive)
PASS  Theorem 4': w = sum lam_i F_i with sum lam_i = 3, all lam_i >= 0 and some lam_i non-integral
      barycentric coordinates of w: ['1/2', '1/2', '1/2', '1/2', '1/2', '1/2']
PASS  Theorem 4': n.w = 3 h and n.F_i = h
PASS  Theorem 4': (sanity) w + t F_j is not a sum of 3 + t of the F_i, t = 0..1, all j
PASS  Theorem 4': all coordinates of the witness are 1/2
PASS  Theorem 4': 0 and e_1..e_6 lie in the ball (spanning)
====================================================================================================
[4] Theorem 4 and the 7-dimensional certificate (ball centre c_S + 8n, rational arithmetic)
PASS  Theorem 4: n primitive, n.v_i = 0, v_0 = 0
PASS  Theorem 4: circumcentre c_S and r_S^2 = 5936999/402222 as stated
PASS  Theorem 4: half-space condition 2s + 1/|n|^2 > r_S^2 (s = 8)
PASS  Theorem 4: R^2 = 10354088323175/402222
PASS  Theorem 4: every lattice point of the ball has n.z >= 0
      Theorem 4: 25088 tuples, 6 lattice points of the ball on n.z = 0
PASS  Theorem 4: the lattice points of the ball on n.z = 0 are exactly v_0..v_5
PASS  Theorem 4: the 6 points are affinely independent (a maximal minor of (F_i - F_0) is non-zero)
PASS  Theorem 4: gcd of the maximal minors of (F_i - F_0) = 2 (index 2 in n^perp cap Z^6; n primitive)
PASS  Theorem 4: w = sum lam_i F_i with sum lam_i = 3, all lam_i >= 0 and some lam_i non-integral
      barycentric coordinates of w: ['1/2', '1/2', '1/2', '1/2', '1/2', '1/2']
PASS  Theorem 4: n.w = 3 h and n.F_i = h
PASS  Theorem 4: (sanity) w + t F_j is not a sum of 3 + t of the F_i, t = 0..1, all j
PASS  Theorem 4: z0 = round(c) = [3094, 202, -2232, -2842, 1752, 9] and z0 + e_i lie in the ball (spanning)
PASS  Theorem 4: ball centre c_S + 8n as stated
PASS  Theorem 4: all barycentric coordinates of x are 1/2
PASS  d = 7: n primitive, n.v_i = 0, v_0 = 0
PASS  d = 7: circumcentre c_S and r_S^2 = 2081093/244974 as stated
PASS  d = 7: half-space condition 2s + 1/|n|^2 > r_S^2 (s = 8)
PASS  d = 7: R^2 = 3840786764357/244974
PASS  d = 7: every lattice point of the ball has n.z >= 0
      d = 7: 38880 tuples, 7 lattice points of the ball on n.z = 0
PASS  d = 7: the lattice points of the ball on n.z = 0 are exactly v_0..v_6
PASS  d = 7: the 7 points are affinely independent (a maximal minor of (F_i - F_0) is non-zero)
PASS  d = 7: gcd of the maximal minors of (F_i - F_0) = 2 (index 2 in n^perp cap Z^7; n primitive)
PASS  d = 7: w = sum lam_i F_i with sum lam_i = 3, all lam_i >= 0 and some lam_i non-integral
      barycentric coordinates of w: ['1/2', '0', '1/2', '1/2', '1/2', '1/2', '1/2']
PASS  d = 7: n.w = 3 h and n.F_i = h
PASS  d = 7: (sanity) w + t F_j is not a sum of 3 + t of the F_i, t = 0..1, all j
PASS  d = 7: z0 = round(c) = [-1919, 2305, -1999, -169, -545, -1536, 10] and z0 + e_i lie in the ball (spanning)
PASS  d = 7: |n|^2 = 244974; coordinates of x are (1/2, 0, 1/2, 1/2, 1/2, 1/2, 1/2)
====================================================================================================
[5] Second question: P = conv(0, e_1..e_6, (3,3,3,3,3,3,4)), Q = 3P (m = 4)
PASS  det of the eight vectors (v, 1) is +-4
      box points: [(0, 0, 0, 0, 0, 0, 0, 0), (1, 1, 1, 1, 1, 1, 1, 2), (2, 2, 2, 2, 2, 2, 2, 4), (3, 3, 3, 3, 3, 3, 3, 6)]
PASS  box points are exactly (j,...,j; 2j), j = 0..3
      |L(Q)| = 128
PASS  |L(Q)| = 128
PASS  (3,...,3) lies in 2Q = 6P
PASS  (3,...,3) is not a sum of two lattice points of Q (Q is not IDP)
PASS  0, e_1..e_6 and (1,...,1) are lattice points of Q (spanning)
      |L(3Q)| = 15784
PASS  |L(3Q)| = 15784 and every lattice point of 3Q is a sum of three lattice points of Q
====================================================================================================
79 checks, 0 failed; time 2.0 s
ALL CHECKS PASSED
