For positive integers n,m,B with m<=Bn, let mu=floor(log2 m)+1, P=20000B^2 mu^2, and D0=320000B^2 mu^3. The initial-check construction promises at most 3n binary rows on m coordinates, each with at most D0 nonzero entries. Its nonzero kernel vectors have weight at least m/P. Construction time is exp(poly(B,log(m+2))), with poly(n,m,B) space. These large constants are theoretical bounds, not an efficient implementation claim. When m/P<=1 the weight guarantee alone says nothing beyond nonzero weight; it is still sufficient for the later probability calculation. Empty formulas are handled before invoking this positive-m contract.