Disjoint-variable factorization uses each predicate's own block
On this page · Permalink · Source line 654
Suppose \(A\) depends on witness variables in block \(S\) and \(B\) on a disjoint block \(T\). Write \(\tau_{z_S}(A)=\sum_s A(s)z_S^s\) for the weighted trace on \(S\), distinct from the unweighted top-coefficient notation \(\tau_w\). Weighted sum over the union factors as
Each factor is traced on its own variable block. The union trace is then their product. This is an ordinary factorization of a finite double sum.
For \(A=w_1\) and \(B=w_2\),
Tracing both factors over the full two-bit ambient domain introduces unused variable sums:
Their product generally differs from the union trace. At \(z_1=z_2=1\), each full ambient factor is zero, while the trace of \(AB\) is one. Disjoint dependence alone does not justify multiplying traces with mismatched domains.
The source checker tests all four one-bit predicates per block and every pair of GF(16) weights: \(4\cdot4\cdot16^2=4,096\) own-block factorization cases. It does not claim an ambient-domain product identity.
General written factorization under the own-block convention; exact finite source check and an explicit ambient-domain counterexample.