The first Feferman–Levy collapse layers

From F1, $H_0=\mathcal{G}$, $H_1$ fixes forcing layer $0$, and $H_2$ fixes layers $0$ and $1$. Thus F2 says that $R_0$ uses no generic collapse layer, $R_1$ may use only layer $0$, and $R_2$ may use only layers $0$ and $1$. More explicitly, the fixed-value theorem built into F2 identifies their Boolean coefficients with the complete algebras of $P\upharpoonright 0$, $P\upharpoonright 1$, and $P\upharpoonright 2$, respectively.

Instantiating F3 and F4 gives the three concrete composites $g_0=e_0\circ f_1:\omega \twoheadrightarrow R_0,g_1=e_1\circ f_2:\omega \twoheadrightarrow R_1,g_2=e_2\circ f_3:\omega \twoheadrightarrow R_2\mathrm{.}$ Here $e_m$ codes the initial-layer Boolean names, while the next unused canonical collapse $f_{m+1}$ makes its ordinal domain countable in $N$; F5 verifies this composition in general. This is a finite list of specified maps, so forming the triple $(g_0,g_1,g_2)$ requires no Choice.

F6 says every real lies in some later $R_m$. Suppose, however, that $N$ contained a sequence $⟨h_m:m<\omega ⟩$ with each $h_m:\omega \twoheadrightarrow R_m$. Then $q(m,k)=h_m(k)$ maps $\omega \times \omega$ onto ${\bigcup }_m{R}_m={\mathbb{R}}^N$; repeated or equal layers do not affect surjectivity. Composing with the explicit Cantor pairing bijection between $\omega$ and $\omega \times \omega$ would make the reals countable, contradicting F7. Therefore the individual maps illustrated in step 2.1 cannot be assembled for all layers inside $N$. The obstruction is precisely simultaneous countable choice, not failure of any fixed layer enumeration.