Solution (source code)

= Solution

For each $\xi<\kappa$, choose a maximal <antichain in a forcing order> below $p$ deciding a witness $\eta>\xi$ in $\dot C$. Write the decided values as $\eta_{\xi,q}$, one for each condition $q$ in that antichain. The $\kappa$-<chain condition for forcing> gives fewer than $\kappa$ possible values. Since $\kappa$ is regular in $M$, choose
$$
g(\xi)=\sup\{\eta_{\xi,q}+1:q\text{ is in the chosen antichain}\}<\kappa.
$$
The <possible-values lemma for chain-condition forcing> ensures
$$
p\Vdash\exists\eta\in\dot C\ (\xi<\eta<g(\xi)).
$$
In $M$ take the <club set> of limit closure points
$$
\boxed{D=\{\delta<\kappa:\delta\text{ is limit and }
\forall\xi<\delta\ g(\xi)<\delta\}.}
$$
It is unbounded by repeatedly closing any starting ordinal under $g$ for countably many steps, and closed by taking increasing limits. For $\delta\in D$, the forced displayed property gives points of $\dot C$ arbitrarily high below $\delta$. Its forced closedness yields $\delta\in\dot C$. Therefore
$$
\boxed{D\in M\text{ is club},\qquad p\Vdash\check D\subseteq\dot C.}
$$
This proves the <ground-model club containment lemma>. The name on the right is $\dot C$, as printed in the PDF.