The source builds Sipser's instance $sipserPCP M w$ over the alphabet $Sym$ of configurations, proves that its matches are exactly the accepting computation histories ($PCP.hasMatch_sipserPCP_iff$, through the modified problem and the $⋆$ trick, $PCP/SRtoMPCP.lean$ and $PCP/StarTrick.lean$), and that the construction is primitive recursive ($PCP/Computable.lean$); $PCP.computablyDecidable_acceptance_of_pcp$ is the reduction. The concept states both problems over $ℕ$: the bridge moves the given decision procedure from $ℕ$ to $Sym$ along the injective encoding of $Sym$, which preserves and reflects matches ($computablyDecidable_hasMatch_sym$), and the resulting procedure for the source's machines to the concept's ($computablePred_accepts_iff$).

Sipser, Theorem 5.15 (Section 5.2); Lean proof by Aristotle ($RequestProject/PCP/$).