How to reduce constrained proofs to 0-1 IP
If your problem is truly in NP, the reduction follows immediately from the Cook-Levin theorem.  You described how to build a verifier for your problem.  The proof of the Cook-Levin theorem shows how to turn that into a 3SAT instance.  Basically, the variables of the 3SAT formulas are the intermediate states of the verifier, and the formula itself says that each pair of consecutive states are consistent and that the verifier ends up accepting.

I am not persuaded by your proof that it is in NP.  Your proof would be fine if $Y$ is provided on the input in unary, but not if it is provided in binary -- in the latter case, the length of the proof is exponential in the size of the input, so your proposed verifier doesn't run in polynomial time.  If the problem is not in NP, there is no (polynomial-time)  reduction to 3SAT.