Composition preserves perfect satisfiability

If $E(G)=\mathrm{\varnothing }$, then $G$ has value one by [F1], while the composition has an empty constraint list by [F7] and therefore $\mathrm{val}(H)=1$ by [F10] and the stated convention. It remains to consider $E(G)\mathrm{\ne }\mathrm{\varnothing }$.

Because $G$ has finitely many vertices and $\mathrm{\Sigma }$ is finite and nonempty, its set of labelings is finite and nonempty, so the maximum in [F1] is attained. Choose $\sigma :V(G)\to \mathrm{\Sigma }$ with ${\mathrm{val}}_{\sigma }(G)=\mathrm{val}(G)=1$. Since the edge set is nonempty, every edge relation is satisfied by its ordered pair of endpoint labels.

For each active vertex $v$, assign its shared block the codeword $B_v=C(\sigma (v))$. By [F2] this is valid and decodes uniquely to $\sigma (v)$. If $e=(v,w)$, then $\sigma$ satisfies its ordered relation, so [F3] says the robust circuit $C_e$ accepts $(B_v,B_w)$. If $e$ is a loop, both pieces are the same block and the satisfied diagonal pair is accepted as well.

For each edge $e$, [F4] supplies the assignment tester on the combined named input list of its two raw pieces. The fixed input $(B_v,B_w)$ is accepted by $C_e$ by step 2.1. Its accepted-input clause in [F5] therefore gives at least one Boolean assignment $b_e$ to the gadget's auxiliary variables satisfying every local constraint. Order that finite variable list as in the explicit tester output and take the lexicographically first such $b_e$. The edge set and each Boolean search space are finite, so this specifies the witnesses without an axiom of choice.

Assign each shared vertex block its fixed codeword and assign each edge-private variable its value from $b_e$. By [F6], the named pieces take the already fixed endpoint blocks, including the same block in both positions of a loop; all other variables are private to their edge. These local labelings agree on every identification, so [F8] combines them into an output labeling $\tau$. Every local constraint accepts under its $b_e$, and [F9] preserves acceptance in every uniform copy. Thus every constraint of $H$ accepts under $\tau$.

Every constraint of $H$ is satisfied by $\tau$, so ${\mathrm{val}}_{\tau }(H)=1$ and ${\mathrm{UNSAT}}_{\tau }(H)=0$ by [F10]. Hence $\mathrm{UNSAT}(H)=0$, and the stated convention gives $\mathrm{val}(H)=1$. Together with the edgeless case, this proves the claim.