3-bit lemma (k = 5): all 256 f (39 distinct polynomials) satisfy sum_i Delta_i^2 <= 20(1-q)^8 on [q6, q5] (exact Sturm); equality identically: 0 f, at q5 only: 0 f: OK
4-bit lemma (k = 5): all 65536 f (1630 distinct polynomials) satisfy sum_i Delta_i^2 <= 20(1-q)^8 on [q6, q5] (exact Sturm); equality identically: 0 f, at q5 only: 2 f (+-OR_4): OK
