CCC forcing cannot create diamond (source code)

= CCC forcing cannot create diamond
{c}
{title2=$M[G]\models\Diamond\ \Longrightarrow\ M\models\Diamond$}

For each index, collect the ground <subsets> which some condition forces to be the corresponding diamond guess. Distinct forced values have incompatible witnessing conditions, so the <countable chain condition for forcing> makes this a countable family. Every ground <subset> is guessed by these families on a ground stationary set, by testing each ground <club set>. The <countable-family diamond equivalence> then yields diamond in the ground model. A generic guess need not itself be a ground <subset>; only values forced equal to one are collected.