Size bound for finite-support ccc iterations

Inductively build a coded order $P_{\alpha }^{\ast }$ of size at most $\mu$ with a dense embedding into $P_{\alpha }$, coherent under restriction. At a successor, the forcing hypothesis and AC give a $P_{\alpha }$-name ${\dot{e}}_{\alpha }$ forced to be a surjection from $\check{\mu }$ onto ${\dot{Q}}_{\alpha }$ (allow repetitions). The local names ${\dot{e}}_{\alpha }(\check{\xi })$ need not belong to the prescribed second-name carrier $R_{\alpha }$. For every $\xi <\mu$, use the AC/maximal-antichain mixing clause of the two-step convention underlying F1 to choose ${\rho }_{\alpha \xi }\in R_{\alpha }$ with $1_{P_{\alpha }}⊩{\rho }_{\alpha \xi }={\dot{e}}_{\alpha }(\check{\xi })$. AC selects these representatives simultaneously; retain only these at most $\mu$ carrier names as coded second coordinates. Given a raw $(p,\dot{q})$, first strengthen its prefix to a coded condition and then choose a stronger coded prefix forcing $\dot{q}={\rho }_{\alpha \xi }$ for some ground $\xi <\mu$, using the forced surjectivity and density of ordinal decisions. The pair with second coordinate ${\rho }_{\alpha \xi }$ is then a legal restricted-iteration condition below the raw pair. The coded successor has at most $\mu \cdot \mu =\mu$ conditions by F3. No arbitrary value name is silently used as an $R_{\alpha }$-coordinate.

At a limit, every raw condition is forcing-equivalent to the one obtained by replacing each off-support coordinate by its distinguished literal top name: the original prefix forces equality to top there, and induction on coordinates preserves the iteration order in both directions. Its remaining support is finite. Strengthen those finitely many coordinates successively to the coded carrier representatives from step 1.1, and pad every other coordinate with the distinguished top names. A finite support is chosen from an ordinal of size at most $\mu$, and each coordinate from one of at most $\mu$ earlier codes; F3 bounds the set of finite coded tuples by $\mu$.

Successor evaluation and the limit union maps are dense embeddings, so the coded iteration is forcing-equivalent stage by stage and coherent under restriction. AC is used to choose the forced enumerations and dense-embedding representatives. Raw presentations may contain arbitrarily many forced-equal names, which is why only a dense presentation, not their literal size, is bounded.