Fix integer beta>=1. After any constant-one padding, let n<=M<=bn, let each factor scope have size at most w, and let each variable belong to at most b scopes. Require b,w<=ceil(log2 n)^beta. For sufficiently large such inputs, the schedule and tail arguments provide a valid polynomial-size layout. For explicit integer polynomial factors evaluated over the rationals, also require total degree O(n) and polynomially bounded factor descriptions and evaluation cost. The fixed-denominator, accumulator and interpolation arguments then justify polynomial bit overhead and streaming space, giving the stated subexponential-time bound. Failed parameter checks use the separate fallback. This does not establish that arbitrary SAT instances meet these hypotheses; sparse-equation lifting, reductions, sparsification and the global ETH claim remain separate obligations.