Finite support iterations of $\sigma$-centered forcing notions

If anyone else had asked this question, I'd start by looking in "Tools for your forcing construction," but I suppose that won't help in the present situation. So, let me attempt a proof with the idea you suggested, and see where I get stuck. Suppose the iteration has length $\lambda<\mathfrak c^+$, the iterands are $Q_\alpha$ (which should have a dot above or a tilde below, but I'm too lazy for that), and $P_\beta$ is the iteration for the first $\beta$ steps (so $\alpha<\lambda$ and $\beta\leq\lambda$). Furthermore, fix a map $F:\lambda\times\omega\to\omega$ such that, for every finitely many pairs $(\alpha,n)\in\lambda\times\omega$ with distinct first components, there exists $k$ such that $F(\alpha,k)=n$ for each of the given finitely many pairs, i.e., the functions $F(\alpha,-):\omega\to\omega$ constitute an independent family. (This, of course, is where I need that $\lambda<\mathfrak c^+$.) The assumption that we're iterating $\sigma$-centered notions of forcing means that we can fix a sequence $(C_\alpha:\alpha<\lambda)$ such that, for each $\alpha$, $C_\alpha$ is a $P_\alpha$-name forced, by every condition in $P_\alpha$, to denote a function on $\omega$ whose values are centered subsets of $Q_\alpha$ that together cover $Q_\alpha$. I'll also assume that (all conditions force that) each $C_\alpha(n)$ is closed upward, i.e., under weakening the conditions; in particular, each $C_\alpha(n)$ contains the trivial condition 1 of $Q_\alpha$. Now, with the notation in place, it's time to start doing some work.

Given any condition $p\in P_\lambda$, I want to extend it to some $p'$ such that, for each $\alpha$ in the support of $p'$, the earlier part of $p'$, namely $p'\upharpoonright\alpha$, decides a particular $n$ such that the centered set $C_\alpha(n)$ contains $p'(\alpha)$. (Of course this will also be true, automatically, when $\alpha$ is not in the support of $p'$, because 1 is in every $C_\alpha(n)$.) Call such conditions $p'$ "fine". If I can produce a fine extension $p'$ for each $p$, then I can finish the proof as follows. For each $k\in\omega$, let $D(k)$ consist of those conditions $p'$ such that, for all $\alpha<\lambda$, $p'\upharpoonright\alpha$ forces $p'(\alpha)\in C_\alpha(F(\alpha,k))$. (Note that, although the requirement refers to all $\alpha<\lambda$, for any particular $p'$ only the $\alpha$'s in its support are relevant.) Each of the countably many sets $D(k)$ is easily seen to be centered: Given finitely many conditions from the same $D(k)$, obtain a common extension by defining its components inductively; the only work occurs at the ordinals $\alpha$ that are in the supports of the given conditions, and for such an $\alpha$ the (forced) centeredness of $C_\alpha(F(\alpha,k))$ and the maximum principle give what you need. Furthermore, thanks to the independence of the functions $F(\alpha,-)$, any fine $p'$ is in some $D(k)$; just use independence to get the right values for $F(\alpha,k)$ for each $\alpha$ in the support of $p'$. Therefore, if the fine conditions $p'$ are dense, then the upward closures of the $D(k)$'s witness that $P_\lambda$ is $\sigma$-centered.

So it remains to extend an arbitrary $p\in P_\lambda$ to a fine $p'$. I'll proceed by induction on the maximum element of the support of $p$. (If $p$ has empty support, this makes no sense, but then $p$ is the trivial condition, which is already fine.) Furthermore, I'll strengthen the induction hypothesis to say that a fine extension can be obtained without increasing the maximum element of the support. (It may be necessary to add new elements to the support, but they can be taken to be smaller than some already existing elements of the support.) So suppose the maximum element of the support of $p$ is $\alpha$, and the result is known for conditions whose support is a subset of $\alpha$. Since the sets $C_\alpha(n)$ (are forced by all conditions in $P_\alpha$ to) cover $Q_\alpha$, we can extend $p\upharpoonright\alpha$ to some $q\in P_\alpha$ forcing $p(\alpha)$ to lie in a particular $C_\alpha(n)$ (with an actual number $n$, not a forcing name). Now apply the induction hypothesis to $q$, extending it to a fine condition $q'$ with support lying below $\alpha$. Then $q'$ together with $p(\alpha)$ gives the required $p'$.

I just wanted to point out how Andreas' proof above relates to the separability of products of $2^{\aleph_0}$ separable spaces:

Let $\lambda<(2^{\aleph_0})^+$. Suppose $\langle X_\alpha:\alpha<\lambda\rangle$ is a family of separable spaces. For each $\alpha<\lambda$ let $\langle x_\alpha^n:n\in\omega\rangle$ enumerate a dense subset of $X_\alpha$. Let $F:\lambda\times\omega\to\omega$ be as in Andreas' proof. Now the set of sequences of the form $\langle x_{\alpha}^{F(\alpha,n)}:{\alpha<\lambda}\rangle$, $n\in\omega$, is dense in $\prod_{\alpha<\lambda}X_\alpha$.

Also note that $\sigma$-centeredness of a forcing notion $\mathbb P$ corresponds to the separability of the Stone space of the completion of $\mathbb P$. However, I don't know whether it is possible to deduce the $\sigma$-centeredness of short finite support iterations of $\sigma$-centered forcing notions directly from the separability of small product of separable spaces.