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