F1  Lemma 6.1 and rule (4): explicit change of basis W = V W_1, K <= 4
    K = 1: W L(4T) W^-1 is block diagonal over x with blocks theta_x(4T) by rule (4): ok  (0.0 s)
    K = 2: W L(4T) W^-1 is block diagonal over x with blocks theta_x(4T) by rule (4): ok  (0.0 s)
    K = 3: W L(4T) W^-1 is block diagonal over x with blocks theta_x(4T) by rule (4): ok  (0.0 s)
    K = 4: W L(4T) W^-1 is block diagonal over x with blocks theta_x(4T) by rule (4): ok  (0.0 s)
    self-test: with x_(j+k) instead of x_(j-k) the test fails at K = 3: detected
F2  (1/|G_K|) sum_x dim ker theta_x(4T), K <= 20 (exact over Q for K <= 10)
    K =  1: sum_x dim ker =        3; d_K =             3/2 = 1.5000000000  = direct group ring  (exact, 0.0 s)
    K =  2: sum_x dim ker =       10; d_K =             5/4 = 1.2500000000  = direct group ring  = Prop. 6.2  (exact, 0.0 s)
    K =  3: sum_x dim ker =        8; d_K =             1/3 = 0.3333333333  = direct group ring  (exact, 0.0 s)
    K =  4: sum_x dim ker =       24; d_K =             3/8 = 0.3750000000  = direct group ring  = Prop. 6.2  (exact, 0.0 s)
    K =  5: sum_x dim ker =       32; d_K =             1/5 = 0.2000000000  = direct group ring  (exact, 0.2 s)
    K =  6: sum_x dim ker =       80; d_K =            5/24 = 0.2083333333  = direct group ring  = Prop. 6.2  (exact, 2.1 s)
    K =  7: sum_x dim ker =      142; d_K =          71/448 = 0.1584821429  (exact, 0.1 s)
    K =  8: sum_x dim ker =      304; d_K =          19/128 = 0.1484375000  = Prop. 6.2  (exact, 0.2 s)
    K =  9: sum_x dim ker =      650; d_K =        325/2304 = 0.1410590278  (exact, 0.4 s)
    K = 10: sum_x dim ker =     1308; d_K =        327/2560 = 0.1277343750  = Prop. 6.2  (exact, 0.9 s)
    K = 11: sum_x dim ker =     2950; d_K =      1475/11264 = 0.1309481534  (0.1 s)
    K = 12: sum_x dim ker =     5848; d_K =        731/6144 = 0.1189778646  = Prop. 6.2  (0.4 s)
    K = 13: sum_x dim ker =    13262; d_K =      6631/53248 = 0.1245304988  (1.0 s)
    K = 14: sum_x dim ker =    26440; d_K =      3305/28672 = 0.1152692522  = Prop. 6.2  (2.6 s)
    K = 15: sum_x dim ker =    59132; d_K =    14783/122880 = 0.1203043620  (6.4 s)
    K = 16: sum_x dim ker =   119072; d_K =      3721/32768 = 0.1135559082  = Prop. 6.2  (15.4 s)
    K = 17: sum_x dim ker =   261802; d_K =  130901/1114112 = 0.1174935734  (34.5 s)
    K = 18: sum_x dim ker =   531968; d_K =       1039/9216 = 0.1127387153  = Prop. 6.2  (75.2 s)
    K = 19: sum_x dim ker =  1151706; d_K =  575853/4980736 = 0.1156160455  (183.1 s)
    K = 20: sum_x dim ker =  2355656; d_K =  294457/2621440 = 0.1123264313  = Prop. 6.2  (383.9 s)
    self-test: alpha = 1 + 2 pi'_0 pi_1 gives d_6 = 17/96 != 5/24: detected
F3  trace formula: 2^-K sum_x sum_i (P_x)_((k,i),(k,i)) = d_K for every index k, K <= 10
    K = 1: for every index k, 2^-K sum_x [ (P_x)_(k,u) + (P_x)_(k,v) ] = 3/2 = d_K: ok  (0.0 s)
    K = 2: for every index k, 2^-K sum_x [ (P_x)_(k,u) + (P_x)_(k,v) ] = 5/4 = d_K: ok  (0.0 s)
    K = 3: for every index k, 2^-K sum_x [ (P_x)_(k,u) + (P_x)_(k,v) ] = 1/3 = d_K: ok  (0.0 s)
    K = 4: for every index k, 2^-K sum_x [ (P_x)_(k,u) + (P_x)_(k,v) ] = 3/8 = d_K: ok  (0.0 s)
    K = 5: for every index k, 2^-K sum_x [ (P_x)_(k,u) + (P_x)_(k,v) ] = 1/5 = d_K: ok  (0.0 s)
    K = 6: for every index k, 2^-K sum_x [ (P_x)_(k,u) + (P_x)_(k,v) ] = 5/24 = d_K: ok  (0.0 s)
    K = 7: for every index k, 2^-K sum_x [ (P_x)_(k,u) + (P_x)_(k,v) ] = 71/448 = d_K: ok  (0.1 s)
    K = 8: for every index k, 2^-K sum_x [ (P_x)_(k,u) + (P_x)_(k,v) ] = 19/128 = d_K: ok  (0.2 s)
    K = 9: for every index k, 2^-K sum_x [ (P_x)_(k,u) + (P_x)_(k,v) ] = 325/2304 = d_K: ok  (0.6 s)
    K = 10: for every index k, 2^-K sum_x [ (P_x)_(k,u) + (P_x)_(k,v) ] = 327/2560 = d_K: ok  (1.3 s)
F4  Table 2, Remark 6.3, generating function (7), sqrt(5)/20
    Table 2: all fractions, decimals and differences to sqrt(5)/20 as printed: ok
    (7): coefficients of (1-2y-3y^2)^(-1/2) = T_N (N <= 40); (1/16)(5/16)^(-1/2) = sqrt(5)/20, minimal polynomial 80t^2 - 1; S_400 < sqrt(5)/20 < S_400 + tail; Remark 6.3: identity exact and both terms <= (1/4)(3/4)^P for P <= 80: ok
    second proof, chain K = 2^i: d_2 - sqrt5/20 = 1.14e+00, d_4 - sqrt5/20 = 2.63e-01, d_8 - sqrt5/20 = 3.66e-02, d_16 - sqrt5/20 = 1.75e-03, d_32 - sqrt5/20 = 3.32e-05, d_64 - sqrt5/20 = 1.21e-07, d_128 - sqrt5/20 = 4.53e-12, d_256 - sqrt5/20 = 1.66e-20, d_512 - sqrt5/20 = 6.08e-37, d_1024 - sqrt5/20 = 2.25e-69
TOTAL checks: 66, failures: 0; running time 709.2 s
ALL CHECKS PASSED
