PASS brute-force Entringer numbers = recurrence (5), n<=9
PASS rows 1..6 printed in the paper
PASS valuation triangle rows 1..5 = Ramassamy Fig. 2
PASS D_1 valuations start 0,inf,0,inf,0 (column reading)
PASS E_0..E_12 = 1,1,1,2,5,16,61,272,1385,7936,50521,353792,2702765
PASS Lemma 2.2: v2(T_{2j-1}) = 2j-2-v2(j) for j<=500 : []
PASS Theorem 2.4 (Stern): v2(E*_2m - E*_2n) = 1 + v2(m-n) for 0<=n<m<=500 (125250 pairs) : []
PASS Corollary 2.5(a): S_2m = 1 mod 4 for m<500
PASS Corollary 2.5(b),(c) for 2<=k<=9 (all m in range)
PASS unsigned S: S_2 = S_0 (Stern fails without signs)
[E_n and Stern done at 12.1s]
triangle built: 3000 rows, 4501499 entries with 2<=n<=3000, B=6128 bits, 21.5s
PASS Lemma 3.1 (lower bound v2(e_{n,i}) >= H(i,n)) on 4501499 entries, 2<=n<=3000 : []
PASS Lemma 3.2 (witness v2(e_{2j*,i}) = G(i)) for 2998 columns i>=3 with 2j*<=3000 : []
PASS Theorem 1.1: finite column minima = G(i) for all i<=3000 (every witness row <= 3000) : []
PASS m_{2t-1} = m_{2t} and monotone, i<=3000
PASS u_k (from triangle) = 2J(k) for k<=2996 : []
PASS every entry of D_4 has valuation 1 (rows 4..3000)
PASS e_{5,3}=4, e_{7,3}=56
PASS Remark 6.1 formulas e_{2J-1,1..3}, e_{2J,1..4}, e_{2J+1,4} for rows <= 1000
PASS Table 1 row h(j), j<=20
PASS Table 1 row m_{2j-1}=m_{2j} (triangle data), j<=20
PASS Table 1 rows u_k, k<=40 (triangle data and 2J(k))
PASS Ramassamy Table 1 (u_1..u_18)
PASS Lemma 5.1 (S1),(S2),(R1),(R2) for 2<=a<=20; (R3) for j<=2^(a+2), a<=16
PASS f(2,4,4,4) = (2,4,4,4,8,8,8,8)
PASS f(2,4,4,4,8,8,8,8) = (...,10,12,12,16,16,16,16,16)
PASS f-transform of (2,4,4,4) = 2J(k) for k <= 2^22
PASS index ell = 2^a-a-1 at every step a=2..21
PASS 2J(k) (scan) = 2J(k) (direct) for k<=5000
PASS Lemma 5.2 (a),(b) for 2<=a<22
OEIS reading, n=0..5: last diagonal with valuation exactly n: [2, 4, 3, 3, 8, 7] ; with valuation <= n: [2, 4, 4, 4, 8, 8] ; 2max{j:h(j)<=n}: [2, 4, 4, 4, 8, 8]
PASS Remark 6.1: 'exactly n' gives 3 for n=2,3 and 'at most n' gives u_{n+1}
done in 63.4s; failures: 0 []
