== A. Section 2 and Lemma 4.1: the diamond, the colouring, the coordinates, the matrix (n <= 30)
PASS A1 |AD_n| = 2n(n+1), n(n+1) black and n(n+1) white squares
PASS A2 (p,q) = (x+y+n, x-y+n) is a bijection onto {0..2n}^2 with p+q odd; black iff p = n+1 (mod 2)
PASS A3 Lemma 2.1: neighbours {E,N} on p=0, {W,S} on p=2n, {E,S} on q=0, {W,N} on q=2n, all four inside; no square on two edges
PASS A4 Proposition 2.2: n^2 + (n-1)^2 blocks of 2x2 squares, each with exactly one -1 (product of signs -1)
PASS A5 Lemma 4.1: black (s even, t odd), white (s odd, t even); N(b) = (s+1,t-1), S(b) = (s-1,t+1), {E(b),W(b)} = {(s+1,t+1),(s-1,t-1)}
PASS A6 Sigma_S = {s = 0} = {p = 0} (n odd) / {q = 2n} (n even), Sigma_N = {t = 0} = {q = 0} (n odd) / {p = 2n} (n even), n squares each
PASS A7 the edges p = 0, 2n are black iff n is odd; the edges q = 0, 2n are black iff n is even
== B. Lemma 3.1 (n <= 30)
PASS B1 K(1/2 * 1_W) = 1_B - 1_{Sigma_S}
PASS B2 K^T(1/2 * 1_B) = 1_W - 1_{Sigma_N}
== C. Lemma 4.2 (n <= 30)
PASS C1 kappa_n(m,k) by the binomial convolution equals [xi^m](1-xi)^k(1+xi)^(n-k) by multiplication
PASS C2 (1-xi)^k(1+xi)^(n-k) + (1-xi)^(k+1)(1+xi)^(n-k-1) = 2R and the difference = -2 xi R, R = (1-xi)^k(1+xi)^(n-1-k), 0 <= k <= n-1
PASS C3 kappa(m,k) + kappa(m,k+1) = 2 lambda(m,k), kappa(m+1,k+1) - kappa(m+1,k) = -2 lambda(m,k), lambda(0,k) = 1, lambda(n,k) = 0 (deg R = n-1)
== D. Proposition 4.3 and Corollary 1.3: the explicit solutions (n <= 30)
PASS D1 Proposition 4.3: K(2 phi) = 2 * 1_{Sigma_S}, 2 phi(s,t) = -kappa_n((s+1)/2, t/2), with K built from the definition
PASS D2 Corollary 1.3 (columns): K^T(2 psi) = 2 * 1_{Sigma_N}, 2 psi(s,t) = -kappa_n((t+1)/2, s/2)
== E. Theorem 1.2 from the closed form (n <= 30)
PASS E1 on Sigma_N the values -2 phi are C(n,1), ..., C(n,n)
PASS E2 sum of phi over Sigma_N = -(2^n - 1)/2
PASS E3 n(n+1)/2 + n/2 - (2^n - 1)/2 = (n+1)^2/2 - 2^(n-1) = (n-1)(n+3)/2 - 2^(n-1) + 2
PASS E4 Remark 5.1: sum of phi over all white squares = -(2^n - n - 1)/2, and n(n+1)/2 + that = the formula
     values of the formula, n = 1..12: 1, 5/2, 4, 9/2, 2, -15/2, -32, -175/2, -206, -903/2, -952, -3927/2
== F. Exact inverse of K_n (n <= 8)
     n = 1: N = 2, det K_n = -2, sum of all entries of K_n^(-1) = 1, boundary block = -1/2
     n = 2: N = 6, det K_n = -8, sum of all entries of K_n^(-1) = 5/2, boundary block = -3/2
     n = 3: N = 12, det K_n = 64, sum of all entries of K_n^(-1) = 4, boundary block = -7/2
     n = 4: N = 20, det K_n = 1024, sum of all entries of K_n^(-1) = 9/2, boundary block = -15/2
     n = 5: N = 30, det K_n = -32768, sum of all entries of K_n^(-1) = 2, boundary block = -31/2
     n = 6: N = 42, det K_n = -2097152, sum of all entries of K_n^(-1) = -15/2, boundary block = -63/2
     n = 7: N = 56, det K_n = 268435456, sum of all entries of K_n^(-1) = -32, boundary block = -127/2
     n = 8: N = 72, det K_n = 68719476736, sum of all entries of K_n^(-1) = -175/2, boundary block = -255/2
