brute force n<=10 matches: True
v2(E_{2j-1}) == h(j) for 2j-1<=N: True
lemma failures: []
m_i (rows<=3000) == G(i) for i<=2960: True []
m_i weakly increasing i<=I: True
u_k (definition, truncated) == 2*max{j:h(j)<k} for k<=2920: True
Table 1: True
count version == max version: True
f-transform == closed form for k<=2^22: True
f-transform prefix == u_k (triangle) for k<=Kmax: True
ALL PASS
