Normalize each fixed-width formula with at most O_k(n^k) possible clauses. Per node, enumerate each clause's at most 2^k literal subsets to select the branch and normalize its children in polynomial time for fixed k. Traverse the sparsification tree depth first: keep a polynomial-depth path and count one leaf at a time, not the whole tree. With sigma=1/s and s<=sqrt(ceil(log2 n)), the path, formulas and one sparse-counter workspace use polynomial space. Disjointness keeps the running sum between zero and 2^n, requiring at most n+1 bits. A polynomial-space bound does not make the exponentially many sequential leaf operations disappear.