A. Constants of Lemma 3.1 and Theorem A
[ok] A1 (1+1/(2d))^d <= 2 for 1 <= d <= 300
[ok] A2 (3+1/d)^d <= 4^d for 1 <= d <= 300
[ok] A3 enlargement: prod(s_k+2rho)-prod(s_k) <= (1+2rho)^d-1 <= 4 d rho  (2 d rho <= 1/2)  (d<=40 x 26 values of rho; 3000 random boxes)
[ok] A4 tails: sum_{i>=N}(c_d 2^-ceil(i/2) + 2^-i) <= eps_N, sum_{i>=n} 2^-floor(i/2) <= tau_n  (closed forms checked exactly, N <= 200, d <= 8)
[ok] A5 identity 2^-i / lambda_i = 2^-ceil(i/2) with lambda_i = 2^-floor(i/2)
B. Lemma 3.1 for d = 1 (random polynomials; exact rational arithmetic)
[ok] B1 Lemma 3.1 (P1)-(P4),(i),(ii) for d = 1  (40 polynomials of degree <= 4, m <= 5, 22533 boxes in V2 in all, 3721 grid points outside V, each with all grid intervals containing it; largest mu(V)/(||g||_1/lam) = 2.745 against c_1 = 18)
C. Finite Vitali step (P4), d = 2, 3
[ok] C1 d = 2: containment in R*, mu(R*) <= (3+1/d)^d mu(R) <= 4^d mu(R), union bound  (300 random families)
[ok] C2 d = 3: containment in R*, mu(R*) <= (3+1/d)^d mu(R) <= 4^d mu(R), union bound  (120 random families)
D. Descent of Lemma 4.3 (exact measures of finite unions)
[ok] D1 d = 1: invariant psi(C_j) >= beta_j and final box outside the open boxes  (60 random families, 30 steps)
[ok] D2 d = 2: invariant psi(C_j) >= beta_j and final box outside the open boxes  (25 random families, 10 steps)
E. The open set of Lemma 5.3 (finite levels)
[ok] E1 E prefix-free, sum_E 2^-|tau| = 1-|T' cap 2^n|/2^n <= 1-|T cap 2^n|/2^n, (i), (ii)  (150 random trees of height <= 10; (ii) also for E built from T)
F. Constants and counts of Lemma 5.4
[ok] F1 2^-J-1 + 1/(1+2^(J+2)) < 2^-J and M delta^2 = 2^(J+2), J <= 400
[ok] F2 J = 2 (M = 4096): int_{-1}^{1} (1-u^2)^M du < 2 delta + (1-delta^2)^M < 1/4  (exact values 0.027692 and 0.125000)
[ok] F3 (n+2) 4^-(n+2) <= 2^-n for n <= 3000
[ok] F4 (1-v)^M <= 1/(1+Mv), (1+v)^M >= 1+Mv, (1-s^2)^M >= 1-Ms^2 on a grid, M <= 30
[ok] F5 #{j >= 1 : M(k,j) s^2 <= 1/2} = max(0, floor((2t-7)/6) - k) for s = 2^-t (unbounded in t)
[ok] F6 p_(n+1) - p_n has exactly n+2 terms (n = 10)
G. Dyadic boxes D_sigma of Lemma 5.1
[ok] G1 mu(D_sigma) = 2^-|sigma| and sup-diameter 2^-floor(|sigma|/d), d <= 3, |sigma| <= 9
H. Iterated covers of Lemma 4.6
[ok] H1 i-fold concatenations of a prefix-free E are prefix-free with weight q^i (i <= 3)
I. Trapezoid functions of Corollary 4.5
[ok] I1 integral of a product of trapezoids >= mu(B) - 2 d theta  (random boxes, d <= 4)

20 of 20 checks passed
ALL CHECKS PASSED
