The source proves it from the domino form over $Sym$ ($Acceptance.hasMatch_not_computablyDecidable$), passing between dominos and indices ($PCPIndex.solvable_iff_hasMatch$) and along the primitive recursive injection of $Sym$ into $ℕ$ ($PCPIndex.solvable_mapInst_iff$, $PCPIndex.primrec_mapInst$); the concept's $Solvable$ is the source's.

Lean proof by Aristotle ($RequestProject/PCP/Index.lean$); the index form is the one the book Transducers consumes.