Parity lifts and bounded-treewidth witnesses for Weisfeiler–Leman equivalence

For k ≥ 4, we construct two uncolored graphs that are k-dimensional Weisfeiler–Leman equivalent exactly when a prescribed finite-domain choice system has no compatible choice. The system has $k+1$ domains for joint refinement and k for separate-coordinate refinement. A successful choice is detected after two joint rounds or one separate round. Applied to sparse satisfiability, the reduction gives fixed-dimension $n^{\Omega (k)}$ time exclusions under positive-rate ETH, even for deciding equality of these early histograms.