=== Part A: the certificate d' = (9/100, 9/100, 9/100, 6/25) ===
PASS A1 Q1(d') = 107811/10^8 (direct product) :: 107811/100000000
PASS A2 Q1(d') from the expanded polynomial agrees
PASS A3 Q2(d') from the definition (formal algebra) = 2368521/(1.28*10^12) :: 2368521/1280000000000
PASS A4 Q2(d') from the expanded degree-8 polynomial agrees
PASS A5 Q2(d') = (1/2)(57/100)^2(15/100)^6
PASS A6 582 Q2 < Q1 < 583 Q2 (so Q1 > 500 Q2) :: Q1/Q2 = 582.6340
PASS A7 d' in the open cube and in Seigal's polytope (convex hull)
PASS A8 r = sqrt(1-4d') = (4/5,4/5,4/5,1/5) exactly
PASS A9 f(d') = (1/10,1/10,1/10,2/5); polygon fails: 2/5 > 3/10
PASS A10 rho_4(d') = 3(4/5) - 1/5 = 11/5 > 2
PASS A11 scale argument: for every admissible t, mu_4 >= 2/5 > 3*mu_1 (Lemma 2.1 at the tensor's own scale) :: 3*mu_1 <= 0.307799
=== Part B: boundary tensor and the segment above it ===
PASS B1 boundary tensor: norm 1, diagonal Gram matrices, Gram tuple (9,9,9,21)/100 :: 9/100, 9/100, 9/100, 21/100
PASS B2 on (9,9,9,b)/100, 21 < b <= 25: Q1 > 5e-4 > 4e-6 > Q2 (rigorous subinterval bounds) :: min Q1 >= 7.859e-04, max Q2 <= 2.631e-06
PASS B3 formula (3) as polynomial identities: Q1(a,a,a,b) = (a+b)^3(3a-b), Q2(a,a,a,b) = (9a-b)^2(a-b)^6/2 :: checked on a 9x9 grid; both sides have degree <= 8 in each of a, b
=== Part C: padding with zeros (Lemma 3.2, Corollary 1.2(b)) and d* ===
PASS C1 Lemma 3.2 (m=3, n=4) as identities: Q2(d,0) = (1/2)(2Q2(d))^2, Q1(d,0) = Q1(d)*s
PASS C2 (d',0,...,0), n = 5..8: Q2 from the definition = (1/2)q^(2^(n-4)), Q1 = Q1(d')(51/100)^(n-4) > Q2, polygon fails
PASS C3 general n >= 5: q < 3.8e-6, Q1(d') > q/2, 51/100 > q, 2^(n-4) >= n-3 (n <= 200)
PASS C4 d*: Q1 = 110937519e-12, q* = 2Q2 = (369/1000)^2(111/1000)^6 < 2.6e-7, Q1 > Q2
PASS C5 d*: rho_4 > 2 by squaring twice: (171/25 - 4 - 79/250)/4 = 631/1000 > 0 and (631/1000)^2 > 79/250
PASS C6 d*: rho_4 (60 digits) = 2.053200593222 > 2
PASS C7 (d*,0,...,0), n = 5..8: Q1 = Q1(d*)0.351^(n-4) > (1/2)q*^(n-3) >= Q2 (Q2 from the definition)
PASS C8 general n: Q1(d*) > q*/2 and 0.351 > q*
=== Part D: the family d(x) = (x, x, x, 3x - x^2) (Proposition 3.3) ===
PASS D1 Q1(d(x)) = x^5(4-x)^3 as a polynomial identity (from the expanded Q1)
PASS D2 Q2(d(x)) = x^8(6+x)^2(2-x)^6/2 as a polynomial identity (from the expanded Q2)
PASS D3 bounds on (0,1/12]: (4-x)^3 >= (47/12)^3 > 60; x^3(6+x)^2(2-x)^6/2 <= (1/12)^3(73/12)^2 2^6/2 < 0.69
PASS D4 3x - x^2 < 1/4 on (0,1/12] (increasing; value at 1/12 is 35/144)
PASS D5 identity (3r1-2)^2 - r4^2 = 4(3 - 6x - x^2 - 3r1) in Q[x][r1]/(r1^2-(1-4x))
PASS D6 identity (3-6x-x^2)^2 - 9(1-4x) = 30x^2 + 12x^3 + x^4
PASS D7 sign conditions for 0 < x < 5/36: 1-4x > 4/9 (so r1 > 2/3) and 3-6x-x^2 > 0
PASS D8 400 rational x in (0,1/12]: rho_4 - 2 > 0 (60 digits) and Q1 > Q2 (exact) :: min margin 4.348e-07
PASS D9 Q1 > 10^6 Q2 at x = 1/1000 (for any c > 0, Q1 > cQ2 for small x)
=== Part E: the path of Remark 3.6 and the interior claim ===
PASS E1 at the path vertices: a+b >= 3/10, 3a-b >= 3/100, 0 < 9a-b <= 2, |a-b| <= 15/100 (all affine/convex)
PASS E2 hence Q1 >= (3/10)^3 3/100 > 8e-4 and Q2 <= (1/2) 2^2 (15/100)^6 < 2.3e-5 along the path
PASS E3 exact Q1 - Q2 > 0 at 603 rational points of the path :: min 1.0763e-03
PASS E4 rigorous box |d - d'|_inf <= 1/1000 (n = 4): inside (0,1/4)^4, Q1 > Q2 and rho_4 > 2 everywhere :: Q1 >= 9.008e-04, Q2 <= 2.425e-06, rho_4 - 2 >= 0.1827
PASS E5 n = 5,6,7: on the box around (d',0,..,0) of radius 1e-4 (intersected with the cube) Q1 > Q2 and rho_4 > n-2
=== Part F: misprint in Theorem 1.4 (Remark 4.2) ===
PASS F1 GHZ tensor (e000+e111)/sqrt2: each flattening has rows of norm^2 1/2, orthogonal -> G_i = I/2, d_i = 1/4 :: p(000) = p(111) = 1/2; pairs differing in one coordinate are never both in the support
PASS F2 at (1/4,1/4,1/4): Q1 - Q2 = -1/512 (Q2 from the definition) and conic = 1/4 > 3/16
PASS F3 (1/5,1/100,1/100): Q1 < Q2, all conics <= 3/16, but d_1 > d_2 + d_3 (outside the convex hull)
PASS F4 grid r in {0,1/12,...,1}^3 (2197 points, exact): printed version wrong at 772, corrected at 0 :: printed 772, corrected 0
=== Part G: Theorem 1.3 and Proposition 4.1 ===
PASS G1 N_3 = -512 (Q1 - Q2) as an identity of polynomials in d
PASS G2 M_k = 16((d_i-d_j)^2 + (d_i+d_j)/2 - 3/16) as identities, k = 1,2,3
PASS G3 N_4 and M_i (n=4) have integer coefficients and degrees 8 and 4 :: 424 monomials in N_4
PASS G4 N_n invariant under r_j -> -r_j: expansion in r has only even exponents (n = 3, 4, 5)
PASS G5 Theorem 1.3 at exact rational-r points n = 3..6 (random, on facets, on L_+=0, grid corners) :: n=3: 1845 pts (1095 in G(B)), n=4: 1812 pts (1556 in G(B)), n=5: 1888 pts (1791 in G(B)), n=6: 1300 pts (1252 in G(B))
PASS G6 Theorem 1.3 at 3000 random rational d (n = 3, 4) with the expanded integer polynomials
=== Part H: the points used in the proof of Theorem 1.4; the case n = 2 ===
PASS H1 n = 3..10: facet points r^delta (ell_n = 0, ell_k = (2n-4)delta, phi(r) in U, sum_{j<n} d_j - d_n = (n-1)(n-2)delta^2/4) and r* on L_+ = 0 with phi(r*) in U
PASS H2 n = 2: det(MM^T) = det(M)^2 = det(M^TM) for 200 random rational 2x2 matrices
=== Part I: Remark 2.4(b) and Lemma 2.2 (construction) ===
PASS I1 for lambda in [0,1/2]^n (n = 3..6, 8000 rational points): Q1(lambda) >= 0 iff lambda in P_n
PASS I2 Lemma 2.2 exact for 420 rational lambda in P_n (n = 2..8, a third pushed onto facets): weights valid, total 2max(lambda), p even-weight with marginals lambda, all Gram matrices diag(1-lambda_j, lambda_j)

SUMMARY: 50 checks, 0 failed
