I agree...I think a real "proof by construction that the language is [Turing] complete" would just be an interpreter for Turing machine programs written in Lisp

I agree...I think a real "proof by construction that the language is [Turing] complete" would just be an interpreter for Turing machine programs written in Lisp, which is pretty boring.