Ah, sorry; deleted my previous comment because I was misunderstanding the notation. To prove that $C_{\infty}$ has the desired universal property, it suffices to show that $t$ acts invertibly on it. The "obvious" attempt to prove this will work if the braiding automorphism of $1 \otimes 1$ is (homotopic to) the identity. But since you are free to trade $t$ to $t^n$, it's also true if the braiding automorphism is (homotopic to) the identity on $1^{\otimes n} \otimes 1^{\otimes n}$.

This is why (for example) the plus construction appears in the definition of algebraic K-theory but not in the definition of topological K-theory. Permutation matrices are not equal to the identity, but they belong to the identity component of $\mathrm{GL}_n(\mathbf{C})$ (and to the identity component of $\mathrm{GL}_n(\mathbf{R})$ in the case of even permutations).

The corollary is correct but the proof given doesn't actually show it (the formula $K(S) = S[t^{-1}]$ is false in general, for example it is false when $S = \coprod_{n} B\Sigma_n$ is the free $E_{\infty}$-space on one generator). You need some additional input to draw the conclusion: for example, you can use the group completion theorem and the fact that the components of $S$ are nilpotent spaces, or you could argue abstractly that $K(S) = S[t^{-1}]$ using that the braiding of $1^{\otimes 2}$ with itself is the identity as an automorphism of $1^{\otimes 4}$.

Without loss of generality $\mathcal{C} = Pic(\mathcal{C})$ is the $0$th space of a connective spectrum $X$. You're asking if every map from the sphere spectrum into $X$ factors through the $1$-truncation of the sphere spectrum. No; for example, the identity map from the sphere spectrum to itself does not admit such a factorization.

The functor definitely doesn't preserve infinite coproducts. But the axioms of ZFC do not involve infinite disjunctions...

It is an isomorphism. Abstract proof: since $i_* i^*$ is a left exact functor, the map $i_* i^*( \mathscr{F} ) \coprod i_* i^*(\mathscr{G} ) \rightarrow i_* i^* (\mathscr{F} \coprod \mathscr{G} )$ is automatically a monomorphism. The epimorphism statement is the one you have to worry about (and is the content of that Lemma in Moerdijk-MacLane). Concretely: the operation $V \mapsto \overline{V}$ and $\overline{V} \mapsto U \cap \overline{V}$ define mutually inverse bijections from clopen subsets of $U$ to clopen subsets of $\overline{U}$, because extremally disconnected spaces are bizarre.

Open and closed subsets of $U$ are the same as open and closed subsets of the closure of $U$, since $S$ is extremally disconnected. Alternatively, you can compute the stalk at $s$ using only clopen neighborhoods. The functor preserves only finite coproducts, not arbitrary ones.

@PeterScholze Ah, I think I see the source of my confusion. There's an operation of "ultrapower by $s \in S$" on models of ZFC, but it doesn't match with the construction of your original post under the (structural set theory $\leftrightarrow$ material set theory) dictionary because it will only "see" those sheaves $\mathscr{F}$ on $S$ which are locally constant on some open set $U$ satisfying $s \in \overline{U}$?

Alternatively: I think what I'm saying is the content of Theorem 15 in the Hamkins and Seabold paper?

@PeterScholze Let $S$ be an extremally disconnected space and let $s$ be a point. For every set $X$, I can take the constant sheaf $\underline{X}$ on $S$, sheafify with respect to the double negation topology, and then take the stalk at the point $s$. I believe that this defines a functor $F: \mathrm{Set} \rightarrow \mathrm{Set}$ that preserves finite limits, coproducts, and epimorphisms, and therefore carries models of any first-order theory (like ZFC + CH) to models of the same theory. The nontrivial ingredient is in Moerdijk and MacLane, Lemma 4 on page 519.

@PeterScholze Isn't it true that the construction of your original post is already an elementary extension of $V$ (with no forcing extension needed)? It's certainly true when $S$ is a Stone-Cech compactification, and I think the proof of Los' theorem shows this too (the essential content is that the direct image functor from the double negation topos to the usual topos of sheaves on $S$ is a map of pretopoi).

@MikeShulman Well, as Peter points out in his original post, a special case is taking ultrapowers of $V$, which is definitely something that set-theorists do. If I understand correctly, you're saying that every ultrafilter gives a model of ZFC? So one can view forcing extensions and ultrapowers as specializations of a more general procedure for making models?

@PeterScholze You absolutely can. That's the "Boolean-valued model" approach, and is better compatible with the perspective that $V$ is the "entire" universe of sets. (If $V$ is already the whole universe, you can't adjoin a new homomorphism $G: B \rightarrow \{0,1\}$ to it: they're all there already. But also no (non-isolated) point of $S$ corresponds to a "generic" filter. In topos language, the double-negation topos is Grothendieck topos with no points.)

@PeterScholze (ctd) There is no overlap between the two, except in the case where $S$ has isolated points (in which case you can take $G$ to "be" an isolated point of $S$, and you will get $V[G] = V$).

@PeterScholze The space $S$ is determined by a Boolean algebra $B$ (in $V$) which "$V$ thinks is complete" (every subset of $B' \subseteq B$ belonging to $V$ has a supremum). The construction $V[G]$ makes sense for any homomorphism of Boolean algebras $G: B \rightarrow \{ 0,1 \}$ belonging the ambient universe. In particular, you can take homomorphisms $G$ which belong to $V$ (this is the construction of your original post). Alternatively, you can take homomorphisms which are "generic" meaning that they preserve suprema of subsets $B' \subseteq B$ which are contained in $V$ (this is forcing).

If V is a model of set theory, then you can do the first part of this construction "in V" to produce some category C that V thinks is a Grothendieck topos. In some ambient universe, C is a Boolean pretopos having an underlying Stone space X. In your example, I think X is Spec(B), where B is the Boolean algebra of clopen subsets of your S? In particular S sits inside X as "the points of the spectrum that V knows about". The usual forcing construction is to take a "stalk" of C at some point of X which is "V-generic": that is, very far from belonging to S.