[1] identities in D = (-1,-3)_F, F = Q(alpha), exact
PASS  A H0 = -H0 B
PASS  B H0 = -H0 C
PASS  C H0 =  H1 A
PASS  A H1 =  H1 C
PASS  B H1 =  H1 B
PASS  C H1 =  H0 A
PASS  trd(A) = 0, nrd(A) = rho, A^2 = -rho
PASS  trd(B) = 0, nrd(B) = rho, B^2 = -rho
PASS  trd(C) = 0, nrd(C) = rho, C^2 = -rho
PASS  trd(H0) = -6 alpha, trd(H1) = -12
PASS  nrd(H0) = nrd(H1) = 36(rho + 1)
PASS  trd(H0)^2 = nrd(H0) (1 - alpha)/2 and trd(H1)^2 = nrd(H1) (5 + alpha)/2
PASS  (1 - alpha)/2 != (5 + alpha)/2  (equality would give alpha = -2, not a root)
[2] the splitting psi over Q(z): exact
PASS  I^2 = -1, J^2 = -3, IJ = -JI
PASS  matrix form: A H0 = -H0 B
PASS  matrix form: B H0 = -H0 C
PASS  matrix form: C H0 =  H1 A
PASS  matrix form: A H1 =  H1 C
PASS  matrix form: B H1 =  H1 B
PASS  matrix form: C H1 =  H0 A
[3] 2-adic data (roots exact modulo 2^200)
PASS  alpha = 10 mod 16, z = 2 mod 8, (2 alpha + 3)^2 = 17
PASS  psi(A), psi(B), psi(C) are 2-integral and = I mod 2; det = rho = 7 mod 8
PASS  A_t = [[3,4],[4,5]], B_t = [[5,2],[0,3]], C_t = [[7,1],[0,1]] mod 8
PASS  psi(H0)/4 = [[2,0],[6,7]] and psi(H1)/4 = [[2,6],[4,3]] mod 8
PASS  h_0 = [[2,8],[12,15]] and h_1 = [[2,11],[8,11]] mod 16
PASS  h_0 satisfies Lemma 2.2(b): a = 2 mod 4, b = 0 mod 2, c = 0 mod 4, d odd, v_2(det) = 1
PASS  h_1 satisfies Lemma 2.2(b): a = 2 mod 4, b = 1 mod 2, c = 0 mod 4, d odd, v_2(det) = 1
PASS  t-coordinates mod 2^120: A_t h_0 = -h_0 B_t
PASS  t-coordinates mod 2^120: B_t h_0 = -h_0 C_t
PASS  t-coordinates mod 2^120: C_t h_0 =  h_1 A_t
PASS  t-coordinates mod 2^120: A_t h_1 =  h_1 C_t
PASS  t-coordinates mod 2^120: B_t h_1 =  h_1 B_t
PASS  t-coordinates mod 2^120: C_t h_1 =  h_0 A_t
[4] the coding kappa_n (Proposition 3.3) for n <= 10
PASS  kappa_n is a bijection onto Z/2^n (n <= 10)
PASS  kappa_n(w x) = kappa_(n-1)(w) mod 2^(n-1) (n <= 10)
PASS  kappa_n(s(w)) = S_t(kappa_n(w)) mod 2^n for s = a, b, c and all w (n <= 10)
PASS  negative control: with the matrices of b and c swapped the equivariance fails on level 3
[5] Theorem 4.1 (Theorem B), finite part
PASS  |H_3| = 32 and |H_4| = 256 = 8 |H_3|
PASS  |Q_3| = 32 and |Q_4| = 256 (enumeration)
PASS  H_k is contained in Q_k, hence H_k = Q_k (k = 3, 4, 5; |H_5| = 2048)
PASS  |GL_2(Z/8)| = 1536, |PGL_2(Z/8)| = 1536/4 = 384, index [PGL_2(Z_2) : Q] = 384/32 = 12
[6] level quotients of G(B) and the Moebius action of Q (Remark 4.2)
PASS  n=3: G(B)_n = image of Q on level n (via kappa_n); order 2^5; kernel of size 1; 15 involutions
PASS  n=4: G(B)_n = image of Q on level n (via kappa_n); order 2^7; kernel of size 2; 43 involutions
PASS  n=5: G(B)_n = image of Q on level n (via kappa_n); order 2^10; kernel of size 2; 167 involutions
PASS  n=6: G(B)_n = image of Q on level n (via kappa_n); order 2^13; kernel of size 2; 647 involutions
[7] Corollary B
PASS  beta_a, beta_b, beta_c act on level 3 as three distinct non-trivial involutions
PASS  eps1, eps2, eps3 are homomorphisms on Q_4 (all 65536 pairs)
PASS  normalized A_t, B_t, C_t mod 16 = (15,4,12), (15,6,0), (15,1,8); eps values (1,0,1), (1,0,0), (1,1,0); det 1 over F_2
PASS  |P_4| = 256 and T, w generate P_4
PASS  P_4^ab has order 16 and exponent 8
PASS  d(G(B)_3) = 3: |G(B)_3| = 32 and the subgroup generated by squares has index 8
PASS  the four characters of I are homomorphisms on I_3 (|I_3| = 128) with unit-vector values on diag(-1,1), diag(5,1), T, L
[8] Lemma 2.1 and the index of the closure of G(A) in J
PASS  level 6: alpha_s = tau o beta_s and tau alpha_s tau = alpha_s^-1 for s = a, b, c
PASS  |G(A)_4| = 128 and tau does not act on level 4 as an element of G(A)_4 (so the index is 2)
[9] Lemma 6.2: fixed points and multipliers of h_0, h_1
PASS  h_0: fixed point p_0 (h(p) = p mod 2^160), v_2(lambda_0) = 1, (lambda+1)^2 det = lambda tr^2 mod 2^156
PASS  h_1: fixed point p_1 (h(p) = p mod 2^160), v_2(lambda_1) = 1, (lambda+1)^2 det = lambda tr^2 mod 2^156
PASS  lambda_1/lambda_0 = 377 mod 2^10 (in particular lambda_0 != lambda_1)
PASS  tau'(p_0) = p_1 mod 2^120
PASS  difference quotients q_j of tau' at x_j = h_0^j(1): |q_j| = 1 and q_j = 3, 11 mod 16 for even, odd j (2 <= j <= 21)
PASS  q_(j+1)/q_j = 377 mod 2^10 for 12 <= j <= 20
checks: 60, failed: 0, time 1.1 s
ALL CHECKS PASSED
