Solution (source code)

= Solution

The <canonical forcing name> $\dot a=\check a$ is defined recursively by
$$
\boxed{\check a=\{(\check b,p):b\in a,\ p\in P\}.}
$$
If a weakest condition $1_P$ is provided, one may instead pair each $\check b$ only with $1_P$. The all-conditions version works for an arbitrary nonempty <forcing> without that extra convention. Induction on rank gives $\check a^G=a$ for every <generic filter>, since each element $b\in a$ is activated by some condition of the nonempty $G$. Thus all ground-model objects have canonical names.