Compile polynomial-space machine reachability into a quantified circuit, then use the verified Cook–Levin gate clauses and quantifier normalization. The checked Byskov game gadgets transfer the resulting alternating-CNF game to positive CNF. Both word transformations have compiled polynomial- time Turing-machine witnesses; their composition uses the archived polynomial-time composition proof.