PASS F1 K X = I exactly (X = K_n^(-1), rows indexed by white squares)
PASS F2 |det K_n| = 2^(n(n+1)/2)
PASS F3 Theorem 1.2: sum of all entries of K_n^(-1) = (n-1)(n+3)/2 - 2^(n-1) + 2
PASS F4 Proposition 3.2: sum of K_n^(-1) over Sigma_N x Sigma_S = 1/2 - 2^(n-1), and S_n = n(n+1)/2 + n/2 + it
PASS F5 Corollary 1.3: row sums (1 - kappa_n((s+1)/2, t/2))/2 and column sums (1 - kappa_n((t+1)/2, s/2))/2
PASS F6 all row sums and all column sums are half-integers
PASS F7 K_n^(-1) 1_{Sigma_S} = phi (Proposition 4.3, by the inverse)
== G. Lemma 2.3: colouring and top/bottom (n <= 8)
PASS G1 both checkerboard colourings, white square on top or at the bottom: the same entry sum (the formula)
== H. Section 6: other Kasteleyn signings (computations; n <= 8)
     alternate columns (i even): entry sums for n = 1..8: 1, 5/2, 4, 6, 9, 25/2, 16, 20
PASS H alternate columns (i even): Kasteleyn condition on every 2x2 block; |det| = 2^(n(n+1)/2); explicit +-1 gauge to K_n; sum predicted from K_n^(-1) and the gauge; sums as stated in Section 6
     alternate columns (i odd): entry sums for n = 1..8: 1, 5/2, 4, 6, 9, 25/2, 16, 20
PASS H alternate columns (i odd): Kasteleyn condition on every 2x2 block; |det| = 2^(n(n+1)/2); explicit +-1 gauge to K_n; sum predicted from K_n^(-1) and the gauge; sums as stated in Section 6
     Kasteleyn-Wilson (row l = lower row): entry sums for n = 1..8: 1, 5/2, 11/2, 8, 13, 31/2, 45/2, 23
PASS H Kasteleyn-Wilson (row l = lower row): Kasteleyn condition on every 2x2 block; |det| = 2^(n(n+1)/2); explicit +-1 gauge to K_n; sum predicted from K_n^(-1) and the gauge; sums as stated in Section 6
     Kasteleyn-Wilson (row l = upper row): entry sums for n = 1..8: 1, 5/2, 11/2, 8, 13, 31/2, 45/2, 23
PASS H Kasteleyn-Wilson (row l = upper row): Kasteleyn condition on every 2x2 block; |det| = 2^(n(n+1)/2); explicit +-1 gauge to K_n; sum predicted from K_n^(-1) and the gauge; sums as stated in Section 6
PASS H the alternate-columns sums differ from the formula exactly for n = 4..8 (n <= 8)
PASS H Section 6: every black square with four neighbours has exactly one domino with -1 (Problem 12 signs)
PASS H Section 6: alternate columns -- this fails at every black square with four neighbours
PASS H Section 6: Kasteleyn-Wilson -- it fails exactly at the black squares with four neighbours of the row y = 1/2 (lower-row reading), resp. y = -1/2 (upper-row reading)
== N. Negative controls (each must be detected)
PASS N1 changing one value of 2 phi violates K(2 phi) = 2 * 1_{Sigma_S} (n <= 30)
PASS N2 the coefficients of (1+xi)^k (1-xi)^(n-k) do not solve the equation (n <= 30)
PASS N3 the closed form does not solve the equation for the convention 'white square at the bottom' (2 <= n <= 30; that matrix has the same entry sum but another solution vector)
PASS N4 the wrong formula (n+1)^2/2 - 2^n differs from the formula for every n <= 30
TOTAL: 38 checks, 0 failed; ALL CHECKS PASSED  (2.1 s)
