--- A. Theorem 1.1: the printed matrices and certificates
PASS  (2,4): 10 Pfaffian terms read from the paper
PASS  (2,4): dim U(V) = C(N,m) - n = 7
PASS  (2,4): every quadric used vanishes on 6 random decomposable vectors
PASS  (2,4): Q positive definite on U(V) (exact LDL^T, 7 positive pivots)   smallest pivot 0.387
PASS  (2,4): printed V equals the matrix in finder/out/cert_24_nice_int.json
PASS  (2,5): 35 multipliers read from the paper
PASS  (2,5): dim U(V) = C(N,m) - n = 11
PASS  (2,5): every quadric used vanishes on 6 random decomposable vectors
PASS  (2,5): Q positive definite on U(V) (exact LDL^T, 11 positive pivots)   smallest pivot 0.501
PASS  (2,5): printed V equals the matrix in finder/out/cert_25_nice_int.json
PASS  (3,3): 45 multipliers read from the certificate file; all are integers times 10^-7 with |lambda| <= 1
PASS  (3,3): dim U(V) = C(N,m) - n = 11
PASS  (3,3): every quadric used vanishes on 6 random decomposable vectors
PASS  (3,3): Q positive definite on U(V) (exact LDL^T, 11 positive pivots)   smallest pivot 5.78e-06
PASS  (3,3): printed V equals the matrix in finder/out/cert_33_nice.json
--- B. The case (2,2)
PASS  det(sI - F - GKH) = det[V'(s); K I_2] (80 points; both sides have degree <= 4 in s and are affine in each k_ij)
PASS  V': the conditions y12 = c, y23 = y14 = -c, y34 = 0, y13 + y24 = c
PASS  printed matrix: the conditions y12 = y23 = y14 = c, y34 = 0, y24 - y13 = c
PASS  printed matrix: det[V(z); L] = z^4 for L = [[1,-t,1,0],[t+1,-1,0,1]], t = (sqrt5-1)/2 (5 points, degree <= 4)
--- C. Example 4.5
PASS  (a): sum_I (V_R)_I y_I = y12(1+z^4) + (y14-y23) z + y34 z^2 + (y13+y24) z^3
PASS  (b): H_0 Hermitian and v H_0 v^* = 2 z^8
PASS  (b): det H_0 = -20
PASS  (b): the 8 x 9 system for K_v has rank 8, so dim K_v = 1
PASS  (b): the printed V_R is the realification of v
--- D. Determinant identities (random Gaussian-integer data, exact)
PASS  Lemma 4.1 (a = 2): det[Re S; Im S] = (-2i)^(-2) det[S; conj S]  (20 random S)
PASS  type j = 1: det[S; conj S] = 2i(tau1 conj(tau2) - tau2 conj(tau1)) and Delta_S = -Im(conj(tau1) tau2)  (20 random)
PASS  type j = 2: Delta_S = +-|det S'|^2  (20 random)
--- E. Degrees of Grassmannians
PASS  d(2,2), d(2,4), d(2,5), d(3,3), d(4,4) = 2, 14, 42, 42, 24024
PASS  d(m,p) is odd iff min = 1 or (min = 2 and max = 2^k - 1), for all m, p <= 40
--- F. The construction of Step 5 (Proposition 2.3) for the (2,4) matrix
PASS  W in P(m,p), W_I = T_eps((V_0)_I), coefficient of s^p of W equals V_0(eps), W_p g = [I | 0]   (eps = 1/3, 1/7)
PASS  det(sI - A_0 - B_0 K C_0) = sum_I (Wg)_I(s) y(K)_I for 4 random integer K (eps = 1/3, 1/7; 9 points, degree 8)
ALL LEAD CHECKS PASSED
