Random-coordinate pullback extends every fair-coin product measure

The discrete two-point space is standard Borel: its discrete metric is complete and its finite underlying set is a countable dense set. On a finite coordinate set $F$, assign mass $2^{-\mathrm{\mid }F\mathrm{\mid }}$ to each point of $2^F$. Summing over the coordinates removed by a restriction verifies consistency, including the empty coordinate set with its one point. F7 therefore supplies the ground product probability, and F6 supplies its probability algebra. The same construction is available for every coordinate ordinal inside $W$, since ZFC in $W$ is an explicit premise.

Every ground cylinder-measurable set $C\subseteq 2^{\kappa }$ has a countable support in the stronger form $C={\pi }_S^{-1}(C_S)$ for a countable $S\subseteq \kappa$ and a cylinder-measurable $C_S\subseteq 2^S$. Indeed the class of sets with this property contains all finite cylinders and is closed under complement. Given a sequence of such sets, use F9 to choose their supports and bases; the union $S$ of their countable supports is countable under AC. Each restriction map from $2^S$ to a coordinate subproduct is measurable, since inverse images of finite cylinders are finite cylinders, and inverse images preserve complement and countable union. Pulling the bases back to $2^S$ and taking their countable union proves the union closure. Generated-sigma minimality proves the assertion. This concerns ${\mathrm{\Sigma }}_{\kappa }$, and hence suffices for a representative of every Boolean condition.

For each $\xi <\kappa$, let $b_{\xi }$ be the class of the event whose $\xi$-bit is one. F5 decides exactly one of $b_{\xi },\mathrm{\neg }{b}_{\xi }$; define $g(\xi )=1$ exactly when $b_{\xi }\in G$. This is a function in $W$: the ground Boolean name $\{⟨\check{\xi },b_{\xi }⟩:\xi <\kappa \}$ evaluates to its one-set, and ZFC in $W$ forms the characteristic-function graph. Check-name evaluation and the vector-name construction are included in F2. No choice of a representative generic point of the ground probability space is required.

Fix a finite partial function $q:D\to 2$ with $D\cap S=\mathrm{\varnothing }$. For every cylinder-measurable $A\subseteq 2^S$ one has ${\mu }_{\kappa }({\pi }_S^{-1}(A)\cap [q])=2^{-\mathrm{\mid }D\mathrm{\mid }}{\mu }_S(A)$. To prove it, the left side as a function of $A$ is a finite measure: inverse images preserve disjoint countable unions and intersecting with the fixed measurable cylinder does also. The right side is a finite measure. Their total masses are both $2^{-\mathrm{\mid }D\mathrm{\mid }}$. On a finite cylinder in $2^S$, the identity is the finite uniform marginal calculation of step 1.1, using disjointness of $D$ and $S$. Finite cylinders together with the empty set form a generating pi-system, so F8 proves the identity. The identical uniqueness argument without $[q]$ gives ${\mu }_{\kappa }({\pi }_S^{-1}(A))={\mu }_S(A)$. Thus ${\mu }_{\kappa }(C\cap [q])=2^{-\mathrm{\mid }D\mathrm{\mid }}{\mu }_{\kappa }(C)$ for every condition representative supported on $S$.

Fix a cardinal $\lambda$ in $W$. Cardinal preservation makes $\lambda$ a ground cardinal. Put $\rho =\max (\lambda ,\kappa )$ in $M$, and take the ground $I,U,(f_{\alpha }{)}_{\alpha <\rho }$ from F1. F2 applies because $M$ satisfies the continuum bound in the statement; write $\eta$ for its measure on $\mathcal{P}(I{)}^W$. In $W$ define $\varphi (i)(\alpha )=g(f_{\alpha }(i))$ for $i\in I,\alpha <\lambda$. Replacement forms $\varphi :I\to (2^{\lambda }{)}^W$. Define $\gamma (Y)=\eta ({\varphi }^{-1}(Y))$ for every $Y\in \mathcal{P}((2^{\lambda }{)}^W{)}^W$. Power Set, Separation and Replacement in the assumed ZFC model $W$ form this whole function. Inverse images preserve empty sets, whole spaces, unions and intersections, so F2 gives total mass one, countable additivity, and null closure for every extension family indexed by a ground ordinal below $\kappa$. Cardinal preservation and unchanged ordinals make these exactly the required bounds in $W$.

Let $p:F\to 2$ be a finite coordinate prescription on $\lambda$, and put $n=\mathrm{\mid }F\mathrm{\mid }$. Every such finite ordinal/bit datum belongs to $M$, by transitivity and closure under finite set constructions. For $i\in I$ let $a_i$ be the Boolean meet of $b_{f_{\alpha }(i)}$ when $p(\alpha )=1$ and their complements when $p(\alpha )=0$, over $\alpha \in F$. This is one ground vector in ${\mathbb{B}}^I$. F5 identifies its represented subset $A(a)=\{i:a_i\in G\}$ exactly with ${\varphi }^{-1}([p{]}^W)$. Fix any $c\in \mathbb{B}$ and a measurable representative $C$ supported on a countable ground $S$ from step 2.1. Since $\mathrm{\mid }S\mathrm{\mid }<\kappa$, F1 gives a $U$-member on which the finitely many coordinates $f_{\alpha }(i)$ are distinct and outside $S$. At every such $i$, the vector element $a_i$ is the class of a consistent cylinder on exactly $n$ coordinates disjoint from $S$. Step 3.1 gives $m(c\wedge a_i)=2^{-n}m(c)$.

The defining large-fibre rule in F3 now gives ${\nu }_a(c)=2^{-n}m(c)$ for every $c$, including zero. The constant density $2^{-n}$ has exactly these integrals, so almost-everywhere uniqueness in F3 identifies it with $h_a$. F4 evaluates it to $2^{-n}$ in $W$, whence $\gamma ([p{]}^W)=2^{-n}$. For $F=\mathrm{\varnothing }$ the vector is constantly one and this also gives total mass one; incompatible simultaneous bit prescriptions instead give the empty cylinder and zero.

In $W$, the restriction of $\gamma$ to the cylinder sigma-algebra and the standard product probability from step 1.1 are finite measures agreeing on all finite cylinders and on the whole space. F8 makes them equal on that sigma-algebra. Step 3.2 already supplies $\gamma$ on its full extension power set, with the required null closure. If the additional continuum equality holds, any family of fewer than continuum many null sets in $W$ can be indexed, using AC there, by an ordinal below $\kappa$; its union is null by that closure. This proves the final PMEA assertion under all the stated premises, without inferring any of those forcing-preservation premises from genericity alone.