P1 Lemma 2.1: recurrence (1) = up/down permutation counts (n <= 9): PASS ; rows 1..6 = [[1], [0, 1], [1, 1, 0], [0, 1, 2, 2], [5, 5, 4, 2, 0], [0, 5, 10, 14, 16, 16]]
P1 Lemma 2.1: row sums of (1) = E_n from sec x + tan x (n <= 1000; series division n <= 60): PASS ; E_0..E_12 = [1, 1, 1, 2, 5, 16, 61, 272, 1385, 7936, 50521, 353792, 2702765]
P2 Lemma 2.2: T_{2j-1} = 2^{2j}(2^{2j}-1)|B_{2j}|/(2j) and v_2(B_{2j}) = -1 (j <= 100): PASS
P2 Lemma 2.2: v_2(T_(2j-1)) = h(j) = 2j-2-v_2(j) (j <= 500): PASS ; h(1..16) = [0, 1, 4, 4, 8, 9, 12, 11, 16, 17, 20, 20, 24, 25, 28, 26]
P3 Theorem 2.4 (Stern): v_2(E*_2m - E*_2n) = 1 + v_2(m-n) for all 0 <= n < m <= 500: PASS ; (125250 pairs)
P3 Corollary 2.5: (a) S_2m = 1 mod 4; (b) period 2^(k-1) of S_2m mod 2^k (2<=k<=12); (c) 2^(k-2) never a period (3<=k<=12): PASS ; unsigned counterexample S_0 = S_2 = 1: True
P4 Lemma 3.1: v_2(e_(n,i)) >= H(i,n) for all 1 <= i <= n, 2 <= n <= 1000: PASS ; (500499 entries)
P5 Lemma 3.2: v_2(e_(2j*,i)) = G(i) for all 998 columns 3 <= i <= 1000 with 2j* <= 1000: PASS ; witness rows for i = 3..24: [4, 4, 6, 6, 8, 8, 10, 10, 12, 12, 16, 16, 16, 16, 18, 18, 20, 20, 22, 22, 24, 24]
P6 Theorem 1.1: m_i = G(i) and m_i weakly increasing for i <= 1000: PASS ; m_1..m_24 = [0, 0, 1, 1, 4, 4, 4, 4, 8, 8, 9, 9, 11, 11, 11, 11, 16, 16, 17, 17, 20, 20, 20, 20]
P6 Theorem 1.1: u_k (max) = number of diagonals with m_i < k = 2J(k) for k <= 1000; Table 1 of the source: PASS ; u_1..u_40 = [2, 4, 4, 4, 8, 8, 8, 8, 10, 12, 12, 16, 16, 16, 16, 16, 18, 20, 20, 20, 24, 24, 24, 24, 26, 28, 32, 32, 32, 32, 32, 32, 34, 36, 36, 36, 40, 40, 40, 40]
P7 E_n mod 2^64 by the triangle agrees with exact E_n (n <= 1000): PASS
P7 Theorem 1.2 by brute force on n <= 16448: s(2^k) = u_k, d(2^k) as predicted, k = 1..13: PASS
     k=1: s=2 (u_k=2), d=2 (predicted 2)
     k=2: s=4 (u_k=4), d=2 (predicted 2)
     k=3: s=4 (u_k=4), d=8 (predicted 8)
     k=4: s=4 (u_k=4), d=16 (predicted 16)
     k=5: s=8 (u_k=8), d=32 (predicted 32)
     k=6: s=8 (u_k=8), d=64 (predicted 64)
     k=7: s=8 (u_k=8), d=128 (predicted 128)
     k=8: s=8 (u_k=8), d=256 (predicted 256)
     k=9: s=10 (u_k=10), d=512 (predicted 512)
     k=10: s=12 (u_k=12), d=1024 (predicted 1024)
     k=11: s=12 (u_k=12), d=2048 (predicted 2048)
     k=12: s=16 (u_k=16), d=4096 (predicted 4096)
     k=13: s=16 (u_k=16), d=8192 (predicted 8192)
P8 Lemma 5.1: (S1), (S2), (R1), (R2) and (R3) (for j <= 2^(a+2)) for 2 <= a <= 20: PASS
P9 examples (8), (9) of the source: PASS
P9 Theorem 1.3: f^n(2,4,4,4) = (2J(1),...,2J(2^(n+2))) up to length 1048576; cut index 2^a-a-1 for 2 <= a <= 19: PASS
P10 Remark 6.1: first entries of rows 2J-1, 2J (J >= 2); e_(2J,4) = 3S_(2J-2) - S_(2J-4), e_(2J+1,4) = S_2J - 3S_(2J-2); every entry of D_4 (rows 4..1000) has v_2 = 1: PASS ; smallest valuations in D_3: [1, 2, 3, 4, 5, 6]
     A108039 literal reading (valuation exactly n; rows <= 1000), n = 0..17: [2, 4, 3, 3, 8, 7, 7, 7, 10, 12, 11, 16, 15, 15, 15, 15, 18, 20]
     A108039 "<= n" reading = u_(n+1),                          n = 0..17: [2, 4, 4, 4, 8, 8, 8, 8, 10, 12, 12, 16, 16, 16, 16, 16, 18, 20]
P11 Appendix A: E*_N = sum_k 2^-k sum_j (-1)^j C(k,j) (2j+1)^N for N <= 60: PASS
P11 Appendix A: b_r = r-th difference of E*_2n: explicit formula (r <= 40), v_2(b_r) >= 2r - floor(log2(2r+1)), beta_1 = -2, beta_2 = 4, v_2(beta_r) >= 2 (r <= 500): PASS ; v_2(b_r), r = 0..16: [0, 1, 3, 4, 7, 8, 10, 11, 15, 16, 18, 19, 22, 23, 25, 26, 31]

18 checks, 0 failures; total time 20.7 s
ALL CHECKS PASS
real 20.76
user 20.45
sys 0.14
