Compile unary header checks, clause normalization, and adjacency-matrix generation into a finite stack program with a polynomial step bound. The archived compiler supplies the Turing-machine witness. The separately proved word-level correctness theorem handles every binary input.