Solution (source code)

= Solution

The infinite <Ramsey theorem> used here says that every finite colouring of the $m$-element subsets of an infinite subset of $\mathbb N$ has an infinite homogeneous subset. Let $(x_n)$ be normalized with <basis constant> $K$.

For each positive integer $m$, rational scalar tuple $a=(a_1,\ldots,a_m)$ and precision $2^{-r}$, colour increasing $m$-tuples according to intervals of length $2^{-r}$ containing $\|\sum_i a_ix_{n_i}\|$. This is a finite colouring, because all these norms lie between zero and $\sum_i|a_i|$. Enumerate the countably many triples $(m,a,r)$ and repeatedly apply the <Ramsey theorem>, obtaining decreasing infinite sets on which each specified norm has oscillation at most $2^{-r}$. Choose a diagonal subsequence $(y_j)$ whose tail is contained in every previously selected infinite set.

Consequently, for every rational tuple $a$, the net of norms over increasing tuples from $(y_j)$ is Cauchy as its first index tends to infinity. Denote its limit by $N(a)$. This extends to arbitrary scalar tuples because
$$
\left|\left\|\sum a_iy_{j_i}\right\|-\left\|\sum b_iy_{j_i}\right\|\right|\leq\sum_i|a_i-b_i|,
$$
uniformly in the indices. For complex scalars use rational real and imaginary parts. The same estimate proves convergence uniformly over all sufficiently late increasing tuples for each fixed scalar tuple.

Homogeneity and the <triangle inequality> pass to the limit. The coordinate functionals of a normalized basic sequence have norm at most $2K$, since the coordinate projection is the difference of two initial projections. Thus
$$
N(a)\geq\frac1{2K}\max_i|a_i|,
$$
so $N$ is a genuine norm. Zero coefficients may be inserted anywhere without changing the value: removing those coordinates simply selects another increasing tuple for the same limiting combination. Also every initial-segment projection has norm at most $K$, by the corresponding inequality for $(y_j)$. Completing the finitely supported scalar sequences in $N$ therefore gives a <Banach space> with a normalized <basic sequence> $(e_i)$.

Its finite norms are invariant under increasing relabellings, by the zero-insertion observation, and
$$
\boxed{\left\|\sum_{i=1}^m a_ie_i\right\|=\lim_{j_1\to\infty}\left\|\sum_{i=1}^m a_iy_{j_i}\right\|,\qquad j_1<\cdots<j_m.}
$$
This is the required <spreading model>, generated by the diagonal subsequence.