1200 (word, x) checks: sum x^t 2^dL <= (1+2x)^M always; max ratio 1.000000
lw's sum C(L,t)8^t / exact weighted count: min ratio 1.000 (>=1, as his lemma needs)
all-beta=2, L=12, x=1/2: lhs/rhs = 1.0
