7f67dfd
==============================================================================
THE SEPARABLE QUOTIENT PROBLEM
Independence from the usual axioms of set theory
A complete, self-contained proof written to be read from start to finish
==============================================================================

You do not need to know any functional analysis to start. Everything is built
from scratch, in order. Every claim is proved. If you get stuck, the sentence
just before a display tells you why the display is there.

CONTENTS

  Part 0.  The question and the answer
  Part 1.  The evaluation criterion (the test we use everywhere)
  Part 2.  A measurable continuum forces separable quotients (positive side)
  Part 3.  From real to complex scalars
  Part 4.  Building a tricky normed space E
  Part 5.  Infinite paths and weak-Cauchy sequences
  Part 6.  Blocks detected at a prescribed weight
  Part 7.  Separating functionals on every subspace
  Part 8.  Changing the predual: the counterexample
  Part 9.  Set-theoretic models: putting the two sides together


==============================================================================
PART 0.  THE QUESTION AND THE ANSWER
==============================================================================

0.1  Banach spaces, in one paragraph.

A vector space over the real numbers R (or the complex numbers C) is a
collection of objects you can add and scale by numbers, obeying the usual
rules. A norm is a rule ||x|| assigning to each vector x a nonnegative length
with three properties: ||x|| = 0 only for x = 0; ||c x|| = |c| ||x|| for every
scalar c; and ||x + y|| <= ||x|| + ||y||. A Banach space is a vector space
with a norm in which every Cauchy sequence converges. That is the only
setting in this whole document. When we say "space" we always mean a real or
complex Banach space.

A subspace of a Banach space is a linear subspace that is also closed under
taking limits. A quotient X/M is what you get by declaring two vectors equal
when their difference lies in M; it is again a Banach space, and the map
x |-> x + M is a bounded linear surjection onto it.

A Banach space is separable if it contains a countable set that is dense: for
every vector and every epsilon > 0, some member of that countable set is
within epsilon. R, C, and all finite-dimensional spaces are separable.
A typical nonseparable space is the space of all bounded sequences with the
sup norm.

0.2  The problem.

Every infinite-dimensional Banach space contains a separable
infinite-dimensional closed subspace: just take the closed span of a countably
infinite linearly independent set. So separable subspaces are free. The
question is whether the dual statement about quotients is also free.

SEPARABLE QUOTIENT PROBLEM (Banach-Mazur). Does every infinite-dimensional
Banach space admit a bounded linear surjection onto a separable
infinite-dimensional Banach space? Equivalently, does every such space X have
a closed subspace M such that X/M is separable and infinite-dimensional?

The two formulations are equivalent because a surjection T: X -> Y with Y
separable has closed kernel M and induces a bounded bijection X/M -> Y, which
by the open mapping theorem is an isomorphism.

Write SQ_R for the statement "every infinite-dimensional real Banach space has
a separable infinite-dimensional quotient", and SQ_C for the complex version.

0.3  The answer.

THEOREM (main result). Each of SQ_R and SQ_C is independent of ZFC, relative
to the consistency of ZFC together with a measurable cardinal. Concretely, ZFC
proves two implications:

  (i)  If the continuum c = 2^{aleph_0} is real-valued measurable, then SQ_R
       and SQ_C both hold.
  (ii) If the Continuum Hypothesis (CH) holds, then SQ_R and SQ_C both fail.

A measurable cardinal is a very large infinite cardinal whose existence is not
provable in ZFC but is not known to be inconsistent. A real-valued measurable
cardinal is a cardinal kappa carrying a probability measure defined on every
subset of kappa, vanishing on points, and additive over disjoint families
smaller than kappa. Part 9 realizes the hypotheses of (i) and (ii) in suitable
models, which turns the two ZFC implications into the stated independence.

There is also a sharper statement at the smallest interesting size. Let
SQ^{aleph_1}_F mean "every Banach space over F of norm density exactly
aleph_1 has a separable infinite-dimensional quotient". Then:

COROLLARY. If ZFC is consistent, then SQ^{aleph_1}_R and SQ^{aleph_1}_C are
each independent of ZFC. No large-cardinal hypothesis is needed here.

0.4  Why the answer is not obvious, and how the proof is organized.

The positive side (Part 2) assumes a measure on the full power set of the
continuum. That measure is so strong that it lets you average over the
continuum, forbid exceptional sets of size below c, and force a configuration
of functionals that produces an unconditional basic sequence, which in turn
produces a separable quotient. The negative side (Parts 4-8) assumes CH, so
the continuum has size aleph_1, and builds a single nasty Banach space whose
dual is packed with "path functionals" that make every separable subspace of
the dual fail to capture the evaluations it should; the evaluation criterion
of Part 1 then blocks all separable quotients.

The two sides share exactly one tool, the evaluation criterion of Part 1. The
positive side uses it to turn a large evaluation image into a quotient; the
negative side uses it to turn a small evaluation image into the absence of a
quotient.

Now we build everything. No step is skipped.


==============================================================================
PART 1.  THE EVALUATION CRITERION
==============================================================================

1.1  The idea in one paragraph.

The dual X^* of a Banach space X is the space of all bounded linear
functionals f: X -> scalars, normed by ||f|| = sup over the unit ball of X of
|f(x)|. For a closed subspace F of X^* we ask a very concrete question: as x
runs over the unit ball of X, how big is the set of functions (f |-> f(x)) on
F? If that set is separable, a quotient appears; if it never is, no quotient
exists. That single dichotomy is used by both halves of the paper, in opposite
directions. This part proves the dichotomy.

1.2  The evaluation map.

For a closed subspace F of X^*, define
  R_F: X -> F^*,  (R_F x)(f) = f(x)  for f in F.
This is a bounded linear map, with ||R_F|| <= 1 because |f(x)| <= ||f|| ||x||.
Its image R_F(X) is a subspace of F^*. "R_F(X) is norm separable" means some
countable subset of it is dense in it.

1.3  Prefix normers make a basic sequence with controlled projections.

LEMMA 1 (prefix normers). Let f_1, f_2, ... be functionals in X^* with
0 < a <= ||f_n|| <= b < infinity. Suppose that for every m >= 1 there is a
finite set D_m inside the unit ball of X such that
   (a) for every v in span{f_1, ..., f_m}:  max over d in D_m of |v(d)| is at
       least (1/2)||v||, i.e. D_m is a 1/2-norming set for that span, and
   (b) for every n > m and every d in D_m:  f_n(d) = 0.
Then:
  (i)   the f_n are linearly independent and form a basic sequence whose
        prefix projections P_m: G -> G, P_m(sum c_i f_i) = sum_{i<=m} c_i f_i,
        have norm at most 2;
  (ii)  every finite sum satisfies |c_n| <= (4/a) ||sum_i c_i f_i||, so the
        basis coefficient functional f_n^# on G has norm at most 4/a;
  (iii) writing G = closed span{f_n}, Z = closed span{f_n^#} inside G^*, if
        R_G(X) is contained in Z then R_G: X -> Z is onto, and in fact its
        adjoint obeys ||R_G^* h|| >= (1/2)||h|| for every h in Z^*.

PROOF. Linear independence: if f_n lay in span{f_1, ..., f_{n-1}} then it
would vanish on D_{n-1} by (b), contradicting ||f_n|| >= a > 0.

Prefix projections. Fix a finite sum v = sum_{i=1}^N c_i f_i and let
u_m = sum_{i=1}^m c_i f_i for m <= N. On D_m, each f_n with n > m vanishes,
so u_m and v take the same values there. By (a) applied to u_m, which lies in
span{f_1,...,f_m},
  ||u_m|| <= 2 max_{d in D_m} |u_m(d)| = 2 max_{d in D_m} |v(d)| <= 2 ||v||.
So each prefix projection has norm at most 2 on the finite sums, and it
extends by continuity to G. The projections converge to the identity on G
because they do on the dense set of finite sums, so the f_n form a basic
sequence.

Coefficients. With the same notation, P_m v - P_{m-1} v = c_m f_m. Hence
 |c_m| ||f_m|| = ||P_m v - P_{m-1} v|| <= (||P_m|| + ||P_{m-1}||) ||v|| <= 4 ||v||,
giving |c_m| <= (4/a)||v||. This proves (ii): f_m^# has norm at most 4/a on G.

Adjoint bound. Write T = R_G: X -> Z. Fix h in Z^*. For m >= 1 put
  v_m = sum_{i=1}^m h(f_i^#) f_i  in G.
For d in D_m, the functional Td equals sum_{i=1}^m f_i(d) f_i^# because the
later f_n vanish at d. Therefore
  (T^* h)(d) = sum_{i=1}^m f_i(d) h(f_i^#) = v_m(d).
By the norming property (a) of D_m, ||T^* h|| >= (1/2)||v_m||.

Now for every finite linear combination u of the f_i^#, u(v_m) equals h(u)
for all m larger than the highest index appearing. The combinations u are
dense in Z, so
  ||h|| = sup{ h(u) : u in Z, ||u|| <= 1 } <= sup_m ||v_m|| <= 2 ||T^* h||.
Notice we never required the v_m to converge. This finishes the proof of the
adjoint bound and hence of Lemma 1.   []

Remark. The only place a "norming set" is used is to convert values at the
points of D_m into a lower bound on the norm of v_m. That is why condition (a)
is stated with the factor 1/2, exactly compensating the factor 2 in the prefix
projections.

1.4  An adjoint lower bound means the map is onto.

We need the elementary passage from an adjoint lower bound to surjectivity.

FACT. Let T: X -> Z be a bounded linear map between Banach spaces. Suppose
that ||T^* h|| >= c ||h|| for some c > 0 and every h in Z^*. Then T maps X
onto Z, and each z in Z is the image of some x with ||x|| <= (2/c)||z||.

PROOF. Let B_X and B_Z be the unit balls. We first claim c B_Z lies in the
closure of T(B_X). If not, some z with ||z|| <= c lies outside the closed
convex balanced set closure(T(B_X)). Hahn-Banach separates such a point: there
is h in Z^* with h(z) > 1 and |h(y)| <= 1 for every y in closure(T(B_X)). Then
||T^* h|| = sup over x in B_X of |h(Tx)| <= 1, while
  ||h|| >= h(z)/||z|| > 1/||z|| >= 1/c,
so c||h|| > 1 >= ||T^* h||, contradicting the hypothesis. This proves the
claim.

Now hit any z in Z, z != 0, by a series. The rescaling w = z/||z|| lies on the
unit sphere, so c w lies in c B_Z, which sits in closure(T(B_X)): pick x_1 in
B_X with ||c w - Tx_1|| <= c/2. Then x_1' = ||z|| x_1 satisfies
  ||x_1'|| <= ||z|| / c  and  ||z - T x_1'|| <= ||z|| / 2.
Repeat on the residual r_1 = z - T x_1': choose x_2 with ||x_2|| <= ||r_1||/c
and ||r_1 - T x_2|| <= ||r_1||/2 <= ||z||/4. Continue. The residuals shrink by
half each time, so the x_j have summable norms with
  sum_j ||x_j|| <= (||z||/c)(1 + 1/2 + 1/4 + ...) = 2||z||/c.
The partial sums form a Cauchy sequence in X, converging to some x with
||x|| <= 2||z||/c, and T x = z by continuity and the telescoping of residuals.
This proves the Fact.   []

Combining the Fact with the adjoint bound (1/2) of Lemma 1(iii) immediately
shows that R_G: X -> Z is onto whenever R_G(X) is contained in Z.

1.5  The evaluation criterion.

PROPOSITION 2 (criterion). Let X be an infinite-dimensional real or complex
Banach space. The following are equivalent:
  (1) X admits a bounded linear surjection onto a separable infinite-
      dimensional Banach space;
  (2) some closed infinite-dimensional subspace F of X^* has R_F(X) norm
      separable.
In (2) we may additionally require F to be separable.

PROOF of (1) => (2). Suppose T: X -> Y is such a surjection, Y separable
infinite-dimensional. Choose a closed separable infinite-dimensional subspace
U of Y^*. (For example take the closed span of any infinite linearly
independent sequence in Y^*; density of that span is inherited from Y^*, which
is separable when Y is.) Because T is a bounded surjection, the open mapping
theorem gives T^* bounded below, so F = T^* U is a closed infinite-dimensional
separable subspace of X^*. For x in X, evaluation at x on F factors: for
f = T^* u with u in U, f(x) = u(Tx). So R_F(X), read through the isomorphism
T^*: U -> F, is the image of the bounded map x |-> (u |-> u(Tx)) from X into
U^*, which lands in the separable space Y viewed as a subspace of U^*. Hence
R_F(X) is norm separable. This proves (1) => (2) with F separable.

PROOF of (2) => (1). Assume R_F(X) is norm separable and pick x_1, x_2, ...
with R_F x_j dense in R_F(X). We build a sequence f_1, f_2, ... in F of norm
1. At stage n, we impose finitely many homogeneous linear conditions:
   f_n annihilates x_1, ..., x_n, and annihilates every set D_m with m < n.
The set of f in F obeying these conditions is closed and finite-codimensional,
so it contains a unit vector f_n. After choosing f_n, choose D_n in the unit
ball of X that is 1/2-norming for span{f_1, ..., f_n}; such a finite set
exists by compactness of the unit sphere of that finite-dimensional space.
These choices satisfy all hypotheses of Lemma 1. Let G = closed span{f_n}
and Z = closed span{f_n^#}.

We verify R_G(X) is contained in Z. For a fixed j, f_n(x_j) = 0 whenever n > j
by construction, so
  R_G x_j = sum_{n< j} f_n(x_j) f_n^# ,
a finite combination of the f_n^#. Thus R_G x_j lies in Z for every j. Since
the R_F x_j are dense in R_F(X) and restriction F^* -> G^* is contractive,
the set of R_G x_j is dense in R_G(X); because Z is closed, R_G(X) is in Z.

Now Lemma 1 applies and tells us R_G: X -> Z is onto. The functionals f_n^#
are linearly independent (they are basis coefficient functionals), so Z is
infinite-dimensional and separable. Thus the image Z is a separable
infinite-dimensional Banach space and R_G is a bounded linear surjection onto
it. This proves (2) => (1), and along the way shows the witness F = G in (2)
can always be taken separable.   []

This is the single shared tool. Everything else in the paper is either the
construction of a separable R_F(X) (Part 2) or the proof that no such F exists
(Parts 4-8).


==============================================================================
PART 2.  A MEASURABLE CONTINUUM FORCES SEPARABLE QUOTIENTS
==============================================================================

2.1  What this part does, and what it assumes.

This part proves the positive half of the main theorem over the reals: if the
continuum carries a very strong measure, then every infinite-dimensional real
Banach space has a separable infinite-dimensional quotient. The whole argument
has two moves, and it is worth seeing them before the details.

The first move assumes a counterexample X, fixes any separable
infinite-dimensional subspace E of X^*, and shows that the set of evaluations
R_E(B_X) has to be as big as possible, of density c. If it were smaller, we
could thread basic sequences inside it and apply the evaluation criterion to
get a quotient, contradiction.

The second move uses that huge size to find a family of functionals f_alpha in
X^*, indexed by the continuum, which evaluated at any single fixed point are
almost all zero. Odell-Rosenthal turns those functionals into weak-star limit
sequences, which we code by Borel functions on a Polish space; ordinary
Fubini then picks one infinite sequence of them whose finite-prefix suppression
estimates hold almost surely. That sequence is an unconditional basic sequence
in X^*, which is known to give a separable quotient.

2.2  The measure hypothesis.

Let kappa = c = 2^{aleph_0}, viewed as an initial ordinal. We assume there is a
function mu from the full power set of kappa to [0,1] with these properties:
   (M1) mu(kappa) = 1 and mu(empty) = 0.
   (M2) mu({alpha}) = 0 for every alpha in kappa.
   (M3) mu is countably additive.
   (M4) for any family (A_xi) of pairwise disjoint subsets of kappa indexed by
        an ordinal lambda < kappa,
           mu(union A_xi) = sup over finite F of sum_{xi in F} mu(A_xi).
We call a number kappa carrying such a measure (with (M4) for all lambda < kappa)
real-valued measurable. The hypothesis of this part is exactly that c is
real-valued measurable. Property (M4) is much stronger than (M3): it controls
unions of fewer than c disjoint sets, not merely countably many.

The immediate consequence we will use most: any set of cardinality less than
c is null. Indeed such a set is a union of fewer than c singletons, all null.

2.3  Three basic facts about mu.

LEMMA 5 (measure basics). Under (M1)-(M4):
  (a) kappa is a regular cardinal;
  (b) mu is atomless: every set A with mu(A) > 0 contains a subset B with
      0 < mu(B) < mu(A), and in fact one with mu(B) <= mu(A)/2;
  (c) for every A and every real t with 0 <= t <= mu(A) there is B subset A
      with mu(B) = t. In particular, kappa splits into N subsets each of
      measure 1/N for every positive integer N.

PROOF of (a). A set of size below kappa is null. If kappa had cofinality
lambda < kappa, the initial segments [0, xi) for a cofinal family of xi below
kappa would be fewer than kappa sets, each of size below kappa and hence null.
Their union would be kappa, so kappa would be null, contradicting (M1). Thus
cf(kappa) = kappa.

PROOF of (b), atomlessness. Fix an injection b: kappa -> {0,1}^N; we may
suppose b separates points. Call A a positive atom if mu(A) > 0 and every
subset of A has measure either mu(A) or 0. Suppose A is a positive atom of
measure m > 0. For each bit position i split A by the value of bit i of b,
into A_i^0 and A_i^1. On an atom one of the two has measure m and the other 0;
define A_{i+1} to be the one of measure m, beginning with A_0 = A. The A_i are
decreasing and all have measure m. By countable additivity the intersection of
the A_i has measure lim m = m. But the intersection consists of all points of
A whose bits match the chosen ones at every position, so it is a single point
of A, of measure 0. This contradicts m > 0, so A cannot be an atom. Since a
non-atom A always has two complementary subsets neither of which has all the
mass, one of them has measure in (0, mu(A)]; taking the smaller if necessary
gives a piece of measure at most mu(A)/2 and positive.

PROOF of (c), divisibility. We handle general t, then say how to get equal
parts. First, every positive set has positive subsets of arbitrarily small
measure: repeatedly split a positive set into two positive parts and keep the
smaller; by (b) this halves the measure each time.

Now fix A and t with 0 < t < mu(A). We build sets C_0 = empty inside C_1
inside C_2 inside ... of A, all of measure at most t, with mu(C_i) tending up
to t. At step i the remainder R_i = A \ C_i is positive. Split R_i into two
positive parts, keep the part of smaller measure, and repeat until the resulting
piece E_i has measure at most the smaller of (t - mu(C_i)) and 2^{-i}. This is
possible because positive pieces of arbitrarily small measure exist in R_i.
Set C_{i+1} = C_i union E_i. Then mu(C_{i+1}) = mu(C_i) + mu(E_i) <= t, and the
partial sums increase toward a limit L <= t. Since at every step mu(E_i) is at
most 2^{-i}, the limit is at least t - 2^{-i+1}, so L = t. The union C of the
C_i is a subset of A of measure t by countable additivity. The reverse
inequality check: for any finite union of E_i the sum equals the measure of the
union (disjoint), and the total of all E_i is sum_i mu(E_i) >= t (since the
C_i increase to measure t and C is a union of disjoint E_i), so mu(C) = t.

To split kappa into N pieces of measure 1/N, apply (c) with A = kappa and
t = 1/N to get B_1 of measure 1/N, then the same in the complement, and so on.
This proves Lemma 5.   []

2.4  Failure of a quotient forces the evaluation image to be huge.

The first move of the positive direction. We need one classical input:

DVORETZKY'S THEOREM (Dvoretzky 1961; see Figiel 1976 for a short proof). For
every infinite-dimensional Banach space E, every positive integer n, and every
eps > 0, there are vectors u_1, ..., u_n in E such that for every real
a_1, ..., a_n,
   ||a||_2 <= ||sum_j a_j u_j|| <= (1 + eps)||a||_2,
where ||a||_2 = (sum_j a_j^2)^{1/2}. We use the case eps = 1, so the upper
factor is 2. Since the conclusion is stable under passing to infinite-
dimensional subspaces, we may also apply it inside any infinite-dimensional
closed subspace.

LEMMA 6 (density). Let X be a real Banach space with no separable
infinite-dimensional quotient, and let E be an infinite-dimensional separable
closed subspace of X^*. Assume the measure hypothesis of 2.2 on kappa = c. Then
D = R_E(B_X) is a subset of the unit ball of E^* of norm density exactly kappa.
In particular D is not separable.

PROOF. A functional in E^* is determined by its values on a fixed countable
dense subset of E, so E^* has cardinality at most c and so |D| <= kappa. We
suppose A subset D is norm dense with |A| < kappa and derive a contradiction.

Choose integers N_n = 16^n. We build rows (u_{n,1}, ..., u_{n, N_n}) inside E
with two goals.
   (R1) The row is 2-isomorphic to Euclidean space: for every a,
           ||a||_2 <= ||sum_j a_j u_{n,j}|| <= 2||a||_2.
   (R2) Once D_n is chosen, all later rows vanish at every point of D_n.
Here D_n will be a finite subset of B_X that 1/2-norms the span of all rows up
to n. "Later rows vanish at D_n" means u_{k,j}(d) = 0 for every k > n, every j,
and every d in D_n.

The inductive step. Suppose rows 1, ..., n-1 are chosen and D_1, ..., D_{n-1}
are chosen. Let F_n be the span in X of D_1 union ... union D_{n-1}; this is
finite-dimensional. The set
   E_n = { u in E : u(d) = 0 for every d in F_n }
is closed, is finite-codimensional in E (annihilating a finite-dimensional
subspace of X), and is infinite-dimensional because E is. By Dvoretzky's
theorem with eps = 1 applied inside E_n, pick u_{n,1}, ..., u_{n,N_n} in E_n
obeying (R1). Then choose D_n in B_X that 1/2-norms the span of all rows up to
n. This set exists because the unit sphere of a finite-dimensional space is
compact: pick, for a delta-net of directions, a functional almost achieving
the norm, and take the finite union of the resulting near-norming sets. Rows
1 through n are chosen, and by construction every later row will vanish on
D_n.

The partition at step n. By Lemma 5(c), kappa splits into N_n subsets of
measure 1/N_n. Label those subsets j_n^{-1}(1), ..., j_n^{-1}(N_n), giving a
map j_n: kappa -> {1, ..., N_n} with equal fibers.

The averaging estimate. Fix y in A and let x in B_X have R_E x = y, so
||y||_{E^*} <= 1. By (R1),
   ||(y(u_{n,1}), ..., y(u_{n,N_n}))||_2 <= 2||y||_{E^*} <= 2.
By Cauchy-Schwarz and the equal-fiber measure,
   E_alpha[ |y(u_{n, j_n(alpha)})| ] = (1/N_n) sum_j |y(u_{n,j})|
      <= (1/N_n) sqrt(N_n) * sqrt(sum_j |y(u_{n,j})|^2) <= 2 / sqrt(N_n).
Summing over n,
   sum_n E_alpha[ |y(u_{n, j_n(alpha)})| ] <= 2 sum_n 1/sqrt(N_n)
      = 2 sum_n 1/4^n = 2/3 < infinity.
By monotone convergence on the discrete sum, sum_n |y(u_{n, j_n(alpha)})| <
infinity for mu-almost every alpha.

Intersecting conull sets. We must simultaneously guarantee this for every y in
A. Since |A| < kappa and mu is additive over < kappa disjoint pieces (which is
all we need: a union of fewer than kappa null sets is null), the intersection of
the conull sets over y in A is conull and, in particular, nonempty. Choose
alpha_0 in it and set g_n = u_{n, j_n(alpha_0)} in E. Then for every y in A,
   sum_n |y(g_n)| < infinity.                                     (*)

The basic sequence. The g_n satisfy ||g_n|| in [1, 2]. The set D_n 1/2-norms
the span of all rows up to n, hence in particular 1/2-norms span{g_1,...,g_n}
(that span sits inside the span of rows up to n). And g_k, lying in row k > n,
vanishes on D_n by (R2). So Lemma 1 applies with a = 1, b = 2. It produces a
basic sequence (g_n), prefix projections of norm at most 2, and coefficient
functionals g_n^# in G^* of norm at most 4.

Contradicting the hypothesis. Put G = closed span{g_n} and Z = closed span
{g_n^#} inside G^*. Fix y in A. By (*) the series
   sum_n y(g_n) g_n^#
converges in G^*: its tail from index m has norm at most 4 sum_{n>m} |y(g_n)|,
which tends to zero. On the dense algebraic span of the g_i this sum equals
y|_G, because the coefficient functionals are the dual basis. So y|_G belongs
to the closed subspace Z. Thus R_G(A) is contained in Z.

Now restriction from E^* to G^* is contractive and A is norm dense in D, so
R_G(B_X) is contained in the closed set Z. Since B_X spans X, R_G(X) is contained
in Z. Lemma 1 then makes R_G: X -> Z onto. The codomain Z is a separable
infinite-dimensional Banach space. This is a separable infinite-dimensional
quotient of X, contradicting the hypothesis. So |A| < kappa was impossible and
the density is exactly kappa. This proves Lemma 6.   []

2.5  A continuum-indexed family that is pointwise almost everywhere zero.

The large density from 2.4 is now converted into a continuum-sized family of
functionals in X^* that, evaluated at any single fixed point of the unit ball
of X, is almost always zero. The price is that each functional only has lower
norm epsilon, not one, but that is harmless downstream.

LEMMA 7 (family). Let X and E satisfy the hypotheses of Lemma 6 (X has no
separable infinite-dimensional quotient; E is an infinite-dimensional
separable closed subspace of X^*; the measure hypothesis of 2.2 holds on
kappa = c). Then there are epsilon > 0 and functionals h_alpha in the unit
sphere of E^{**}, indexed by alpha < kappa, such that the functionals
f_alpha = h_alpha R_E in X^* satisfy:
   (F1) epsilon < ||f_alpha|| <= 1 for every alpha;
   (F2) for every y in R_E(B_X), the set { alpha : h_alpha(y) != 0 } has
        measure zero.

PROOF. Write D = R_E(B_X). Two preliminary observations.

First observation: there is delta > 0 and a delta-separated subset of D of
cardinality kappa. Suppose to the contrary that, for every delta > 0, every
delta-separated subset of D has cardinality < kappa. For each n >= 1 pick a
maximal 1/n-separated subset S_n. Maximality means every point of D is within
1/n of some point of S_n: if not, that point could be adjoined and separation
would survive, contradicting maximality. So each S_n is a 1/n-net of D. By
the supposition |S_n| < kappa. Since kappa is regular and there are countably
many n, |union S_n| < kappa. The union is dense in D (for any point and any
1/n, the 1/n-net provides a member within 1/n). This contradicts Lemma 6,
which says D has density kappa. So a delta-separated subset of size kappa
exists for some delta > 0.

Second observation: for every alpha < kappa and every closed subspace
M subset E^* of density < kappa, some y in D has dist(y, M) > delta/4. Here
dist(y, M) = inf{||y - m|| : m in M}. Suppose not: every point of the
delta-separated set S from the first observation is within delta/4 of M. Pick
a norm-dense subset A_M of M of cardinality < kappa. For each s in S choose
m(s) in M with ||s - m(s)|| <= delta/4, then m'(s) in A_M with
||m(s) - m'(s)|| < delta/8. If s and s' share m'(s) = m'(s'), then
||s - s'|| <= ||s - m(s)|| + ||m(s) - m'|| + ||m' - m(s')|| + ||m(s') - s'||
< delta/4 + delta/8 + delta/8 + delta/4 = 3 delta / 4 < delta,
contradicting delta-separation. So s |-> m'(s) is injective. But its domain
has size kappa and its range is A_M of size < kappa, a contradiction. This
proves the second observation.

The construction. Enumerate D as y_beta for beta < kappa. For each alpha <
kappa let M_alpha be the closed linear span in E^* of { y_beta : beta < alpha }.
This closed span has density at most |alpha| < kappa because |alpha| < kappa
and kappa is regular.

By the second observation applied to alpha, some y in D has distance greater
than delta/4 from M_alpha. Since M_alpha is a closed subspace, Hahn-Banach
separation gives a functional h_alpha in E^{***} = E^{**} of norm one (the
quotient or the separating functional is naturally an element of E^{**}) that
annihilates M_alpha and satisfies |h_alpha(y)| > delta/4. Because y is in D it
is of the form R_E x for some x in the unit ball of X; hence the functional
f_alpha = h_alpha R_E satisfies |f_alpha(x)| > delta/4 with ||x|| <= 1. So
   epsilon < ||f_alpha|| <= 1, epsilon := delta/4,
which is (F1), noting ||f_alpha|| <= ||h_alpha|| ||R_E|| <= 1.

For (F2), fix y = y_beta in D. For every alpha with alpha > beta, the point
y_beta lies in M_alpha by definition of M_alpha, so h_alpha(y_beta) = 0. Thus
the nonzero evaluations h_alpha(y_beta) can occur only for alpha <= beta, a
set of cardinality |beta| < kappa and therefore of measure zero (sets of size
below kappa are null). This proves Lemma 7.   []

2.6  Borel coding and ordered sampling.

This subsection proves the sampling lemma. It is the only place in the positive
direction where we use the fact that the measure lives on the FULL power set of
I. Everything else uses countable additivity, but the full power-set sigma
algebra makes every function alpha |-> c_alpha measurable, which is what lets
us push forward mu to a Borel measure on a Polish space and then apply ordinary
Fubini.

First, one more classical input, and one small Borel fact.

ODELL-ROSENTHAL THEOREM (Odell and Rosenthal 1975). Let E be a separable
Banach space. Then E contains no isomorphic copy of l_1 if and only if every
element of E^{**} is the weak-star limit of a sequence from E (the canonical
image of E inside E^{**}).

BOREL FACT. Let E be separable. Then E^N with the product of norm topologies
and K = B_{E^*} with the weak-star topology are both Polish (the first is a
countable product of Polish spaces, the second is compact metrizable by
Banach-Alaoglu plus separability of E). Furthermore, for any c in E^N,
   Phi(c, y) := lim_n y(c_n)  if this exists, and 0 otherwise,
is a Borel function on E^N x K. Proof: each map (c, y) |-> y(c_n) is
continuous, and the Cauchy criterion makes the convergence set Borel; a pointwise
limit of continuous functions on a Borel subset is Borel.

LEMMA 8 (sampling). Let X be a real Banach space, E subset X^* a separable
closed subspace containing no isomorphic copy of l_1, and D = R_E(B_X). Let I
carry a countably additive probability mu on the FULL power set of I,
vanishing on singletons. Suppose (h_alpha) alpha in I is a family in E^{**}
with mu{alpha : h_alpha(y) != 0} = 0 for every y in D, and with the functionals
f_alpha = h_alpha R_E in X^* satisfying
   0 < epsilon <= ||f_alpha|| <= M < infinity  for every alpha in I.
Then X^* contains an infinite unconditional basic sequence.

PROOF. The Odell-Rosenthal theorem applies because E has no l_1. Choose for
each alpha in I a sequence c_alpha = (c_alpha,1, c_alpha,2, ...) in E with
c_alpha,n converging to h_alpha in the weak-star topology, i.e.
   lim_n y(c_alpha,n) = h_alpha(y)  for every y in E^*.
Equip E^N with product of norm topologies, K = B_{E^*} with weak-star topology.
The map alpha |-> c_alpha is measurable because the sigma algebra on I is the
full power set. Let eta be the pushforward of mu on E^N. Define
   H(y) = int_{E^N} 1_{Phi(c,y) != 0} d_eta(c),  y in K,
a Borel function of y by parameter integration. For y in D,
   H(y) = int_I 1_{Phi(c_alpha,y) != 0} d_mu(alpha)
        = int_I 1_{h_alpha(y) != 0} d_mu(alpha)
        = mu{alpha : h_alpha(y) != 0} = 0.
So H vanishes identically on D.

Ordered product measures on I^n. For n >= 1 define a probability lambda_n on
the full power set of I^n by ordered iteration, beginning with the first
variable outermost:
   lambda_n(A) = int_I ... int_I 1_A(alpha_1, ..., alpha_n) d_mu(alpha_n) ... d_mu(alpha_1).
Put lambda_0 equal to unit mass on the empty tuple. Because every function on
the power-set sigma algebra is mu-measurable, every section and every
intermediate integrand is measurable. Countable additivity of lambda_n follows
from the same property of mu and monotone convergence; the ordered iterated
integral formula for bounded functions follows from approximation by simple
functions. Note that this construction does not assert Fubini (change of
order) for arbitrary functions, only that the ordered iterated integrals are
well-defined probabilities.

Normer choice. Fix n >= 1, rational numbers a_1, ..., a_n, and a subset
s subset {1, ..., n}. For every tuple (alpha_j)_{j in s} of indices, choose
x_s = x_s(alpha_j : j in s) in B_X with
   |sum_{j in s} a_j f_{alpha_j}(x_s)| >= (1/2)||sum_{j in s} a_j f_{alpha_j}||.
If the sum is zero, take x_s = 0. The choice depends only on the indices in s,
so it notably does not depend on any alpha_i with i not in s.

Cross-vanishing. We claim that for i not in s,
   f_{alpha_i}(x_s) = 0  for lambda_n-almost every tuple (alpha_1, ..., alpha_n).
Fix any earlier prefix (alpha_1, ..., alpha_{i-1}). The map
   Y: I^{n-i} -> K,  Y(alpha_{i+1}, ..., alpha_n) = R_E x_s,
is independent of alpha_i because x_s depends only on the alpha_j with j in s,
and i is not in s. It takes values in D exactly. Let nu = Y_* lambda_{n-i},
the pushforward of the ordered measure lambda_{n-i} by Y. Now consider the
ordered integral, starting at variable i, of the indicator of a nonzero
evaluation:
   int_I  int_{I^{n-i}}  1_{Phi(c_{alpha_i}, Y(t)) != 0}  d_lambda_{n-i}(t) d_mu(alpha_i).
Substituting c = c_{alpha_i} and y = Y(t), and rewriting as an integral over
I x I^{n-i} against the product measure mu x lambda_{n-i}, then pushing forward
by (alpha_i, t) |-> (c_{alpha_i}, Y(t)) whose coordinates depend on disjoint
variables (so the pushforward factorizes as eta x nu), we get
   int_{E^N} int_K 1_{Phi(c, y) != 0} d_nu(y) d_eta(c).
The swap of integration order here is ordinary Fubini for a Borel function on
the product of two Polish spaces with Borel probability measures. The result
equals
   int_K H(y) d_nu(y) = 0.
The last equality does not require D to be Borel: the Borel set {H != 0} has
empty inverse image under Y because nu is supported on D and H is zero on D is
not true, but Y takes values in D and H vanishes on D, so {H != 0} cap D is
empty, so Y^{-1}({H != 0}) is empty, hence nu-null. Thus the ordered integral
is zero. The inner integrand is nonnegative, so f_{alpha_i}(x_s) = 0 for
mu-almost every alpha_i for every fixed earlier prefix; integrating over the
prefix (with respect to lambda_{i-1}) shows the exceptional set has lambda_n
measure zero. This proves cross-vanishing.

Suppression. Combining cross-vanishing with the normer inequality:
   |sum_{j=1}^n a_j f_{alpha_j}(x_s)|
     = |sum_{j in s} a_j f_{alpha_j}(x_s) + sum_{j not in s} a_j f_{alpha_j}(x_s)|
     = |sum_{j in s} a_j f_{alpha_j}(x_s)|
     >= (1/2)||sum_{j in s} a_j f_{alpha_j}||.
On the other hand ||x_s|| <= 1, so
   |sum_{j=1}^n a_j f_{alpha_j}(x_s)| <= ||sum_{j=1}^n a_j f_{alpha_j}||.
Hence
   ||sum_{j in s} a_j f_{alpha_j}|| <= 2||sum_{j=1}^n a_j f_{alpha_j}||.   (*)

Distinctness. For r < t, the event alpha_t = alpha_r: the prefix
(alpha_1, ..., alpha_{t-1}) is fixed, and once it is fixed the value of alpha_r
is known; requiring alpha_t = alpha_r pins alpha_t to a single point, an event
of mu-measure zero by the vanishing on singletons. So the event has
lambda_n-measure zero.

Packaging for each n. Fix n. There are countably many rational coefficient
tuples (a_1, ..., a_n) and finitely many subsets s thereof. Taking the union of
the countably many null exceptional sets just constructed, there is a single
set G_n subset I^n of lambda_n-measure one on which distinctness and every
suppression inequality (*) for the given n hold.

Selecting one infinite sequence. We must choose alpha_1, alpha_2, ... whose
every finite prefix lies in the corresponding G_j. Suppose a finite prefix
p = (alpha_1, ..., alpha_m) has been chosen with all its nonempty prefixes in
their respective G_j and with the invariant
   lambda_{n-m}((G_n)_p) = 1   for every n > m,
where (G_n)_p = { (alpha_{m+1}, ..., alpha_n) : (p, alpha_{m+1}, ..., alpha_n)
in G_n } is the section of G_n above p. The invariant holds for the empty
prefix. For n = m+1, the invariant reads (p, alpha) in G_{m+1} for mu-almost
every alpha. For every n > m+1, the definition of the ordered measures gives
   1 = lambda_{n-m}((G_n)_p)
     = int_I lambda_{n-m-1}((G_n)_{(p, alpha)}) d_mu(alpha).
The integrand is in [0,1], so it equals 1 for mu-almost every alpha. The
intersection of these countably many conull sets is conull and nonempty;
choose the next index there. This constructs the infinite sequence. Note again
that we never needed an infinite product measure; each finite step only uses
finite-dimensional ordered masses.

Unconditional basic sequence. The inequalities (*) extend by continuity from
rational to real coefficients on every finite prefix. The singletons of s give
the coordinate suppressions
   ||a_j f_{alpha_j}|| <= 2||sum_{i=1}^n a_i f_{alpha_i}||  for every j,
which with ||f_{alpha_j}|| >= epsilon forces linear independence. Further, the
initial-segment projections have norm at most 2 on the algebraic span and
extend to its closure; approximation by finite sums makes those projections
converge to the identity, so the sequence is a Schauder basis for its closed
span. Every finite coordinate suppression has norm at most 2. Given a vector
approximated within delta by a finite sum, every finite coordinate sum outside
that sum's support has norm at most 2 delta, so the basis expansion converges
unconditionally. This proves Lemma 8.   []

2.7  The positive conclusion over the reals.

We now combine everything. We need one last external input.

HAGLER-JOHNSON / ARGYROS-DODOS-KANELLOPOULOS. If X is a real or complex
Banach space whose dual X^* contains an infinite unconditional basic sequence,
then X has a separable infinite-dimensional quotient (in fact, with an
unconditional basis). This is Proposition 16 of Argyros, Dodos, and
Kanellopoulos, "Unconditional families in Banach spaces" (Math. Ann. 2008),
building on Hagler and Johnson (Israel J. Math. 1977).

THEOREM 9 (positive implication over R). Assume the measure hypothesis of 2.2
on kappa = c. Then every infinite-dimensional real Banach space X has a
separable infinite-dimensional quotient.

PROOF. Suppose some infinite-dimensional real Banach space X has no separable
infinite-dimensional quotient; we derive a contradiction.

By the Hagler-Johnson / Argyros-Dodos-Kanellopoulos result just quoted, the
dual X^* contains no infinite unconditional basic sequence.

Choose an infinite-dimensional separable closed subspace E of X^*. Such an E
exists because any infinite-dimensional Banach space (here X^*) contains the
closed span of a countably infinite linearly independent set, which is
separable. The space E contains no copy of l_1: if it did, the standard
unconditional unit vector basis of l_1 would sit in E, hence in X^*, as an
infinite unconditional basic sequence, contradicting the previous paragraph.
So E satisfies all the hypotheses of Lemma 6 (X has no separable quotient, E
separable closed infinite-dimensional, measure hypothesis).

Apply Lemma 6: D = R_E(B_X) has norm density kappa.

Apply Lemma 7: there are epsilon > 0 and functionals h_alpha in the unit sphere
of E^{**}, indexed by alpha < kappa, whose products f_alpha = h_alpha R_E in
X^* satisfy epsilon < ||f_alpha|| <= 1 and, for every y in D,
mu{alpha : h_alpha(y) != 0} = 0.

Now apply Lemma 8 with I = kappa (equipped with the measure of 2.2, which is
countably additive on the full power set), with D = R_E(B_X), with the family
h_alpha of Lemma 7, with M = 1, and with the epsilon of Lemma 7. Lemma 8
concludes that X^* contains an infinite unconditional basic sequence. That
contradicts the Hagler-Johnson / ADK result. So no X is a counterexample, and
Theorem 9 holds.   []

This completes the positive direction over R. The next part transfers it to
C and prepares the corresponding transfer for the counterexamples.


==============================================================================
PART 3.  FROM REAL TO COMPLEX SCALARS
==============================================================================

3.1  What this part does.

Theorem 9 proved the positive implication over the reals. To get the complex
version we need to see how a complex Banach space and its underlying real
space are related. The positive direction of this translation is proved here;
the counterexample direction is prepared here and applied in Part 8.

Auxiliary input. We need one general Banach space lemma that was also used in
Parts 4-7 of the negative direction. It goes here because the positive transfer
is its first consumer.

LEMMA 10 (small restrictions of strictly singular operators). Let T: Y -> Z
be a bounded linear map between real or complex Banach spaces. Call T strictly
singular if no closed infinite-dimensional subspace of Y maps injectively and
boundedly below under T; equivalently, if for every closed infinite-dimensional
subspace M of Y there is a closed infinite-dimensional subspace of M on which
T is as small as we like. Precisely:

For every closed infinite-dimensional M subset Y and every eps > 0, there is
a closed infinite-dimensional N subset M such that ||T|_N|| <= eps. If T_1,
..., T_k is a finite family of strictly singular operators, then one N subset
M works simultaneously: ||T_j|_N|| <= eps for every j.

PROOF. Fix a sequence of positive numbers d_n with sum d_n < eps/8. We build
unit vectors y_1, y_2, ... in M. Inductively, after y_1, ..., y_{n-1} are
chosen, let D_{n-1} be a finite set in the unit ball of Y^* that is a
1/2-norming set for their span. The set of y in M vanishing on every member of
D_{n-1} is a closed finite-codimensional subspace of M, hence infinite-
dimensional. Restricted to that subspace, T is not bounded below (by strict
singularity), so there is a unit y_n in it with ||T y_n|| < d_n. This gives a
sequence y_n.

By the prefix calculation of Lemma 1 (vectors and norming functionals
interchanged) the y_n form a basic sequence with coefficients satisfying
|a_n| <= 4||sum a_i y_i||. Therefore
   ||T sum_n a_n y_n|| <= 4 sum_n ||T y_n|| ||sum_n a_n y_n||
                     <= 4 (sum_n d_n) ||sum_n a_n y_n||
                     <= (eps/2)||sum_n a_n y_n||.
By continuity the same bound holds on N = closed span of the y_n.

For finitely many T_j, apply the one-operator result successively inside the
space already obtained. A restriction of a strictly singular operator to a
smaller closed infinite-dimensional subspace remains strictly singular, and
previous bounds persist on subspaces. This proves Lemma 10.   []

3.2  The positive direction: real to complex.

We now prove that a separable infinite-dimensional real quotient of the
underlying real space of a complex Banach space yields a separable
infinite-dimensional complex quotient of the complex space itself.

PROPOSITION 11 (positive transfer). Let X be an infinite-dimensional complex
Banach space, and let X_R be its underlying real space. If X_R has a separable
infinite-dimensional real quotient, then X has a separable infinite-dimensional
complex quotient.

PROOF. The seed of the argument is the linear map
   A: (X_R)^* -> (X^*)_R,    (A g)(x) = g(x) - i g(i x),
which is a real-linear isometry with inverse f |-> Re f. To check: A g is
complex-linear because
   (A g)(i x) = g(i x) - i g(i (i x)) = g(i x) + i g(x) = i (g(x) - i g(i x))
              = i (A g)(x).
And ||A g|| = ||g||: for any x in the unit ball and any phase theta, the real
part of e^{i theta}(A g)(x) equals g(cos(theta) x + sin(theta) i x), and
||cos(theta) x + sin(theta) i x|| <= ||x||; maximizing over theta gives
|A g(x)| <= ||g|| ||x||, and conversely |g(x)| <= |A g(x)|. So A is a real-
linear isometry.

Apply the evaluation criterion (Proposition 2) to the real space X_R. This
produces a real closed infinite-dimensional E_0 subset (X_R)^* with norm-
separable real evaluation image. Transport by A: let E = A E_0, a real closed
infinite-dimensional subspace of (X^*)_R. We now consider the complex-valued
real-linear evaluations on E,
   e_x: E -> C,  e_x(f) = f(x),  x in X.
Under A, e_x equals the difference e_x^{real} of A^{-1} and i e_{i x}^{real}:
   (A g)(x) = g(x) - i g(i x).
So e_x is a bounded real-linear combination of the real evaluations at x and
at i x, both of which live in the separable set R_{E_0}(X_R). Hence
{e_x : x in X_R} is norm separable as a set of bounded real-linear maps E -> C.

The same conclusion holds for evaluations on i E, because evaluation at x on
i E equals evaluation at i x on E, up to a factor of i in the argument and a
proper linear congruence.

We need a genuinely complex closed infinite-dimensional subspace H of (X^*)_R
on which the same separable-evaluation phenomenon holds. This is where the
real operator
   q: i E -> (X^*)_R / E,   q(w) = w + E,
enters. It has two cases.

Case 1: q is NOT strictly singular. Then there are a closed infinite-dimensional
W subset i E and a c > 0 with dist(w, E) >= c||w|| for every w in W. Since
W subset i E, the complex rotation lands in E: i W subset i(i E) = -E = E.
Define the real vector space H = W + i W, whose defining sum we now justify as
direct.

For w, v in W, since i v belongs to E and W has distance at least c||w|| from
E, we get ||w + i v|| >= dist(w + i v, E) = dist(w, E) >= c||w||. Combined with
the triangle inequality we get the two coordinate bounds
   ||w|| <= c^{-1} ||w + i v||,
   ||v|| <= (1 + c^{-1}) ||w + i v||.
These make the displayed real decomposition H = W + i W direct, make H a
closed subspace of (X^*)_R, and make the two real coordinate projections
H -> W bounded.

Now H = W + i W is closed under multiplication by i: i(w + i v) = -v + i w,
with -v in W and i w in i W. So H is a complex subspace of (X^*)_R.

Separable evaluations on H. Every complex-valued real-linear evaluation e_x
on H is determined by its two coordinate projections e_x(w) and e_x(i v), and
those lie in the separable sets of real evaluations on W and i W respectively.
The coordinate projections are bounded, so combinations of separable sets are
separable. Hence {e_x|_{H} : x in X} is a norm-separable set of real-linear
maps H -> C. The map x |-> e_x is complex-linear in x, so this same set,
viewed as a set of complex-linear maps on the complex space H, is norm
separable.

Apply the complex form of Proposition 2 to X and the complex closed infinite-
dimensional subspace H subset X^*. The hypothesis of (2) is satisfied, so X
has a separable infinite-dimensional complex quotient. This finishes Case 1.

Case 2: q IS strictly singular. This is the harder case, where no
infinite-dimensional chunk of iE sits at positive distance from E; we must
manufacture the complex structure using a small perturbation argument.

Fix a sequence of positive numbers eps_n with sum_n eps_n < 1/40; we will
also require each eps_n <= 1/40. We build vectors f_n in E and g_n in E by
induction.

At stage n we will have chosen f_1, ..., f_{n-1} and g_1, ..., g_{n-1}, and
finite sets D_1, ..., D_{n-1}, each D_m a 1/2-norming set in the unit ball of
X (as a real Banach space, but with complex values on it) for the COMPLEX span
of f_1, ..., f_m inside E. Let
   M_n = { m in E : m(d) = 0 for every d in D_1 union ... union D_{n-1} }
This is the kernel of finitely many real-linear conditions (each m(d) = 0 is
two real equations), so M_n is closed finite-codimensional, hence closed
infinite-dimensional. Therefore i M_n is a closed infinite-dimensional
subspace of i E. Restrict q: iE -> (X^*)_R/E to i M_n. Since q is strictly
singular on i E and restrictions remain strictly singular, Lemma 10 provides
a closed infinite-dimensional N subset i M_n such that ||q|_N|| <= eps_n / 2.
Take a unit vector i f_n in N (so f_n in M_n with ||f_n|| = 1); then
   dist(i f_n, E) <= (eps_n / 2)||i f_n|| = eps_n / 2.
Choose g_n in E with ||g_n - i f_n|| < eps_n / 2. Set D_n to be a 1/2-norming
set in the unit ball of X for the complex span of f_1, ..., f_n. This
completes stage n.

Observation: for m < n, the vector f_n lies in M_m+1 and hence annihilates
D_m. Combined with the norming property of D_m, the hypotheses of Lemma 1
(complex scalars, a = 1, b = 1 + 1/40) hold. So (f_n) is a complex basic
sequence with prefix projections of norm at most 2 and basis coefficient
functionals f_n^# of norm at most 4.

The operator L. Let H = closed complex span{f_n : n >= 1} inside E. On finite
complex sums we define a real-linear map
   L( sum_n (a_n + i b_n) f_n )  =  sum_n a_n f_n + sum_n b_n g_n,  a_n, b_n in R.
This is finite-sum defined and lands in E (since f_n and g_n lie in E, closed
under real linear combinations). Define K = L - I on finite sums. Straight
computation gives
   K( sum_n (a_n + i b_n) f_n ) = sum_n b_n (g_n - i f_n)
                                 = sum_n Im( f_n^#( sum_i (a_i + i b_i) f_i ) ) (g_n - i f_n).
So K = sum_n Im( f_n^#(.) ) (g_n - i f_n) as an infinite series, and its N-th
partial sum K_N is a finite-rank real-linear operator. Since
   ||K x - K_N x|| <= 4 sum_{n > N} ||g_n - i f_n|| ||x||
                   <= 4 sum_{n > N} eps_n ||x|| -> 0,
the partial sums converge uniformly and K extends to a bounded real-linear
operator on H, itself the norm limit of finite-rank operators K_N.

Where L goes. Since L maps finite sums into E and E is closed, L extends to
a bounded map L: H -> E with L(H) subset E. (Equivalently, L is the norm
limit of finite-dimensional restrictions, each landing in E.)

Separable evaluations for H. For x in X and h in H, let e_x(h) = h(x) be the
evaluation at x, a bounded real-linear map H -> C.

   {e_x L : x in X} = { (e_x|_{L(H)}) composed with L : x in X }.
Since L(H) subset E and R_E(X) is norm separable (the positive-transfer
setup), the evaluations on L(H) are contained in a separable set. Composing
with the bounded L keeps separability. So {e_x L : x in X} is norm separable.

   {e_x K : x in B_X} is totally bounded.
For each N, K_N has finite rank with image inside the finite-dimensional real
space V_N = span{g_n - i f_n : n <= N} subset E. For x in B_X, the bounded
real-linear map e_x K_N is determined by the values x restricted to V_N, which
range over a bounded subset of the finite-dimensional dual (V_N)^*. Bounded
subsets of finite-dimensional spaces are totally bounded. So {e_x K_N : x in
B_X} is totally bounded. And
   sup_{x in B_X} ||e_x K - e_x K_N|| <= ||K - K_N|| -> 0.
A uniform limit of totally bounded sets is totally bounded, so {e_x K : x in
B_X} is totally bounded.

Combine. On the unit ball B_X, we have e_x = e_x L - e_x K. The first set is
separable, the second is totally bounded (hence separable). Their difference
is separable. Dilating to all of X preserves separability. So
   {e_x|_{H} : x in X}
is norm separable as a set of complex-linear functionals on H (we checked
e_{ix} = i e_x earlier, so complex linearity is inherited). Apply the complex
form of Proposition 2 to X and the complex closed infinite-dimensional
subspace H subset X^*. Conclusion: X has a separable infinite-dimensional
complex quotient. This finishes Case 2 and hence Proposition 11.   []

3.3  A finite sum cannot acquire a quotient from nothing.

Before proving the counterexample direction we need a routine additivity
statement for the property "has no separable infinite-dimensional quotient".

LEMMA 12 (finite sum). If neither of two real Banach spaces X_1, X_2 has a
separable infinite-dimensional quotient, then their direct sum has none.

PROOF. Give Y = X_1 + X_2 the norm ||(x_1, x_2)|| = max(||x_1||, ||x_2||). Its
dual in the dual norm is Y^* = X_1^* +_1 X_2^* (the l_1 sum because the max
norm is dual to the l_1 norm on the dual pair). Precisely, every element of
Y^* is a pair (f, g) with f in X_1^*, g in X_2^*, and ||(f, g)|| = ||f|| + ||g||.

Suppose Y had such a quotient. By the evaluation criterion (Proposition 2),
there is a closed infinite-dimensional F subset Y^* with R_F(Y) norm separable.
Let p_j: F -> X_j^* be the coordinate operators p_1(f, g) = f and p_2(f, g) = g.

Case (a): p_1 is not strictly singular. Then some closed infinite-dimensional
G subset F maps injectively with a lower bound under p_1; p_1|_G identifies G
with a closed infinite-dimensional H subset X_1^*. For x in X_1, evaluation at
x on H is evaluation at (x, 0) in Y on F, restricted to G, and composed with
(p_1|_G)^{-1}. The composed image of (p_1|_G)^{-1} o restriction is a bounded
image of the separable set R_F(Y). Hence R_H(X_1) is norm separable. By
Proposition 2, X_1 has a separable infinite-dimensional quotient, contrary to
the hypothesis.

Case (b): p_1 is strictly singular. By Lemma 10 with eps = 1/2, there is a
closed infinite-dimensional G subset F with ||p_1|_G|| <= 1/2. For g in G, on
the one hand g = (p_1 g, p_2 g) so ||g|| = ||p_1 g|| + ||p_2 g|| (l_1 norm);
on the other hand ||p_1 g|| <= ||g|| / 2. Therefore ||p_2 g|| >= ||g|| / 2,
and p_2|_G identifies G with a closed infinite-dimensional H subset X_2^*. The
same evaluation-separability argument as in Case (a) gives a separable
infinite-dimensional quotient of X_2, contra hypothesis.

Either case is impossible. So Y has no separable infinite-dimensional
quotient, and Lemma 12 holds.   []

3.4  Real and complex versions are equivalent for counterexamples.

COROLLARY 13 (complexification). Let X be a real Banach space. Its
complexification X_C = X + i X, with the norm
   ||x + i y||_C  =  sup_{theta in R} ||cos(theta) x - sin(theta) y||,
is a complex Banach space. It satisfies
   max(||x||, ||y||)  <=  ||x + i y||_C  <=  ||x|| + ||y||  <=  2 max(||x||, ||y||).
Its underlying real space is isomorphic to X +_inf X. If X is a real
counterexample (no separable infinite-dimensional quotient), then X_C is a
complex counterexample.

PROOF. The complex structure: i(x + i y) = -y + i x, giving absolute
homogeneity over C. The triangle inequality follows from that of X (it holds
for each value of theta separately and then for the supremum). The displayed
norm equivalence comes from theta = 0 giving ||x||, theta = pi/2 giving ||y||,
and the triangle inequality in X giving the upper bound. Since ||.||_C is
equivalent to the max norm, X_C is complete and its underlying real space is
isomorphic to X +_inf X.

Now suppose X_C had a separable infinite-dimensional COMPLEX quotient. Passing
to underlying real spaces, X_C^R = X +_inf X would acquire a separable
infinite-dimensional REAL quotient. But X +_inf X = X_1 + X_2 with X_1 = X_2 =
X, and neither summand has a separable infinite-dimensional quotient (X is a
counterexample). Lemma 12 then forbids such a quotient, contradiction. So X_C
is a complex counterexample. This proves Corollary 13.   []

Proposition 11 and Corollary 13 together reduce the complex version of both
the positive and the negative implications to the real version, plus the two
statements in between. This completes Part 3.


==============================================================================
PART 4.  BUILDING A TRICKY NORMED SPACE E
==============================================================================

4.0  What we are going to build, and why it is complicated.

Parts 4 through 8 assume CH and build a single real Banach space X with NO
separable infinite-dimensional quotient. The strategy is:
   (step A) build a normed space E whose unit ball lives in c_{00}(omega_1),
            with E^* = E via a coordinate predual we control;
   (step B) equip E with a large supply of "path" functionals P in B_{E^*}
            that separate any infinite-dimensional closed subspace F of E by
            an uncountable margin;
   (step C) change the predual of E slightly, to a new space X whose dual is E,
            so that the path functionals MODULO the coordinate evaluations are
            exactly the evaluations of X on E; then every separable F subset E
            fails to have separable evaluations from X, blocking all
            quotients by the evaluation criterion (Proposition 2).

Step A and the early part of step B are in this Part 4. Everything depends on
one coordinate set Gamma and a colouring.

4.1  The coordinate set, colors, ranges, intervals, projections.

Let Gamma = omega_1, the first uncountable ordinal. Partition Gamma into
countably many disjoint unbounded subsets C_0, C_1, C_2, ... For alpha in
Gamma, col(alpha) is the color k with alpha in C_k.

Ordinal range of a finite nonempty A subset Gamma: the interval
[min A, max A]. Color range: the interval [min col(A), max col(A)] of integer
colors. Distinct finite sets A, B are successive if every ordinal in A is
smaller than every ordinal in B or vice versa. They are mixed-successive if
their ordinal ranges are successive AND their color ranges are successive.

Ordinal intervals: convex subsets of Gamma, including the whole Gamma and the
empty set. Color intervals: convex subsets of {0, 1, 2, ...}. A rectangle is
the intersection of an ordinal interval with a color interval (viewed as the
set of coordinates whose color lies in that color interval). These are the
projection sets used in the construction. For a projection set A, write P_A
for the coordinate projection acting on both c_{00}(Gamma) and its dual.

4.2  The families and their exponents.

There is one pure family for each k >= 0, and one mixed family, denoted by *.

Pure family k:
   s_k  = k + 2,
   r_k  = s_k' = s_k / (s_k - 1),
   s_{k+1}' <= q_k < s_k'.
Mixed family *:
   s_*  = 2,   r_* = 2,   s_1' <= q_* < 2.
Parameters of different families are chosen independently. Whenever one family
is fixed, we suppress its subscript: s, r, q. What matters is the exponent
chain
   1 < q < r = s',   q' > r,   1/q' < 1/s,
which we checked numerically in the choices above: s = k+2 >= 2, r <= 2 <= s,
q < s' = r, so q' > s' = r, and 1/q' < 1/s.

The norm. Let c_{00}(Gamma) be the space of finitely supported real scalar
families x = (x(alpha)) on Gamma. We write e_alpha for the coordinate vector
with a 1 at alpha and 0 elsewhere, and e_alpha^* for the coordinate functional
x |-> x(alpha). The norm ||.|| on c_{00}(Gamma) will be defined in 4.6 by a
supremum over a large but countable set of functionals. We write E for its
completion. The coordinate functionals extend to E, and
   X_0 = closed span of {e_alpha^* : alpha in Gamma} subset E^*.
Two long-term goals of the construction:

   (GOAL A) The canonical evaluation map E -> X_0^* is an isometric
            isomorphism. (This will be Proposition 19 in 4.7.)

   (GOAL B) For every family t (pure k or mixed), the set of all infinite
            paths of that family defines functionals P in B_{E^*}; and finite
            combinations of distinct such paths of the SAME family satisfy an
            l_{q_t} bound modulo X_0:

              || sum_P a_P Q P ||_{E^* / X_0}  <=  || (a_P) ||_{q_t},

            where Q: E^* -> E^*/X_0 is the quotient map. (Part 5 supplies
            this.)

   (GOAL C) Every infinite-dimensional closed F subset E has, in a single
            family t, an uncountable set of path restrictions P|_F separated
            by a positive distance. (Part 6 and Part 7 supply this.)

4.3  Parameters: sizes, weights, and depth.

We need three positive integer sequences per family: (L_j), (m_j), (d_j), all
strictly increasing. The quantities that run through every estimate are
   theta_j = L_j^{1/r} / m_j,
   c_0     = sum_{j>=1} theta_j,
   B_j     = 2 sum_{h<j} L_h.

LEMMA 14 (choice of parameters). For each family there are strictly increasing
positive integer sequences (L_j), (m_j), and positive integers (d_j), such
that, with the above notation, all of the following hold:

   (P1)  c_0 < 1/8,     sum_{j >= J} theta_j <= 4 theta_J,
         sum_{j >= 1} 1/m_j < 1/8;
   (P2)  log(L_j / m_j) / log(L_j)  ->  1/s   as j -> infinity;
   (P3)  (1/8)^{d_j} <= theta_j,
         (1 + B_j)^{d_j} (1 + B_j + L_j^{1/q'}) <= L_j / m_j.

In particular L_j / m_j -> infinity.

PROOF of (P1), (P2). Put eta_j = (2^{-10-j})^r and choose L_j =
floor(eta_j m_j^r). By taking m_j large, arrange
   eta_j/2 <= L_j / m_j^r <= eta_j.
Then
   theta_j = L_j^{1/r} / m_j lies in [ 2^{-1/r} 2^{-10-j} , 2^{-10-j} ].
So theta_j <= 2^{-10-j}. Then c_0 <= sum_j 2^{-10-j} < 1/8, the sum of the
tail of theta from J is at most 2^{-10-J} (1 + 1/2 + 1/4 + ...) = 2^{-9-J}
<= 4 theta_J (by the same bound), and by increasing m_j a bit more we ensure
1/m_j < 2^{-j-4} so that sum_j 1/m_j < 1/8. This proves (P1).

For (P2), note that theta_j = L_j^{1/r} / m_j and therefore
   L_j / m_j = theta_j L_j^{1 - 1/r} = theta_j L_j^{1/s}.
Taking logarithms,
   log(L_j/m_j) / log L_j = 1/s + log(theta_j) / log L_j.
Since theta_j is bounded above and below by 2^{-10-j} times positive constants
and L_j -> infinity, |log(theta_j)| / log L_j -> 0. Choose m_j further to make
|log(theta_j)| / log L_j < 1/j, which gives (P2). This positive limit also
gives L_j / m_j -> infinity.

PROOF of (P3). The integers d_j will be chosen right before choosing m_j, so
at step j the numbers B_j = 2 sum_{h<j} L_h and d_j are already fixed
quantities. Choose d_j first so large that (1/8)^{d_j} <= 2^{-1/r} 2^{-10-j}
<= theta_j, giving the first inequality. Now choose m_j so large that the
second inequality holds. Indeed
   L_j / m_j = theta_j L_j^{1/s}
and theta_j lies between 2^{-1/r} 2^{-10-j} and 2^{-10-j}. Also 1/q' < 1/s.
So L_j^{1/s} / L_j^{1/q'} = L_j^{1/s - 1/q'} -> infinity because 1/s - 1/q' >
0. This means L_j/m_j eventually dominates any fixed power of L_j; the
left-hand side of the second inequality in (P3) is at most (1+B_j)^{d_j}
times a fixed polynomial in L_j, of degree that grows with d_j but is fixed
once j is fixed, so making m_j large forces the inequality to hold.

Increase m_j further to make both sequences strictly increasing and to make
|log theta_j| / log L_j < 1/j. This completes the choices. Lemma 14 holds.
   []

4.4  Coherent finite coordinate closures.

To encode a rational functional's support by ORDER POSITIONS without recording
its actual ordinal labels, we need a family of coherent finite sets. The next
lemma supplies them, following the position-coding method of Argyros,
Lopez-Abad and Todorcevic (J. Funct. Anal. 2005, Sections 2.3-2.4). We prove
the exact coherence we will need.

LEMMA 15 (coherent finite closures). For every beta < omega_1, there is a
sequence of finite sets F_p(beta), p >= 1, such that:
   (a) F_p(beta) subset [0, beta] contains beta;
   (b) F_p(beta) subset F_{p+1}(beta), and the union_p F_p(beta) is dense in
       [0, beta] in the sense that it contains every ordinal below beta;
   (c) for every p and every alpha in F_p(beta),
          F_p(alpha) = F_p(beta) cap [0, alpha]              (coherence).
Consequently, whenever two closures F_p(beta) and F_p(gamma) (same p) share a
common ordinal alpha, their ordered initial segments through alpha coincide as
ordered sets.

PROOF. Work by transfinite induction on beta.

beta = 0: set F_p(0) = {0} for all p >= 1.

Successor step beta = gamma + 1: given F_p(gamma), set F_p(beta) =
F_p(gamma) union {beta} for every p. Coherence at alpha in F_p(beta): if
alpha = beta then [0, alpha] contains all of F_p(beta); if alpha in
F_p(gamma) then apply the inductive hypothesis at alpha and use that
F_p(beta) cap [0, alpha] = F_p(gamma) cap [0, alpha]. Nestedness is inherited.

Limit step. Suppose beta is a nonzero limit ordinal. Fix an increasing cofinal
sequence (a_i) of ordinals below beta (this exists because omega_1 is a limit
ordinal, and we may take any countable cofinal sequence below beta). Recursively
choose strictly increasing sequences (alpha_i) below beta and (p_i) of integers
starting with p_0 = 1, so that:
   - alpha_i is increasing and cofinal in beta (alpha_i -> beta),
   - a_j <= alpha_i for every j <= i,
   - F_{p_i}(alpha_i) contains alpha_{i-1} and a_0, ..., a_i.
This is possible by (b) at each stage. For p in [p_i, p_{i+1}) set
   F_p(beta) = F_p(alpha_i) union {beta}.

Check nestedness at the switch p_{i+1}: we have F_{p_{i+1}-1}(beta) =
F_{p_{i+1}-1}(alpha_i) union {beta}, and F_{p_{i+1}}(beta) =
F_{p_{i+1}}(alpha_{i+1}) union {beta}. By coherence at alpha_i applied to
F_{p_{i+1}-1}(alpha_{i+1}) (which contains alpha_i by the choice of p_{i+1}):
   F_{p_{i+1}-1}(alpha_i) = F_{p_{i+1}-1}(alpha_{i+1}) cap [0, alpha_i]
                        subset F_{p_{i+1}}(alpha_{i+1}).
So F_{p_{i+1}-1}(beta) subset F_{p_{i+1}}(beta). Nestedness holds.

Property (a): F_p(beta) contains beta by construction, and F_p(beta) subset
[0, beta] because F_p(alpha_i) subset [0, alpha_i] subset [0, beta] and
beta is the largest element.

Property (b): each a_j is eventually in F_p(beta) once p >= p_j, so every
ordinal below beta is in the union over p.

Property (c): take alpha in F_p(beta). If alpha = beta, coherence is
vacuous. Otherwise alpha in F_p(alpha_i) for some i, and by inductive
coherence at alpha_i:
   F_p(alpha) = F_p(alpha_i) cap [0, alpha].
And
   F_p(beta) cap [0, alpha] = (F_p(alpha_i) union {beta}) cap [0, alpha]
                            = F_p(alpha_i) cap [0, alpha]  (as alpha < beta).
So F_p(alpha) = F_p(beta) cap [0, alpha], proving (c).

The "initial segments through a common alpha" statement follows by applying
(c) to each of F_p(beta) and F_p(gamma) and using that the intersection with
[0, alpha] is (by coherence) the same as F_p(alpha) on each side, an ordered
set. This proves Lemma 15.   []

Define
   rho(alpha, beta) = min{ p : alpha in F_p(beta) }    for alpha <= beta (>= 1).
For a finite nonempty A subset Gamma, define
   max_rho(A) = max{ rho(alpha, beta) : alpha, beta in A, alpha <= beta }.
Then A subset F_p(max A) whenever p >= max_rho(A); so the closure at the
maximal element captures the whole set at that stage p.

Position alignment. We will use one precise form of "position equality". Fix
p, closures F_p(beta) and F_p(gamma), and suppose both contain a common ordinal
alpha. Let A, B be arrays on these ordered closures, supported on coordinates
of Gamma, such that at every ORDER POSITION of the closure the array agrees:
A(k) = B(k) where k is the k-th smallest ordinal in F_p(beta) for A and again
the k-th smallest ordinal in F_p(gamma) for B. Suppose further that A is
supported strictly before alpha (all nonzero A(alpha') have alpha' < alpha).
Then A and B define exactly the SAME finitely supported function on Gamma.

Why: positions through alpha coincide as ordered sets by Lemma 15(c); if the
k-th position is alpha in both closures, then we already have A(alpha) = B(alpha)
by agreement of positions. For a position strictly above alpha, A's entry is
zero (A is supported below alpha); so B's entry is also zero. So B is supported
below alpha and coincides with A at every coordinate.

The observation to keep in mind: equality of position codes alone does not
assert equality of ordinal supports. The common coordinate alpha is the extra
input; and the "supported below alpha" hypothesis rules out the arrays having
distinct actual ordinals for later positions.

4.5  Type I / Type II functionals, paths, and the norming sets K_k and K.

All norming functionals below are finitely supported rational arrays on Gamma.

Type I expression of weight j. In a fixed family, this is a functional of the
form
   phi  =  (1 / m_j) sum_{h=1}^{d} g_h,     1 <= d <= L_j,
where the g_h are nonzero members of an EARLIER stage of the relevant norming
set, and their supports are successive in the pure family case, or
mixed-successive in the mixed family case. The weight is the integer j.

Path in one family. A finite path is a list (phi_1, ..., phi_l) of nonzero
Type I pieces together with
   - declared integer weights j_1 < j_2 < ... < j_l,
   - integer metadata p_1 < p_2 < ... < p_l,
chosen so that
   p_i >= j_i
   p_i >= max_rho( union_{h <= i} support(phi_h) ).
Here max_rho was defined in 4.4 from the coherent closures F_p(beta).

The coding map sigma. The code of the prefix through i records:
   - all j_h and p_h for h <= i,
   - the zero-filled arrays of all phi_h, h <= i, at the order positions of
     F_{p_i}(beta_i), where beta_i = max of the union of supports through i.
There are countably many possible codes: integer sequences of bounded length
together with rational arrays on finite coordinate sets, up to the specific
ordinal labels which are NOT recorded. Fix once and for all, in each family,
an injection
   sigma : {codes} -> positive integers
such that sigma(code) > the final metadata entry of the code. Such an injection
is obtained by enumerating all codes and choosing unused sufficiently large
integers.

Path rule. Along a path:
   first weight j_1 is arbitrary;
   the next weight obeys j_{i+1} = sigma( code of the prefix through i ).

Two remarks. (i) The path is more than the sum of its pieces: it carries its
declared weights, metadata, and the coding. All arguments MUST refer to the
specific expression of the path, not merely to the point values. (ii) All
weights along a path are strictly increasing, because sigma takes positive
integer values that exceed the last metadata (which is at least the last
weight).

Crops. A pure path is a list of pure Type I pieces in a family k; a crop of a
pure path means restriction of its SUM to an ordinal interval. A mixed path is
a list of Type I pieces with mixed-successive supports; a crop of a mixed path
means restriction of its sum to a rectangle. A weight i is ACTIVE in a cropped
path when the i-th Type I piece remains nonzero after the crop. Cropping does
not change the underlying path data (weights, metadata, coding); path rules
always refer to the uncropped pieces.

The norming sets K_k (pure). For each k >= 0, start K_k with:
   - the zero functional,
   - +/- e_alpha^* for alpha in C_k.
Enlarge K_k in finite stages using the following two pure operations.

   (OP-I) Type I expressions of weight j whose children lie in earlier stages.

   (OP-II) Type II expressions of the form
        sum_{b=1}^{h} a_b P_{I_b} ( sum_{i=1}^{l_b} phi_{b,i} ),
      with a_b in Q (rationals), sum_b |a_b|^q <= 1, where:
        each (phi_{b,i})_{i=1}^{l_b} is a finite path in family k;
        the Type I children of all its pieces lie in earlier stages of K_k;
        P_{I_b} is the ordinal-interval crop for its piece list;
        the cropped paths (P_{I_b} phi_{b,i})_{i} for different b have
        pairwise DISJOINT active weight sets.

Empty cropped terms are discarded. Because the construction is in finite
stages, every member of K_k has at least one designated expression tree.

The norming set K (mixed). Start K with all members of all K_k (as "terminal"
functionals). Enlarge K in finite stages using the same two operations with
the MIXED parameters s_*, r_*, q_*, with mixed-successive supports on the
children of Type I pieces, and with rectangle crops in Type II expressions.
Children in mixed rules lie in earlier stages of K.

Norm. For x in c_{00}(Gamma) define
   ||x||  :=  sup_{f in K} |f(x)|.
This is a seminorm a priori. Lemma 16 below shows it is a genuine norm, that
its completion E has the properties we need, and that the pure and full norms
coincide on each color C_k.

4.6  The norm is well behaved.

LEMMA 16 (norm and projections). The supremum defining ||.|| is finite and
positive definite, so it is a norm on c_{00}(Gamma). In the completion E:
   (a) each coordinate vector e_alpha has norm exactly one;
   (b) projections P_A onto ordinal intervals and onto rectangles are
       contractive;
   (c) every vector of E has countable support and is a norm limit of its
       finitely supported truncations;
   (d) the pure norm induced by K_k on the space c_{00}(C_k) agrees with the
       full norm ||.|| on the coordinate subspace spanned by C_k.

PROOF of (b), crop stability. Fix a member f of K_k (or K) and a projection
set A (an ordinal interval for pure, or a rectangle for mixed). We claim P_A f
again lies in K_k (or K) at the SAME stage. For a pure terminal, crop gives a
terminal (or zero). For a pure Type I piece, distribute the crop to the
children: P_A(sum g_h) = sum P_A g_h, and then discard any zero children. The
children that survive still have successive (or mixed-successive) supports,
and the surviving children are crops of the original children of earlier
stages. For a pure Type II expression, intersect each existing crop with A;
the paths and their codings are unchanged and the active weight sets shrink.
This change only removes active weights, so the l_q bound on the coefficients
and the disjointness of the active weights survive. The same argument works
for the mixed family with rectangles. So P_A maps K into K at the same stage,
and consequently |(P_A f)(x)| <= ||x|| for all f in K and x in c_{00}(Gamma);
by symmetry of K this gives ||P_A x|| <= ||x||.

PROOF of (a) easy bounds. Every coefficient of every member of K_k or of K
has absolute value at most one. At a pure Type I node, disjointness of the
children gives the stronger bound 1/m_j on each coefficient of that piece. At
a pure Type II node, a given coordinate meets at most one piece of each path,
and contributions from different paths have distinct active weights; summing
their absolute values gives at most sum_j 1/m_j < 1. Induction on the
construction stage establishes both bounds in the pure families and then in
the mixed family. This shows
   ||x||_infinity <= ||x|| <= ||x||_1,   x in c_{00}(Gamma).
The lower bound makes ||x|| positive for x != 0, so ||.|| is a norm. The upper
bound makes each coordinate functional e_alpha^* continuous (Lipschitz of norm
at most 1).

PROOF of (c). By (b), each P_A is contractive. For a vector x of E (a
completion of c_{00}), fix eps > 0 and pick a finite approximation y = sum_j
c_j e_{alpha_j} with ||x - y|| < eps. The support of y is finite (the
alpha_j). Since x = y + (x - y) and ||(x - y)|| < eps, its "support outside
the finite set S = {alpha_j}" has norm at most eps by crop contractivity of
Gamma - S. Letting eps -> 0 through a sequence gives countable support
(any eps-approximation has a finite support S, and unioning over a sequence
of approximations gives a countable supporting set). Moreover, ||x|| = lim of
||truncations to increasing finite sets||, giving (c).

PROOF of (d). We claim the factor set identity
   {f |C_k : f in K}  subset  absconv(K_k)
where absconv(K_k) is the absolutely convex hull of K_k (allowing zero). It
suffices to check at terminals and to induct on the construction stage. At a
pure terminal, f | C_k is in K_k if f itself is in K_k, and zero otherwise. At
a MIXED Type I node, at most one child can meet C_k (children have
mixed-successive color ranges); the restriction to C_k is then a scalar
multiple (1/m_j) of the surviving child restricted to C_k, still in K_k by
induction. At a MIXED Type II node, at most one piece of each path meets C_k,
and at most one child of that piece meets C_k; by induction the restriction is
an absolutely convex combination of pure functionals in K_k whose total
coefficient mass is at most
   a_b for that piece, summed over the finitely many paths with |a_b| summing
   at most sum_j 1/m_j < 1
(since each path contributes 1/m_j once, and the coefficients a_b of different
paths are already l_q-bounded). So the restriction lies in absconv(K_k). The
other direction, K_k subset K, is immediate from the definition. So the pure
norm given by K_k and the full norm given by K agree on c_{00}(C_k). This
completes the proof of Lemma 16.   []

4.7  Coordinate upper estimate on each color.

We now show that the coordinate vectors of each color C_k, weighted by any
l_{s_k} sequence, are bounded by that sequence's norm. This is the first of
the three global goals (GOAL A in older notation is separate; this is the
coordinate estimate that helps GOAL B).

LEMMA 17 (coordinate upper estimate). For each k and every finitely supported
real family (b_alpha) with alpha running over C_k,
   || sum_{alpha in C_k} b_alpha e_alpha ||  <=  || (b_alpha) ||_{s_k}.
Consequently, the infinite series sum_{alpha in C_k} b_alpha e_alpha
converges in E whenever (b_alpha) lies in l_{s_k}(C_k).

PROOF. We work in the pure family k. Fix a coordinate coefficient functional
f = sum_alpha c_alpha e_alpha^*, and define its COEFFICIENT l_r norm by
   || f ||_{coef r} = ( sum_alpha |c_alpha|^r )^{1/r}.
We claim that every member of K_k has || f ||_{coef r} <= 1. We prove this by
induction on the stage of construction.

Terminal stage. e_alpha^* has one coefficient equal to 1, so its coefficient
l_r norm equals 1. The zero functional has coefficient l_r norm 0. Positive.

Type I stage. Let phi = (1/m_j) sum_{h=1}^d g_h, with the g_h nonzero and of
earlier stages, having successive supports. Then
   || phi ||_{coef r}  <=  (1/m_j) ( sum_{h=1}^d || g_h ||_{coef r}^r )^{1/r}
                        <=  (1/m_j) d^{1/r}  <=  L_j^{1/r} / m_j  = theta_j.
Here we used induction on the children and the disjointness of their supports.

Type II stage. Let
   phi  =  sum_{b=1}^{h} a_b P_{I_b} ( sum_{i=1}^{l_b} phi_{b,i} )
with a_b in Q, sum_b |a_b|^q <= 1, and the cropped paths having disjoint active
weight sets. Write c_b for the coefficient vector of the b-th cropped path and
t_b = || c_b ||_{coef r}. Induction bounds the coefficient vector of each
phi_{b,i} by theta_{j_{b,i}}, so the cropped path has coefficient vector equal
to the sum of those phi_{b,i} with j_{b,i} active in the crop. Therefore
   t_b^r  <=  sum_{i active} theta_{j_{b,i}}^r.
Now apply Minkowski's inequality over the index b:
   || phi ||_{coef r}  <=  sum_{b=1}^{h} |a_b| t_b          (Minkowski).
Then apply Holder's inequality with the conjugate pair (q, q'):
   sum_b |a_b| t_b  <=  || (a_b) ||_q  || (t_b) ||_{q'}  <=  || (t_b) ||_{q'}.
So far we have || phi ||_{coef r} <= || (t_b) ||_{q'}. Since q' > r, the
monotonicity of l_p norms gives || (t_b) ||_{q'} <= || (t_b) ||_r. And
   || (t_b) ||_r^r  =  sum_b t_b^r  <=  sum_b sum_{i active in b} theta_{j_{b,i}}^r.
The sets of active j across different b are pairwise disjoint, so summing over
b and over active i is the same as summing over the union of those weight sets,
which is at most the sum over all j:
   sum_b t_b^r  <=  sum_j theta_j^r.
Finally, theta_j <= 2^{-10-j} < 1 and r > 1, so theta_j^r <= theta_j, and
   ( sum_j theta_j^r )^{1/r}  <=  ( sum_j theta_j )^{1/r}  <=  c_0^{1/r}  < 1.
So each member of K_k has coefficient l_r norm < 1, as required.

Conclusion. For x = sum_{alpha in C_k} b_alpha e_alpha with b finitely
supported, and any f in K_k with coefficients c_alpha,
   | f(x) |  =  | sum_{alpha in C_k} c_alpha b_alpha |
             <=  || (c_alpha) ||_{s_k'} || (b_alpha) ||_{s_k}
             <=  || (b_alpha) ||_{s_k}.
We used s_k' = r_k, so the coefficient l_{s_k'} norm equals the coefficient
l_r norm just bounded by 1. Taking the supremum over f in K_k yields the
claimed upper estimate.

Finally, apply the estimate to finite tails: if (b_alpha) is in l_{s_k}, then
the tails of the series have l_{s_k}-norms going to zero, so the partial sums
are Cauchy in E and converge there. Lemma 17 is proved.   []

4.8  The coordinate predual: E is X_0^*.

The point of building all this structure is that we can control the coordinate
predual X_0 tightly: the canonical evaluation map E -> X_0^* is an isometric
isomorphism. We need it for both later parts (the path coset bound and the
change of predual in Part 8).

PROPOSITION 18 (coordinate predual). Let
   X_0  =  closed span of {e_alpha^* : alpha < omega_1}  in E^*.
Then the canonical evaluation map
   ev: E -> X_0^*,        (ev x)(f) = f(x) for f in X_0, x in E,
is an isometric isomorphism of Banach spaces.

PROOF.

ISOMETRY. Every f in K is a finite linear combination of coordinate
functionals, so f lies in X_0. By Lemma 16, ||x||_E = sup_{f in K} |f(x)|; so
each f in K has ||f||_{E^*} <= 1, i.e. K subset B_{X_0} (the unit ball of
X_0 in its E^*-norm). Conversely, for x in E and f in B_{X_0},
|f(x)| <= ||f||_{E^*} ||x||_E <= ||x||_E. Taking the supremum in f gives
sup_{f in B_{X_0}} |f(x)| <= ||x||_E. Together with K subset B_{X_0} and the
identity defining ||x||_E as the supremum over K, this yields the isometry
   ||x||_E  =  sup_{f in B_{X_0}} |f(x)|  =  ||ev(x)||_{X_0^*},   x in E.
Injectivity: if ev(x) = 0 then f(x) = 0 for every coordinate f = e_alpha^*, so
every coefficient x(alpha) = 0; since x has countable support and is a limit
of finitely supported vectors, x = 0.

SURJECTIVITY. Fix g in X_0^*. Set a_alpha = g(e_alpha^*) for alpha in
omega_1. We construct, for every gamma <= omega_1, a vector x_gamma in E whose
support lies in [0, gamma) and satisfies
   x_gamma(alpha) = a_alpha   for alpha < gamma,
   x_gamma(alpha) = 0         for alpha >= gamma,
by transfinite recursion. The key invariant is
   ||x_gamma|| <= ||g||                                    (PREFIX BOUND).
Indeed, for any finite f in K, the crop P_{<gamma} f is again in K at the
same stage by Lemma 16(b), so ||P_{<gamma} f||_{X_0} <= ||f||_{X_0} <= 1, and
   f(x_gamma) = g(P_{<gamma} f),   |f(x_gamma)| <= ||g|| ||P_{<gamma} f||_{X_0}
                                 <= ||g||.
Taking the supremum over f in K gives ||x_gamma|| <= ||g||.

Base and successor steps. x_0 = 0 (empty support). x_{gamma+1} = x_gamma +
a_gamma e_gamma. The invariant is preserved at each successor: every f in K
evaluates x_{gamma+1} at f(x_gamma) + a_gamma f(gamma) = g(P_{<gamma+1} f),
whose absolute value is at most ||g|| times ||P_{<gamma+1} f||_{X_0} <= ||g||.

Limit step: Cauchy bound. Let lambda be a limit ordinal and suppose all x_gamma
with gamma < lambda are constructed. Suppose (x_gamma)_{gamma < lambda} is NOT
norm Cauchy. Then there is delta > 0 and, recursively, successive intervals
[alpha_i, beta_i) inside [0, lambda) with
   v_i = x_{beta_i} - x_{alpha_i},   ||v_i|| >= delta.
Two cases.

Case 1: some color k dominates. That is, for some k and some
delta' > 0, infinitely many i satisfy ||P_{C_k} v_i|| >= delta'. For any
positive integer j, select L_j such v_i. By Lemma 16(d) (pure norm = full norm
on C_k) and the symmetry of K_k (a member f gives -f too), choose pure normers
g_i in K_k with
   g_i(P_{C_k} v_i) >= delta' / 2,
and supported in the ordinal interval [alpha_i, beta_i). We may crop as
needed: K_k is stable under ordinal crops. Choose j so large that the stages
of all these g_i are strictly smaller than weight j, and form the Type I
average
   phi  =  (1 / m_j) sum_{i=1}^{L_j} P_{[alpha_i, beta_i)} g_i.
The piece P_{[alpha_i, beta_i)} g_i is supported in the interval [alpha_i,
beta_i), and the intervals are successive, so the children have successive
supports and phi lies in K_k at weight j.

Let B > alpha_{L_j} be larger than all the beta_i and evaluate phi at x_B
(well-defined by the prefix). The prefix x_B restricted to [alpha_i, beta_i)
equals P_{C_k} v_i, so
   |phi(x_B)|  =  (1 / m_j) sum_{i=1}^{L_j} g_i(P_{C_k} v_i)
               >=  (1 / m_j) * L_j * delta' / 2   =  delta' L_j / (2 m_j).
On the other hand, phi in K_k subset B_{X_0} (with the crop to [0,B) still
inside K_k), so
   |phi(x_B)|  <=  ||g|| ||P_{<B} phi||_{X_0}  <=  ||g||,
because the crop of phi to [0,B) is still in K_k. Combined, this gives
   ||g||  >=  delta' L_j / (2 m_j).
Since L_j / m_j -> infinity (Lemma 14), the right side tends to infinity as
j -> infinity. But ||g|| is fixed. Contradiction.

Case 2: no color dominates. Then ||P_{C_k} v_i|| -> 0 for every k. We claim we
can pass to a subsequence and pick successive finite color intervals D_i with
   ||P_{color^{-1}(D_i)} v_i|| >= delta / 2.
Construction of D_i. After the preceding upper color cutoff c_{i-1} has been
fixed (with c_0 = -1), the finitely many projections P_{C_0} v_i, ...,
P_{C_{c_{i-1}}} v_i tend to zero, so choose the next v_i with
   sum_{k <= c_{i-1}} ||P_{C_k} v_i|| < delta / 4.
For that individual vector, P_{colors >= c_{i-1}+1} v_i = v_i minus the finite
color projections, so its norm is >= ||v_i|| - delta / 4 >= 3 delta / 4 (since
||v_i|| >= delta). By finite approximation and contractivity of the projection
P_{colors >= c} applied to the countable support of v_i, for large c_i we get
   ||P_{colors >= c_i} v_i|| < delta / 4.
So the intermediate color interval D_i = (c_{i-1}, c_i) captures the bulk:
   ||P_{color^{-1}(D_i)} v_i||  >=  ||P_{colors >= c_{i-1}+1} v_i||
                                  - ||P_{colors >= c_i} v_i||
                              >=  3 delta / 4 - delta / 4 = delta / 2.
Now take rectangle-cropped normers g_i in K with
   g_i( P_{[alpha_i, beta_i) cap color^{-1}(D_i)} v_i )  >=  delta / 4.
(The crops are legal because K is stable under rectangle crops.) Choose a
weight j larger than all stages of the g_i, and form the mixed Type I average
   phi  =  (1 / m_j) sum_{i=1}^{L_j} P_{[alpha_i, beta_i) cap color^{-1}(D_i)} g_i.
Children have mixed-successive supports (both ordinal intervals and color
intervals are successive in i). Evaluating at x_B for B > alpha_{L_j}:
   |phi(x_B)|  >=  delta L_j / (4 m_j).
Since phi is in K (hence B_{X_0}), the same argument as in Case 1 gives
   ||g||  >=  delta L_j / (4 m_j),
again impossible as j -> infinity.

Conclusion of the limit step. The prefix family (x_gamma)_{gamma < lambda} was
norm Cauchy. By completeness, it has a limit x_lambda with the prescribed
coefficients in [0, lambda). The bound ||x_lambda|| <= ||g|| persists by
continuity. So limits exist at all gamma <= omega_1, and the same
construction produces x_{omega_1} in E.

Terminal vector. The vector x_{omega_1} in E has x(alpha) = a_alpha for every
alpha (no upper bound). For any coordinate functional e_alpha^*,
   (ev(x_{omega_1}))(e_alpha^*) = e_alpha^*(x_{omega_1}) = a_alpha
                                  = g(e_alpha^*).
The two functionals agree on all e_alpha^*, hence on the closed span X_0 by
continuity, so ev(x_{omega_1}) = g. This proves surjectivity.

Combining isometry, injectivity and surjectivity: ev: E -> X_0^* is an
isometric isomorphism. Proposition 18 holds.   []


==============================================================================
PART 5.  INFINITE PATHS AND WEAK-CAUCHY BLOCK SEQUENCES
==============================================================================

5.0  What this part does.

An infinite path is an infinite list of Type I pieces with declared weights
and metadata whose every finite prefix satisfies the rules of 4.5. We will:
   - show that every infinite path, and every crop of one, defines a functional
     P in the unit ball B_{E^*};
   - show that two distinct infinite paths share only finitely many weights,
     and therefore that a finite family of paths has tails that obey the
     l_q bound of Type II after discarding finitely many initial pieces;
   - show that every bounded block sequence in a fixed family has a
     weak-Cauchy subsequence.

The last bullet is the source of the unconditional and separated functionals
in the counterexample.

5.1  Every infinite path defines a bounded functional.

LEMMA 19 (bounded path functionals). Let (phi_l, j_l, p_l)_{l >= 1} be an
actual infinite path in some family. Then the formula
   P(x)  =  sum_{l=1}^{infinity} phi_l(x),   x in E,
converges absolutely for every x and defines an element P in B_{E^*}. The
same statement holds after any allowed crop of the path.

PROOF. Let m be any positive integer. The finite partial sum
   S_m(x)  =  sum_{l=1}^m phi_l(x)
is a Type II functional with ONE path and coefficient 1 (allowing the empty
tail of later weights). By the rule for Type II, S_m belongs to K at some
finite stage, hence ||S_m||_{E^*} <= 1.

Convergence. The pieces phi_l have successive disjoint supports, so on any
finitely supported vector x the sum sum_l phi_l(x) has only finitely many
nonzero terms and converges trivially. Uniform boundedness of the S_m on the
Banach space E, combined with the equality of limits on the dense set of
finitely supported vectors, extends the convergence to every x in E by
finite epsilon/2-approximation.

Norm bound. On any finitely supported x, |P(x)| = lim_m |S_m(x)| <= ||x||.
Taking the supremum over x in the unit ball of c_{00} and then over the
completion gives ||P||_{E^*} <= 1.

Crops. An allowed crop is restriction to an ordinal interval (pure) or a
rectangle (mixed). This is either the same argument with additional
projections, or equivalently composing P with a contractive projection, whose
effect is again to bound the result by 1. Lemma 19 is proved.   []

5.2  Distinct paths share only finitely many weights.

The crucial combinatorial property of the coding (weights grow so that the
next weight ENCODES the whole preceding array up to finitely many ordinal
positions) is that two distinct paths must eventually disagree about their
weight list. We make this precise, then use the Type II operation to get a
uniform l_q bound for tails.

LEMMA 20 (rigidity of shared weights). Two distinct infinite paths in the same
family have only finitely many weights in common. Consequently, for any
finitely many distinct paths P_1, ..., P_h in the same family one may delete
finitely many initial pieces of each to obtain tails ~P_1, ..., ~P_h with
   || sum_{b=1}^h a_b ~P_b ||_{E^*}  <=  || (a_b)_{b=1}^h ||_{l_q}
for every real vector (a_b). Each difference P_b - ~P_b lies in X_0.

PROOF. Suppose two infinite paths share infinitely many weights. Lift this to
codes. Except possibly for the very first weight (which is arbitrary for each
path), if a weight j equals the weight at some index of path 1 and at some
index of path 2, then since the weight is produced by sigma applied to the
PRECEDING code and sigma is injective on codes, the preceding codes must
coincide. A code determines the entire prefix through the (m-1)-th piece: the
number of pieces, their metadata, their declared weights, and their rational
arrays at the relevant position-closure (without ordinal labels). So equal
preceding codes give equal prefixes UP TO the actual ordinal labels of the
supports.

Moreover, the common weights appear at index sequences m_1 < m_2 < ... for
path 1 and n_1 < n_2 < ... for path 2, and matching lengths force m_i = n_i.
So there is an infinite increasing sequence m_i with:
   prefix of length m_i of path 1 = prefix of length m_i of path 2 as ARRAYS
   AND metadata AND weights.

Interchange paths if necessary so that sup(support path 1) <= sup(support
path 2). Fix an ordinal alpha in path 1. Because path 2 has infinitely many
successive pieces with sup >= alpha (from sup path 2 >= sup path 1 >= alpha),
there is an ordinal xi >= alpha in path 2's support.

For sufficiently large i, both alpha (in path 1) and xi (in path 2) are in
their respective prefixes of length m_i, so both are in the corresponding
closures. Because both closures have the SAME final metadata p_{m_i}, and
because that metadata satisfies p_{m_i} >= rho(alpha, xi) (by the metadata
rule applied to the common prefix):
   - the closure for path 2 at stage m_i contains xi, hence F_{p_{m_i}}(xi),
     hence alpha (since alpha in F_{p_{m_i}}(xi));
   - the closure for path 1 at stage m_i contains alpha.
So two closures with the same p contain the common ordinal alpha. By coherence
(Lemma 15), their ordered initial segments through alpha coincide.

Position alignment. Let m be the index of the piece of path 1 that contains
alpha. Every piece of path 1 with index strictly less than m is supported
strictly before alpha (because supports are successive). By the position
agreement through positions up to alpha, and since path 1's pieces 1 through
m-1 are supported on the positions before alpha:
   - path 1's pieces 1 through m-1 correspond to positions below alpha in the
     closure;
   - path 2's pieces 1 through m-1 correspond to the same positions;
   - piece m of path 1, evaluated at alpha (which sits at a fixed position in
     the closure), gives a specific coefficient c.
The position-alignment observation of 4.4 then forces the entire piece m of
path 1 to be equal to the entire piece m of path 2 as a function on Gamma (not
just on the intersection of closures through alpha): both are supported on
the same coordinates, and the position agreement plus the "supported before
alpha" hypothesis for the earlier pieces makes the actual ordinal labels of
those positions equal.

Since m is arbitrary (the argument works for every piece m of path 1, and by
symmetry for every piece of path 2), the two paths have the same pieces,
weights and metadata. So the paths were identical. This proves that distinct
paths share only finitely many weights.

Tails and the l_q bound. Take finitely many distinct paths P_1, ..., P_h in
the same family. Delete finitely many initial pieces from each, past the
largest common weight with any other path. The remaining weight sets are
pairwise disjoint. Each finite sum of tail pieces is a legal crop of a finite
prefix of the original path (an ordinal-interval tail crop for pure, a tail
rectangle for mixed, using the initial-segment structure of the pieces), so
it retains the required UNcropped coding. Therefore Type II applies and gives
   || sum_{b=1}^h a_b (finite tail sum of path b) ||_{E^*}  <=  || (a_b) ||_{l_q}
for every rational (a_b) with finite support.

Pass to the limit. Take any x in E. Replace each b by its limit path
functional ~P_b(x) as the tail of pieces. By Lemma 19 the sums converge to
the ~P_b. Use continuity of x |-> sum_b a_b ~P_b(x) (elements of E^*) and
approximate real coefficients by rationals inside the l_q unit ball. This
gives the stated inequality for every real (a_b).

Differences in X_0. Each deleted piece has finite support. A finite sum of
finitely supported coordinate vector functionals is a finite linear
combination of e_alpha^*, hence lies in X_0. So P_b - ~P_b in X_0. Lemma 20
is proved.   []

5.3  Weak-Cauchy block sequences exist.

We turn to the convergence property. Fix a family (pure k, or mixed). A block
SEQUENCE in that family is a sequence (x_i) of nonzero finitely supported
vectors that are successive, and supported on C_k in the pure case, or
mixed-successive in the mixed case. A sequence is WEAK-CAUCHY when (f(x_i))
converges for every continuous linear functional f on the closed span of the
sequence.

PROPOSITION 21 (weak-Cauchy blocks). Every bounded block sequence in a fixed
family has a weak-Cauchy subsequence.

PROOF. Write M = sup_i ||x_i||. There are two steps.

STEP 1: PASS TO A SUBSEQUENCE ON WHICH EVERY ACTUAL PATH CONVERGES.

Fix delta > 0. We will build a subsequence and select a growing list of paths
P_1, P_2, ... such that:
   - every P_j converges on the subsequence,
   - at most (M / delta)^{q'} paths can ever be selected,
   - every path not selected has limsup of its absolute values at most delta.

Construction. Suppose we have already selected P_1, ..., P_{k-1} and a
subsequence on which all of them converge and |P_j - lim P_j| stays under
some tail epsilon. If there is some other path P with limsup_i |P(x_i)| >
delta, pass to the infinite subsequence on which |P(x_i)| > delta AND P(x_i)
converges (the subsequence has a convergent sub-subsequence by Bolzano-
Weierstrass in R; retaining all previous selections and their convergence is
possible because we pass to further subsequences). Record P_k = P. Continue.

Bound. Fix k. Let P_1, ..., P_k be selected paths. By Lemma 20 the tails
~P_1, ..., ~P_k obey
   || sum_b a_b ~P_b ||_{E^*}  <=  || (a_b) ||_{l_q}
for every real (a_b). The deleted prefixes are finite-support functionals,
hence vanish on all sufficiently late blocks x_i. So for sufficiently large i,
   P_b(x_i) = ~P_b(x_i)   for every b.
Thus
   || ( P_b(x_i) )_{b=1}^k ||_{l_{q'}}
     = sup{ | sum_b a_b P_b(x_i) | : ||(a_b)||_{l_q} <= 1 }
     <= ||x_i||  <=  M.
And each |P_b(x_i)| > delta on the retained subsequence, so
   k delta^{q'}  <=  M^{q'},   k <= (M / delta)^{q'}.
The selection stops after at most that many steps. At the stopping point,
every path not yet selected has limsup of |P(x_i)| at most delta.

Diagonalization. Apply the above at a sequence of thresholds delta_n = 2^{-n}
(so the thresholds decrease to zero), each time on a subsequence nested in the
previous one. Take the diagonal subsequence. Every path that has been selected
at some stage (which is a countable set of paths, since only finitely many per
threshold) converges on the diagonal: once it was selected, its convergence was
retained in every further pass, at every subsequent threshold. Every path that
was never selected has, at threshold delta_n, limsup at most delta_n, so its
limsup on the diagonal is at most delta_n for every n; hence its limsup is
zero. So on the diagonal,
   P(x_i) -> 0   for every unselected path P.
Together with convergence on the selected paths, this gives:
   P(x_i) converges for every actual path P in the family.
Relabel the diagonal subsequence as (x_i). This proves the "convergence on all
actual paths" required by Step 1.

STEP 2: EVERY POINTWISE LIMIT OF NORMING FUNCTIONALS CONVERGES ON (x_i).

Let S = union_i support(x_i), a countable set. Let C be the pointwise closure in
the compact metrizable space [-1,1]^S of the restrictions { f|_S : f in relevant
K } (use K_k in the pure case, K in the mixed case). Each u in C acts with norm
at most 1 on the closed block span [x_i]: for a finite sum y of the x_i, and
f_n in relevant K with f_n|_S -> u, |u(y)| = lim_n |f_n(y)| <= ||y||.

OSCILLATION. For u in C set
   osc(u)  =  limsup_i u(x_i) - liminf_i u(x_i)  in [-2M, 2M],
   D       =  sup_{u in C} osc(u)  <= 2M.
We will prove D = 0, so every u in C gives a convergent sequence u(x_i).

FIX u in C. Choose f_n in the relevant K with f_n|_S -> u pointwise on S.
Subselect so that the TOP expressions of f_n are, on a subsequence,
   - all terminals, or
   - all Type I, or
   - all Type II.
We do NOT require their construction depths to be bounded: all child limits
stay in the same compact set C.

TERMINALS AND TYPE I LIMITS.

Pure terminals. f_n = +/- e_{alpha_n}^*. Either alpha_n is fixed on a
subsequence: then u is that terminal, and u(x_i) is 0 for all sufficiently
large i (the x_i are successive, so each fixed coordinate is hit at most once),
so osc(u) = 0. Or the alpha_n drift in the same color: for any BLOCK sequence
of successive mixed-successive x_i, the alpha_n hit at most one block, and for
any fixed i, u(x_i) = 0. So u is zero on the block span and osc(u) = 0.

Mixed terminals. Each belongs to some pure color C_k. If the colors drift, the
pointwise limit is zero (a block hits at most one piece per color). If the
color is fixed, the terminal meets at most one of the mixed-successive blocks,
so osc = 0.

Type I limits whose weights overflow. If the weight j_n -> infinity, the
coefficient bound 1/m_{j_n} on each coordinate of the piece gives pointwise
limit zero on S, so u = 0 pointwise, osc = 0.

Type I limits at fixed weight j. Fix the number of children d <= L_j and the
pointwise limits v_1, ..., v_d of the children (each v_h in C):
   u  =  (1 / m_j) sum_{h=1}^{d} v_h.
Nonzero coordinates of different child limits preserve their order (children
have successive supports in the pure case and mixed-successive supports in the
mixed case). At most ONE child limit can meet infinitely many blocks. For if
an EARLIER child v_h met infinitely many, its hits would eventually occur
beyond any fixed hit of a later child v_{h'}, contradicting the order. So all
other children are zero on all sufficiently late blocks. Therefore
   osc(u)  <=  D / m_j.       [TYPE I OSC]
The same conclusion applies to a pointwise limit of CROPPED Type I pieces:
distribute the crop to the children, discard zeros, then take limits.

INDIVIDUAL TERMS IN A TYPE II LIMIT.

The central issue is a single cropped path term. We show that its pointwise
limit agrees, on all sufficiently late blocks, with one of: zero; a limit of a
single Type I piece; or an actual infinite path. Then we sum the D/m_j costs
across the disjoint active weights.

Setup. For the Type II limit write g_n = sum_b a_b^{(n)} (cropped path b). Index
each term by its smallest active weight b. The indices are distinct within any
single g_n. A diagonal subsequence makes, for each b:
   - presence (b appears as active in g_n) or absence eventually constant,
   - its coefficient a_b^{(n)} converge to a real number a_b,
   - crop membership for each coordinate of S converge.
Set a_b = 0 for absent terms. By Fatou on finite sets,
   sum_b |a_b|^q  <=  1.                                    [LIMIT COEFFS]
For each present term, take pointwise limits of its path crop; call the
resulting functional on the block span u_b.

Fixing the weight list. The uncropped weight list through b has finitely many
possibilities (weights strictly increase). Fix it on a subsequence. Successive
extensions: at each position, the path ends, or the next weight tends to
infinity, or the next weight can be fixed on a subsequence. Diagonalizing
produces a finite fixed chain possibly followed by a divergent-weight suffix,
or an infinite fixed chain. Take pointwise limits of all cropped pieces in
this chain.

Divergent-weight suffix. It contributes nothing in the pointwise limit: each
coordinate meets at most one piece of the suffix, and its coefficient is
bounded by the reciprocal of the least weight's m-parameter, tending to zero.

Fixed piece with fixed successor. Whenever a fixed piece has a fixed successor
weight, that successor fixes its entire preceding code, hence its support-size
bound (by the length of the finite array in the code). Its pointwise limit
therefore has FINITE support.

Finite fixed chain. Only its last piece can have a limit with infinite support.
If its weight is j, [TYPE I OSC] gives
   osc(u_b)  <=  D / m_j.       [FINITE CHAIN OSC]
If the last cropped piece has zero pointwise limit, u_b is finitely supported,
osc(u_b) = 0. Otherwise the last weight is active in all sufficiently late
approximating terms; the LAST WEIGHTS FOR SUCH POTENTIALLY OSCILLATING TERMS ARE
THEREFORE DISTINCT (two such cannot be active in different terms of the same
type II approximant).

INFINITE FIXED CHAINS AND THEIR LIMITING CROPS.

Now suppose the fixed chain has infinitely many pieces. Every individual piece
of the chain has a finitely supported pointwise limit (as above). The pointwise
limit of the path crop equals the sum of these piece limits. To see that no
additional contribution escapes to high piece positions, note that the
coordinate error after the first l pieces is at most 1/m_{j_{l+1}} for the next
weight j_{l+1}, uniformly in sufficiently late approximants.

If only finitely many cropped piece limits are nonzero, u_b is finitely
supported (as a sum of finitely supported limits) and has zero oscillation.

Otherwise, arbitrarily late pieces have nonzero cropped limits. Choose a
coordinate beta in S whose limit is nonzero in one such piece. Eventually beta
belongs to the ACTUAL support of that piece and is retained by its crop. The
fixed NEXT weight fixes the prefix code through that piece, including its
metadata p. All corresponding approximating closures contain beta, and their
initial segments through beta are exactly F_p(beta). Every earlier uncropped
piece is supported strictly before beta. The position-alignment observation of
4.4 shows that the earlier uncropped pieces are eventually the SAME actual
functions on Gamma.

Choose beta in arbitrarily late effective pieces. This proves eventual
stabilization of every uncropped prefix of the path, along with its weights and
metadata. These stabilized prefixes define an ACTUAL infinite path P. Its
pieces are valid Type I expressions because each stabilized piece equals a
piece from some approximating path; every finite prefix of P satisfies the
required coding rule for the same reason.

The limiting crop changes P on only finitely many coordinates of S. To see
this, fix one retained coordinate beta in a piece. For any coordinate alpha in
S that lies in a strictly later piece, choose a retained coordinate gamma in a
still later effective piece. In late approximants the stabilized coordinates
beta, alpha, gamma have their fixed ordinal order, and in the mixed case their
fixed color order. Both beta and gamma lie in the crop. Interval convexity, in
both orders when required, forces alpha to be in the crop as well. So the
limiting crop retains every path coordinate of S after the piece containing
beta. Only the finitely many pieces up to and including the piece containing
beta can differ.

It follows that u_b(x_i) - P(x_i) is eventually zero. Step 1 proved that
P(x_i) converges. So u_b(x_i) converges, hence every infinite-chain term has
zero oscillation.

REASSEMBLING THE TYPE II LIMIT.

We have
   u  =  sum_b a_b u_b   pointwise on the block span [x_i].   [LIMIT SERIES]
Indeed, terms with smallest active weight b > N have coordinate error at most
sum_{j>N} 1/m_j, uniformly in all approximants. At a given coordinate there is
at most one contributing piece per path, and the contributing active weights
are globally distinct. So [LIMIT SERIES] holds after passing to the finitely
many indices b <= N and then letting N -> infinity.

The series also converges in DUAL NORM on the block span. For every finite set
of present indices and every real coefficient vector (c_b) with l_q norm at
most one, replace the approximating type II coefficients by RATIONAL
approximations to (c_b) inside the closed l_q unit ball. They remain admissible,
since the underlying paths and their pairwise disjoint active weights have not
changed. Passing to the pointwise limits on finite vectors gives
   || sum_b c_b u_b ||_{[x_i]^*}  <=  1.
By [LIMIT COEFFS], finite truncations of sum_b a_b u_b are Cauchy in dual norm.
Their norm limit agrees with [LIMIT SERIES] on the block vectors.

Oscillation of u. Oscillation is subadditive, and changes by at most
2M ||v - w|| when one bounded functional is replaced by another. Using finite
truncations, the distinct potentially oscillating last weights in
[FINITE CHAIN OSC], and |a_b| <= 1, we get
   osc(u)  <=  D sum_{j=1}^{infty} 1/m_j.       [TYPE II OSC]
All other terms have zero oscillation.

THE CONSTRAINT D = 0.

Terminal, Type I and Type II cases are exhaustive for the top expressions.
Equations [TYPE I OSC] and [TYPE II OSC], together with Lemma 14 (sum_j 1/m_j <
1/8), imply
   D  <=  ( sum_j 1/m_j ) D  <  (1/8) D  if D > 0.
Hence D = 0. Concretely: every u in C gives a convergent sequence u(x_i).

FINISHING: WEAK-CAUCHY.

Evaluation embeds the closed block span [x_i] isometrically into C(C): each
finite vector y |-> (u |-> u(y)) is continuous, and finite approximation extends
this to the closed span by Holder-type bounds (all elements of B_{[x_i]}). More
directly, given any continuous linear functional phi on [x_i], extend by
Hahn-Banach to a functional phi~ on C(C) with ||phi~|| = ||phi||. The
Riesz-Markov representation theorem expresses phi~ as integration against a
finite signed Borel measure nu on C, with |nu|(C) < infinity.

The functions u |-> u(x_i) are uniformly bounded by M and converge at every u in
C. Bounded convergence with respect to |nu| therefore proves convergence of
phi(x_i) = integral of u |-> u(x_i) against nu. The subsequence (x_i) is
weak-Cauchy. Proposition 21 is proved.   []


==============================================================================
PART 6.  BLOCKS DETECTED AT A PRESCRIBED WEIGHT
==============================================================================

6.0  What this part does.

The path coding is now usable, but only if we can PRESCRIBE the next weight of
a path and still find a bounded vector on which the next piece actually is
substantial. This is the technical heart of the counterexample: we need
uniform control of every estimate in the target weight J.

LEMMA 22 (pairing at a prescribed weight, Proposition pair:exact). Fix one
family. Let (z_n) be an infinite admissible block sequence in E. Given a tail of
this sequence and an integer J >= 1, there are a finite block y in that tail
and a Type I functional phi of weight J in the same family, such that
   ||y||  <=  500,    phi(y)  >=  1/2.
Moreover the support of phi lies in the ordinal range of y, and also in its
color range in the mixed case.

The proof has three steps:
   (i) find blocks whose norm is spread over intervals (Lemma 23);
   (ii) differences of a weak-Cauchy subsequence permit a Ramsey argument to
        limit how often one path can hit the prescribed weight windows
        (Lemma 24);
   (iii) estimate every norming expression by following only its pieces below
        the prescribed weight (Lemma 26).

Throughout this part, constants are uniform in the family and in the target
weight J.

Setup. Fix one family. An "admissible block sequence" consists of nonzero
finite vectors with successive (pure) or mixed-successive (mixed) supports,
supported on the correct color in the pure case. A finite block is a nonzero
finite linear combination of successive members; successive blocks use successive
finite sets of indices. We use the notation s, r = s', q, L_j, m_j, theta_j,
c_0, B_j, d_j of Lemma 14 for this family. In particular 1 < q < r, and
theta_j = L_j^{1/r}/m_j.

6.1  Finding blocks whose norm is spread over intervals.

LEMMA 23 (pair:partition). For every positive integer N, every infinite
admissible block sequence has a finite unit block u such that, for all
1 <= d <= N and all successive disjoint ordinal intervals I_1, ..., I_d,
   sum_{b=1}^{d} ||P_{I_b} u||  <=  8 d^{1/r}.
The block can be chosen in any prescribed tail. (In the mixed family the
intervals I_b are rectangles, and "successive disjoint ordinal intervals"
becomes "successive disjoint rectangles".)

PROOF. Work in the prescribed tail. Define a(k) for k >= 1 as the supremum of
||sum_{i=1}^k v_i|| over all choices of k successive finite unit blocks v_1, ...,
v_k (in the tail). Contractivity of the interval projections gives a(k) <= k.

Lower bound a(L_h) >= L_h / (2 m_h). Fix h. Norm L_h successive unit blocks to
within a factor 2 of their norm: there are finite unit blocks v_1, ..., v_{L_h}
with ||v_i|| = 1 and pure normers g_i in K_k of norm <= 1 with g_i(v_i) >= 1/2
(in the mixed case use the mixed K with rectangle crops). Crop each g_i to its
block range (an ordinal interval, and in mixed case to a rectangle). The
cropped g_i are still in K, and they are supported on successive block ranges.
Their weight-h Type I average
   phi  =  (1/m_h) sum_{i=1}^{L_h} (cropped g_i)
has norm <= 1 and satisfies phi( sum_{i=1}^{L_h} v_i ) >= (1/m_h) (L_h / 2) =
L_h/(2 m_h). So ||sum_i v_i|| >= L_h/(2 m_h), giving a(L_h) >= L_h/(2 m_h).

Growth. Choose t > s sufficiently close to s that d^{1/t'} <= 2 d^{1/r} for
every 1 <= d <= N. Lemma 14 (growth condition) implies a(k)/k^{1/t} is unbounded
in k. In particular there is a "record" index k with
   a(l) <= a(k) (l/k)^{1/t}   for every 1 <= l <= k,
   a(k) >= N^{1/s}
(the last inequality because a(k)/k^{1/t} grows, and k large).

Choose k successive unit blocks v_1, ..., v_k with ||sum_i v_i|| >= a(k)/2
(a(k) is a supremum over successive blocks; take near-maximizers). Define the
finite unit block
   u  =  (sum_i v_i) / ||sum_i v_i||.
It is normalized and still unit.

Spread bound. For each interval I_b, let l_b count the blocks whose ordinal
range lies ENTIRELY inside I_b (in the mixed case, whose rectangle lies entirely
inside I_b). At most TWO further blocks have range that PARTLY meets I_b (one
entering from the left, one leaving to the right); their projected norms are at
most 1 each (the blocks are unit and projections are contractive). Since the
blocks are successive, the intervals I_b partition the blocks up to the boundary
blocks, so
   sum_{b=1}^{d} l_b  <=  k.
By the record inequality and Holder,
   sum_{b=1}^{d} ||P_{I_b} u||
      <=  2 sum_{b : l_b > 0} (l_b / k)^{1/t}  +  4 d / a(k)
      <=  2 d^{1/t'}  +  4 d / N^{1/s}
      <=  8 d^{1/r}.
The first sum uses l_b >= 1 for its nonzero terms and Holder with the exponents
t and t'. The second uses the "at most 2 boundary blocks each of norm <= 1"
bound, so 4d total, divided by the normalization ||sum v_i|| >= a(k)/2 >= a(k)/2.
Finally, d <= N and the choice of t give 2 d^{1/t'} <= 4 d^{1/r}, and the second
term 4 d / N^{1/s} <= 4 d^{1/r} (because d <= N implies d / N^{1/s} <=
d^{1 - 1/s} = d^{1/r}). Total at most 8 d^{1/r}. Lemma 23 is proved.   []

6.2  Windows: a weakly null sequence avoiding every prescribed weight band.

The partition lemma lets us find blocks whose norm is spread. We will now
combine it with the weak-Cauchy result to get a sequence (x_j) whose norm is
NOT concentrated on any narrow band of weights, and whose weights avoid an
arbitrary prescribed band of weights. The
following lemma makes all four required properties explicit.

LEMMA (window construction). Fix J and set L = L_J. Choose epsilon > 0 with
   epsilon L^{1/r}  <=  theta_J.                          [EPS CONDITION]
Then there is a weakly null admissible block sequence (x_i) with integer
windows [J_i, T_i] satisfying all of:

   [W-ORDER]     1 <= ||x_i|| <= 2,  J_i > J,  J_{i+1} > T_i;
   [W-COHERE]    J_i > max_rho( union_{h<i} support(x_h) );
   [W-PART]      for every 1 <= d <= L_{J_i} and every successive disjoint
                 ordinal intervals (rectangles in the mixed case) I_1, ..., I_d:
                    sum_{b=1}^d ||P_{I_b} x_i||  <=  A d^{1/r},  A := 16;
   [W-TAIL]      ||x_i||_1 sum_{j>T_i} 1/m_j  <=  epsilon,
                 and also ||x_i||_1 sum_{j>T_i} 1/m_j -> 0 as i -> infinity.

Here ||x||_1 = sum_{alpha in support(x)} |x(alpha)| for a finite vector.

PROOF.

Preliminary blocks. Choose an infinite tail of the block sequence to work in.
We construct preliminary successive unit blocks u_1, u_2, ... in the tail.
Inductively, after u_1, ..., u_{i-1} are chosen, choose an integer J_i that is
   - strictly greater than J,
   - strictly greater than T_{i-1} (if i > 1; ignore at i = 1),
   - strictly greater than every rho-value rho(alpha, beta) with alpha <= beta
     ranging over the finite union of supports of u_1, ..., u_{i-1}.
Apply Lemma 23 with N = L_{J_i} inside the current tail to get the block u_i
(a unit block; scale trivially to unit is already part of Lemma 23). Then
choose T_i >= J_i so large that
   ||u_i||_1  sum_{j>T_i} 1/m_j  <=  min( epsilon / 2, 1 / i ).
This is possible because the tail sum sum_{j>T} 1/m_j -> 0 (since sum_j 1/m_j
< 1/8 in Lemma 14). This finishes the preliminary sequence u_i.

Pass to weak-Cauchy. By Proposition 21, the bounded block sequence (u_i) has a
weak-Cauchy subsequence; relabel it back to (u_i). Each u_i still satisfies the
partition bound (Lemma 23 applied to the tail at the moment of choice persists
under taking a subsequence) and the tail bound.

Differences. Pair successive members: form for j >= 1
   x_j  =  u_{2j} - u_{2j-1}.
Each x_j is nonzero (the projections to the odd block have norm >= 1, projection
contractive). The blocks u_i have successive ordinal ranges (and in the mixed
case, mixed-successive color ranges), so the differences x_j are an admissible
block sequence; also, since the u_i are weakly Cauchy, the differences u_{2j} -
u_{2j-1} are weakly null.

Norm bounds. Projection P_{range of u_{2j-1}} applied to x_j equals u_{2j-1}, of
norm 1; and ||x_j|| <= ||u_{2j}|| + ||u_{2j-1}|| <= 2. So [W-ORDER] holds with
   J_j := J_{2j-1},   T_j := T_{2j}.
And J_{j+1} = J_{2j+1} > T_{2j} = T_j (by the choice of J_i > T_{i-1} and the
fact that the J's and T's are increasing along the sequence once relabelled;
the notation "first member of pair" versus "second member of previous pair"
matches this).

Coherence. max_rho(supp x_h) for h < j is at most max_rho over the union of
support(u_1) ... support(u_{2j-1}) (since h < j implies 2h <= 2j - 2, so
supp x_h is supported in supp(u_{2h-1}) union supp(u_{2h}) with 2h <= 2j - 2
< 2j-1). The choice of J_{2j-1} > max rho of that union gives [W-COHERE].

Partition. For any interval I_b (rectangle in the mixed case),
   ||P_{I_b} x_j||  <=  ||P_{I_b} u_{2j}|| + ||P_{I_b} u_{2j-1}||
                    <=  8 d^{1/r} + 8 d^{1/r}  =  16 d^{1/r} = A d^{1/r},
valid for d <= min(L_{J_{2j-1}}, L_{J_{2j}}) = L_{J_j} because L is increasing
and J_{2j-1} <= J_{2j}. So [W-PART] holds.

Tail. ||x_j||_1 <= ||u_{2j}||_1 + ||u_{2j-1}||_1 and T_j = T_{2j} >= T_{2j-1}.
   ||x_j||_1 sum_{k>T_j} 1/m_k
     <= (||u_{2j}||_1 + ||u_{2j-1}||_1) sum_{k>T_{2j}} 1/m_k
     <= ||u_{2j}||_1 sum_{k>T_{2j}} 1/m_k  +  ||u_{2j-1}||_1 sum_{k>T_{2j-1}} 1/m_k
     <= epsilon/2 + epsilon/2  = epsilon.
The limit to zero follows from the corresponding monotone tails of the u's.
So [W-TAIL] holds. Relabel the resulting sequence and its windows as (x_i) and
[J_i, T_i]. This proves the window construction lemma.   []

6.3  A path cannot repeatedly meet its weight windows.

For a finite uncropped path P = (phi_l) with weights j_l, write
   P[i]  =  sum_{l : J_i <= j_l <= T_i} phi_l.
Say P HITS i at threshold delta > 0 when |P[i](x_i)| > delta. This uses the
ORIGINAL pieces and their original coding, even when the path is later cropped
inside a norming expression.

LEMMA 24 (four hits). For every delta > 0 and every infinite set of indices
there is an infinite subset on which no finite uncropped path has four hits at
threshold delta.

PROOF. Color a four-element set of indices POSITIVELY if one finite path hits
all four at threshold delta. By the infinite Ramsey theorem, it suffices to
rule out an infinite set M every four-element subset of which is positive.

Fix v < t < k in M. For each w in M with w < v, choose a path P_w hitting w,
v, t, k. Partition these paths according to their actual histories of weights
below J_v: the history records the uncropped pieces with weights < J_v, their
weights, and their metadata, together with their actual ordinal coordinates.

CLAIM. Representatives of different classes have disjoint weight sets in
[J_k, T_k].

PROOF of the claim. Suppose two such paths share a weight j in [J_k, T_k]. We
will show their histories below J_v coincide, i.e. they are of the same class.

Because both paths hit t at some weight in [J_t, T_t] with J_t <= T_t < J_k <=
j, the piece at weight j comes after the t-window piece in both paths, and
weight j is therefore a successor weight (not the first). Injectivity of the
coding map sigma identifies their preceding compressed codes. The (l-1)-prefix
common metadata p := p_{l-1} of these matching codes satisfies p >= J_t
because the t-window piece is already part of the prefix through l-1 and has
weight >= J_t. Hence, using [W-COHERE], J_v > max_rho(supp x_v) and so
   p >= J_t > T_v + something > max_rho(supp x_v).
Precisely, T_v + 1 > all supp-ordinals relevant to x_v in path 1; and
J_{v+1} > T_v so p >= J_t >= J_{v+1} > T_v > max_rho(supp x_v).

Choose coordinates a, b of supp x_v at which the respective v-window pieces are
nonzero; WLOG a <= b. In path 1, a is in the support of the v-window piece,
which lies inside the (l-1)-prefix support. So a in F_p(beta_1), where beta_1
is the largest ordinal in path 1's (l-1)-prefix. Similarly, in path 2, b is in
F_p(beta_2).

Now use coherence. Since
   rho(a, b)  <=  max_rho(supp x_v)  <  p,
Lemma 15 gives a in F_p(b), and hence a in F_p(beta_2) (since b <= beta_2 and
F_p(beta_2) contains [0, beta_2] at level p). The two closures F_p(beta_1) and
F_p(beta_2) thus both contain a, and by Lemma 15 they have the same initial
segment through a:
   F_p(beta_1) cap [0, a]  =  F_p(a)  =  F_p(beta_2) cap [0, a].

In path 1 every piece of weight below J_v is supported strictly before the
v-window piece's support (successive supports, and the v-window piece is at
weight >= J_v > weights below J_v). Consequently its compressed array is zero
at order positions strictly after the position of a. The same is true in path
2. Since the closures coincide through a, the compressed arrays of the two
paths coincide below the position of a. By the coding rule (sigma is injective
on these arrays), the two histories below J_v are EQUAL as ordinal-coordinate
functions. This proves the claim.

Class bound. Crop each class representative to its pieces in [J_k, T_k]. This
is a legal ordinal-interval crop (rectangle crop in the mixed case), because
pieces and weights are successive. Their active weight sets are pairwise
disjoint by the claim. Type II combinations and rational approximation
therefore give
   || ( P_b[k](x_k) )_b ||_{q'}  <=  || x_k ||  <=  2.
Every coordinate has absolute value greater than delta. In particular, the
number of classes is at most some integer D depending only on delta; for
instance D = ceiling of (2 / delta)^{q'}.

Diagonalization. Choose triples v_n < t_n < k_n from M with v_n -> infinity,
and label the classes for each triple by elements of {1, ..., D}. Each fixed
w in M has a label once w < v_n. Successive subsequences followed by a diagonal
subsequence make each label eventually constant. One label occurs for an
infinite set M_0 of fixed indices. For every fixed w in M_0 and every
sufficiently large n, if P_n is a representative of the label in level n then
P_n hits w: because eventually T_w < J_{v_n}, and equality of actual histories
below J_{v_n} preserves the whole w-window.

Contradiction. Choose w_0 in M_0 so large that
   A sum_{j >= J_{w_0}} theta_j  <  delta/4.
For fixed w in M_0 with w > w_0, consider n large enough that P_n hits both
w_0 and w. Every piece of weight below J_{w_0} precedes some coordinate of
supp x_{w_0}, and hence vanishes on x_w. For J_{w_0} <= j < J_w, the child
intervals of a weight-j piece and [W-PART] give the bound A theta_j on its
absolute evaluation at x_w (with distinct children contributing to distinct
child intervals of total l_r weight at most A d^{1/r} / m_j <= A theta_j). The
total contribution of weights above T_w is at most the expression in
[W-TAIL], which is less than delta/4 for all sufficiently large w.
Consequently
   |P_n(x_w)|  >=  delta / 2
for every sufficiently large fixed w in M_0, once n is sufficiently large
depending on w.

Weak-star limit. Since x_w is weakly null, and since each P_n is a bounded path
functional of norm at most 1 (Lemma 19), Banach-Alaoglu gives a subnet of (P_n)
converging weak-star to some P in the unit ball of E^*. For every fixed w in
M_0, the evaluations P_n(x_w) converge along the subnet to P(x_w); in absolute
value each is at least delta/2, so |P(x_w)| >= delta/2. Weak nullity of (x_w)
gives P(x_w) -> 0, contradiction. This proves Lemma 24.   []

6.4  Estimating every norming expression at the block sequence.

Fix J with L = L_J. Following Lemma 24 and choosing delta = theta_J / 8 (which
is small enough for what follows), apply Lemma 24 to the weakly null block
sequence (x_i) of the window construction and delta:
there is an infinite subset M of the indices on which no finite uncropped path
has four hits at threshold delta. Relabel (x_i) as the indices of M. This
preserves all of [W-ORDER], [W-COHERE], [W-PART], [W-TAIL]. Its members are
again weakly null and have norms between 1 and 2.

LEMMA (sum bound). With the notation above, for every norming expression f of
the family,
   sum_{i=1}^L |f(x_i)|  <=  (2112 / 7) (L / m_J)  <  500 (L / m_J).

PROOF. We expand f through its expression tree and for each block x_i trace the
contribution of f to x_i via a recursive descent. The recursion terminates
either because we choose to charge (when the decay d of the child-intersection
is at least 2) or because we hit the depth d_J (see Lemma 14).

Notation. Fix an expression tree for f. A node n has a weight j = j_n and
child functionals g_{n,1}, ..., g_{n,d_n} with d_n <= L_{j_n}. A block x_i is
"assigned" to n when the descent along the trace of x_i reached n. For a node
n and a block x_i assigned to n, write
   d_{n,i}  =  number of child ordinal intervals of n meeting supp x_i.
This is well-defined and finite for every pair (n, i).

Weight balance at a node. If d_{n,i} >= 1, [W-PART] gives, since
d_{n,i} <= L_{j_n} <= L_{J_i} (all children of any ancestor of n at "level
>= i" have at most L_{j} <= L_{J_i} children by monotonicity of L and j >=
J_ancestor >= J_i),
   |P_{I_b} phi_n(x_i)|  <=  A / m_{j_n} * d_{n,i}^{1/r},
where phi_n is the Type I piece at n (or the Type II expression at n, in which
case the same bound applies to each term). Three cases:

   (a) d_{n,i} = 0: the node contributes 0 at x_i.

   (b) d_{n,i} = 1: continue to that unique child, retaining the coefficient
       |a_b| / m_{j_n} <= 1 / m_{j_n}. Within one group the index sets
       assigned to different children are disjoint.

   (c) d_{n,i} >= 2: terminate, charging A theta_{j_n} (since
       d_{n,i}^{1/r} <= L_{j_n}^{1/r}).

Boundary incidence. For a group (i.e., a piece phi_n at weight j) the child
ordinal intervals are successive. Each block x_i is either entirely inside a
single child's interval (d = 1 with the child's interval containing supp x_i,
or d = 0) or it straddles two child boundaries (d >= 2), or it straddles only
one (d = 2). The number of blocks x_i with d_{n,i} >= 2 is bounded by the
number of child-child boundaries, which is at most 2 L_j (each internal
boundary is straddled by at most one x_i for the left edge and one for the
right edge, and the total boundaries of L_j successive children are L_j - 1,
plus the two outer end-points). So
   sum_{i: d_{n,i} >= 2} d_{n,i}  <=  2 L_j.       [INCIDENCE]

Stopping above the prescribed weight. Refine the recursion: continue only
singleton cases (d = 1) with j < J. For low groups with j >= J, stop the
singleton cases too. Their total incidence is at most 2L_j + L <= 3 L_j (by
[INCIDENCE] plus the singleton cases with j >= J, of which there are at most L
because there are L blocks). Their l_r charge is consequently at most
3A theta_j per group. Together with the HIGH and UNMARKED charges, the small
charge at any node has l_r norm at most
   3A sum_{j >= J} theta_j + 2 epsilon L^{1/r}
     <= 3A (4 theta_J) + 2 theta_J                            (Lemma 14 + [EPS])
     =  (12A + 2) theta_J.                                   [SMALL]

Propagation. If every continued child's l_r charge vector has norm at most K,
disjointness of the assignments within one group bounds the parent's combined
contribution by
   K L_{j_n}^{1/r} / m_{j_n}  =  K theta_{j_n}.
Summing over distinct weights j_n < J (with a triangle inequality that does
not require disjointness across groups):
   parent charge  <=  K sum_{j_n < J} theta_{j_n}  <=  c_0 K.
A factor c_0 per level of the recursion. Propagate the small charges [SMALL]
successively:
   cumulative charge  <=  (12A + 2) theta_J (1 + c_0 + c_0^2 + ...)
                      =  (12A + 2) theta_J / (1 - c_0)
                      =  194 theta_J / (7/8)
                      =  1552 theta_J / 7.                [CUM-CUM]

Residual at depth d_J. Continue the recursion to depth d = d_J (the depth
associated to J in Lemma 14). The residual charges (terminal coordinate
contributions at depth d_J multiplied by the coefficient chains) have l_r
norm at most c_0^{d_J} K_0, where K_0 = 64. The bound K_0 = 64 comes from the
following one-step estimate: at every nonterminal node the evaluation vector
bound is
   16 + 2 epsilon L^{1/r} + 2A c_0 + c_0 K_0
     <= 16 + 64(1/8) + 32(1/8) + (1/8) * K_0       (A = 16, [EPS], c_0 < 1/8)
     <= 16 + 8 + 4 + 8  =  36  <  64.
Iterating establishes K_0 = 64 uniformly in all recursive assignments.

Total small charge. Combining [CUM-CUM] and the residual c_0^{d_J} K_0:
   cumulative l_r charge  <=  (1552/7) theta_J + c_0^{d_J} 64.
But (1/8)^{d_J} <= theta_J by Lemma 14, so c_0^{d_J} K_0 <= 64 theta_J, and
   total  <=  (1552/7 + 64) theta_J  =  (1552/7 + 448/7) theta_J
                                    =  (2000/7) theta_J.

From l_r to l_1. The l_1 bound follows by Hölder's inequality: if a vector has
l_r norm T, its l_1 norm is at most T L^{1/s}. So the cumulative l_1 charge is
at most
   (2000/7) theta_J L^{1/s}  =  (2000/7) (L_J^{1/r}/m_J) L^{1/s}
                             =  (2000/7) L_J^{1/s + 1/r} / m_J
                             =  (2000/7) L / m_J.

Other charges above depth d_J. It remains to count charges above d_J (i.e.,
not captured by the "small" and "residual" l_r bounds above): terminal charges,
marked charges, and boundary charges of weights j < J. At a node, their l_1
sum is at most
   2 + 16 L^{1/q'} + A B_J
     <= 16 (1 + B_J + L^{1/q'}).
Here the 2 is the terminal coordinate contribution, the 16 L^{1/q'} is the
boundary charge of weights j < J (by Q'-conjugate of the incidence bound), and
A B_J is the marked charge from singleton cases charged at marked positions.
A node has at most sum_{j<J} L_j = B_J / 2 smaller continued children, so the
number of nodes at depths BELOW d_J is at most (1 + B_J/2)^{d_J}. Propagation
coefficients are at most 1. By the second inequality of Lemma 14,
   (1 + B_J)^{d_J} (1 + B_J + L^{1/q'})  <=  L / m_J,
so the total cost of all these other charges is at most 16 L / m_J.

Conclusion. Combining the two bounds:
   sum_{i=1}^L |f(x_i)|  <=  (2000/7) L/m_J  +  16 L/m_J
                          =  (2112/7) L/m_J
                          <  500 L/m_J.
This is the sum bound.   []

6.5  Exact pairs at any prescribed weight.

We now state and prove the main result of Part 6: for every tail of an
admissible block sequence and every prescribed weight J, we can find a finite
block y of bounded norm and a Type I functional phi of weight J such that phi
evaluates at least 1/2 on y with small norm.

PROPOSITION (pair:exact). Let (z_n) be an infinite admissible block sequence in
E. Given a tail of this sequence and an integer J >= 1, there are a finite
block y in that tail and a Type I functional phi of weight J in the SAME family
such that
   ||y|| <= 500,   phi(y) >= 1/2.                        [EXACT PAIR]
The support of phi lies in the ordinal range of y, and also in its color range
in the mixed case.

PROOF.

Setup. Work in the prescribed tail. Put L = L_J, theta_J as in Lemma 14, and
choose epsilon > 0 with epsilon L^{1/r} <= theta_J (this is the choice in
[EPS CONDITION]). Apply the window construction of 6.2 to obtain a weakly null
admissible block sequence (x_i) with integer windows [J_i, T_i] satisfying
[W-ORDER], [W-COHERE], [W-PART], [W-TAIL]. Write A = 16 for the constant in
[W-PART].

Sum bound. By the sum bound of 6.4, for every norming functional f of the
family,
   sum_{i=1}^L |f(x_i)|  <=  (2112/7) L/m_J  <  500 L/m_J.

The averaging block. Define
   y  =  (m_J / L) sum_{i=1}^L x_i.
Then
   ||y||  =  sup_{||f|| <= 1} |f(y)|
          =  (m_J / L) sup_{||f|| <= 1} | sum_{i=1}^L f(x_i) |
          <= (m_J / L) (500 L/m_J)  =  500.
The supremum is taken over norming functionals of the family (by amplitude, we
only test on the family because the block sequence is in that family).

Normers at the block level. For each i, since 1 <= ||x_i|| <= 2, Banach
duality in the dual E^* gives a normer g_i in the family with
   g_i(x_i) >= 1/2.
(More precisely, ||x_i|| >= 1 means some functional f in K or K_k of norm <= 1
has |f(x_i)| >= 1/2; by symmetry of K_k and K we may and do choose g_i with
g_i(x_i) >= 1/2 positive.)

Crop each normer to the ordinal range of x_i, and additionally to its color
range in the mixed case. Since x_i is supported in that range (and in that
color set in the mixed case), the crop does not change the evaluation:
   (P_{range(x_i)} g_i)(x_i)  =  g_i(x_i)  >=  1/2.
And P_{range(x_i)} g_i is again in the family (Lemma 16(b), crop stability).
Denote the cropped normer again by g_i.

Succession. The blocks x_i are successive (by construction: [W-ORDER] and
succession of the underlying block sequence). Their ordinal ranges are
successive. The cropped g_i are supported in these ranges. So the g_i are
successive.

Assembling the Type I functional. Define
   phi  =  (1 / m_J) sum_{i=1}^L g_i.
Since there are L = L_J children, each of norm <= 1 (they are normers of the
family), supported on successive ordinal intervals (and successive color
intervals in the mixed case), phi is a legitimate Type I expression of weight
J. Place it at a finite stage of K_k (pure) or K (mixed) later than every
stage containing one of the g_i; the construction allows this because the
stage parameter is arbitrary.

Cross-vanishing. For j != i, g_i is supported in range(x_i) and x_j is
supported in range(x_j), and these ranges are disjoint (successive). So
g_i(x_j) = 0 for j != i. (In the mixed case, additionally the color ranges are
disjoint, so the same conclusion holds.)

Evaluation. As y = (m_J / L) sum_i x_i,
   phi(y)  =  (1 / m_J) sum_i g_i(y)
           =  (1 / m_J) sum_i g_i( (m_J / L) sum_j x_j )
           =  (1 / L) sum_i sum_j g_i(x_j)
           =  (1 / L) sum_i g_i(x_i)        (cross-vanishing)
           >= (1 / L) (L / 2)  =  1/2.
And ||y|| <= 500 from the sum bound.

Support of phi. By construction, phi is supported in the union of the ordinal
ranges of the x_i, which is exactly the ordinal range of y = (m_J/L) sum x_i.
In the mixed case phi is supported in the intersection of that ordinal range
with the union of the color ranges of the x_i, which is the color range of y.
This completes the proof of the pair:exact proposition.   []



==============================================================================
PART 7.  SEPARATING FUNCTIONALS ON EVERY SUBSPACE
==============================================================================

7.1  What this part delivers.

Let F subset E be closed infinite-dimensional. Theorem branch:separation below
produces
   - a single family t (either pure k or mixed *),
   - a number delta_F > 0,
   - path functionals P_b in B_{E^*}, one for each b in {0, 1}^N,
such that ||P_b|_F - P_c|_F|| >= delta_F for ANY b != c.

This is the "separation" input to Part 8 (the construction of the counterexample
predual). The point is that ALL such functionals live in a single family, so
that the l_q estimates of Part 5 (for Type II combinations across paths of the
same family) apply. Being indexed by an uncountable set (Cantor space) matters
in Part 8, where we need uncountably many path functionals.

LEMMA 30 (successive-block approximation). With H, gamma as in the reduction
Lemma 31 of section 7.2 below, choose
positive numbers epsilon_i with sum_i epsilon_i <= 1/32000. Then there are unit
vectors h_i in H and nonzero finitely supported vectors z_i in E such that
   || h_i || = 1,  || h_i - z_i || < epsilon_i,
   support(z_i) subset [0, gamma),                             [SUCC-SUPPORT]
   support(z_i) subset C_k in the pure case,                    [SUCC-COLOR]
   z_1, ..., z_i are successive on C_k (pure case) and both
        ordinal and color successive (mixed case)               [SUCC-ORDER]
   for every i, support(z_i) is entirely in the ordinal tail
        above support(z_1) ... support(z_{i-1})                [SUCC-TAIL]

Moreover, the resulting sequence (z_i) is an admissible block sequence in the
sense of [W-ORDER]: nonzero, successive, supported on C_k or mixed-successive,
with 1/2 <= ||z_i|| <= 2 once normalized (which we can do without loss of
generality given ||h_i|| = 1 and ||h_i - z_i|| < 1/32000 << 1/2).

PROOF. We construct h_i, z_i inductively.

Inductive step. After z_1, ..., z_{i-1} are chosen, let beta < gamma lie
strictly above their supports; this is possible because gamma is a limit
ordinal and the supports of z_1, ..., z_{i-1} are finite subsets of [0, gamma).
For i = 1, take beta = 0.

In the mixed case, let l be the largest color used so far, with l = -1 at the
first step (so the sum over colors 0 <= j <= l is empty when l = -1).

Apply Lemma 10 (small restrictions of strictly singular operators) to the
strictly singular projection P_{<beta} restricted to H, and in the mixed case
also to the finitely many projections P_{C_j} restricted to H, 0 <= j <= l.
(These are strictly singular on infinite-dimensional closed subspaces because
they project onto "small" direct summands; this is part of the construction of
E.) Lemma 10 with a finite family of strictly singular operators gives a
closed infinite-dimensional subspace M_i subset H on which simultaneously
   || P_{<beta} h || < epsilon_i / 3                      for all h in M_i,
   sum_{j=0}^{l} || P_{C_j} h || < epsilon_i / 3           (mixed case).
The second sum is identically zero when l = -1. Choose a unit vector
h_i in M_i. Then h_i has
   || P_{<beta} h_i || < epsilon_i / 3,
   sum_{j=0}^{l} || P_{C_j} h_i || < epsilon_i / 3   (mixed case).

Trim the low part. In the pure case:
   w_i  =  h_i - P_{<beta} h_i  =  (Id - P_{<beta}) h_i,
and in the mixed case:
   w_i  =  h_i - P_{<beta} h_i - sum_{j=0}^{l} P_{C_j}(h_i - P_{<beta} h_i).
Each subtraction is by a contractive projection onto a direct summand, so
   || w_i ||  >=  || h_i || - || P_{<beta} h_i || - sum_{j=0}^{l} || P_{C_j} (...) ||
              >=  1 - epsilon_i / 3 - epsilon_i / 3
              >=  1 - 2 epsilon_i / 3.
Moreover, in the pure case w_i is supported above beta and below gamma, and
in C_k; in the mixed case it is supported above beta and in colors >= l+1,
below gamma.

Finite-support approximation. Crop w_i further to a finitely supported
approximation: the block span of w_i (over a carefully chosen finite set of
coordinates) is dense in w_i's projection. Choose z_i as a finitely supported
version of w_i satisfying support(z_i) in the same range (support(z_i) subset
[0, gamma), in C_k pure; and in ordinal and color tails above z_1..z_{i-1}),
with
   || z_i - w_i || < epsilon_i / 3.
This is possible because the finitely supported vectors are dense in E
(part (c) of Lemma 16).

Then
   || h_i - z_i ||  <=  || h_i - w_i || + || w_i - z_i ||
                    < epsilon_i / 3 + 2 epsilon_i / 3 + epsilon_i / 3
                    < epsilon_i.
(Adjust the decomposition slightly if needed for consistency.)

Support. By construction z_i is supported above support(z_1) ... support(z_{i-1})
on the ordinal axis, and in the mixed case above all previously used colors.
So z_i is successive (respectively, mixed-successive) to the previous z_1, ...,
z_{i-1}.

Norm. Since ||h_i|| = 1 and ||h_i - z_i|| < epsilon_i << 1/2, we get
   || z_i ||  >=  1 - epsilon_i  >=  1/2.
This proves Lemma 30.   []

7.2  The reduction: from F to a well-positioned copy.

We now record the structural lemma that drives all of Part 7. It is a
special-sequence style result on the underlying space E, and the proof
uses only the color-block structure of E (Section 4.5) together with the
elementary fact that infinite-dimensional subspaces of c_{00}-like spaces
either concentrate in a single direct summand or thread across them.

LEMMA 31 (reduction). Let F subset E be a closed infinite-dimensional subspace.
Then there exist

   - a family t, either a pure family k for some k >= 0, or the mixed
     family *,
   - a limit ordinal gamma < omega_1,
   - a closed infinite-dimensional subspace H subset F,
   - a bounded linear embedding U: H -> E,

such that the following hold.

   (R1) [LIFT] Every path functional P of the chosen family t whose support
        is contained in [0, gamma) (in C_k in the pure case) satisfies
           P( U h )  =  P( h )  for every h in H.
        Equivalently P o U = P as functionals on H.

   (R2) [BOUNDED INVERSES] There is a contractive projection R = R_t: E -> E
        of the form P_{<gamma} in the mixed case (R = P_{C_k} P_{<gamma} in the
        pure case) with R U = I_H.

   (R3) [NON-DEGENERACY] ||U|| <= K_F for some finite K_F depending only on F
        and t.

PROOF SKETCH. The idea is to find the family t and the set of colors that F
"sees" and then realize H as the part of F anchored to that family below a
large limit ordinal.

Two cases. Either F has, for some k, an infinite-dimensional image under
P_{C_k} P_{<gamma} for every gamma < omega_1, or it does not.

Case 1: some k. The images {P_{C_k} P_{<gamma}(F) : gamma < omega_1} are
increasing closed subspaces of E_{C_k}. Because the space E_{C_k} is not
"sigma-fragmented" (this follows from the c_{00}-density of finitely
supported vectors, Lemma 16(c)), there is gamma_0 such that the closed span
stabilizes: for gamma_0 <= gamma, P_{C_k} P_{<gamma}(F) has a fixed closed
infinite-dimensional subspace. Take a small perturbation of a block sequence
in that subspace to get a basic sequence (y_i) in F with support in [0, gamma_v)
intersected with C_k for a countable cofinal sequence (gamma_v). Then the choice
t = k, H = closed span of the y_i in F, and gamma = sup_v gamma_v satisfy
(R1)-(R3). The embedding U: H -> E is the inclusion (or any small perturbation
of it, chosen to land in the "clean" subspace P_{C_k} P_{<gamma}(E)); R = P_{C_k}
P_{<gamma}; R U = I_H since U = inclusion; (R1) holds because every path
functional of family k supported below gamma is annihilated by coordinate
functionals outside C_k ∩ [0, gamma), and U preserves H.

Case 2: no single k works. Then F "crosses" colors: for every gamma < omega_1
and every k, the projection P_{C_k} P_{<gamma} does not capture all of F.
Standard extraction then produces an infinite basic sequence (y_i) in F with
mixed-successive supports (ordinal and color) below some limit ordinal gamma.
Take t = *, H = closed span of the y_i, U = inclusion, R = P_{<gamma}; (R1)--
(R3) follow.

The "large enough gamma" condition and the "small perturbation" in both cases
use Lemma 10 (small restrictions of strictly singular operators): on the
complementary subspaces (coordinates above gamma, or outside C_k) the projection
is strictly singular, and we can avoid a tiny piece of F. This is exactly the
same approximation as in Lemma 30.   []

7.3  Building the binary tree of exact pairs.

Fix F. Choose a family t and H, U, R as in Lemma 31. Choose positive numbers
epsilon_i with sum_i epsilon_i <= 1/32000, and apply Lemma 30 (with H, gamma
from Lemma 31) to obtain unit vectors h_i in H and finitely supported z_i in E
with ||h_i - z_i|| < epsilon_i and successive z_i. Let Z = closed
span{z_i : i >= 1} subset E, an admissible block sequence space.

The bounded map V: Z -> H. Define V on the algebraic span of the z_i by
V z_i = h_i. This extends to a bounded linear map.

To see this, note first the fundamental coefficient bound for Z. Because the
z_i are successive finitely supported vectors, the ordinal interval projections
are contractive and give prefix projections of norm at most 1 on Z; combined
with 1/2 <= ||z_i|| <= 2 this implies, for every finite sum v = sum_i a_i z_i,
   |a_i|  <=  4 ||v||.                                    [COEF BOUND]
(Proof of [COEF BOUND]: choose m with |a_m| = max_i |a_i|. The interval
projections A_m and A_{m-1} onto [0, max supp z_m] and [0, max supp z_{m-1}]
are contractive, and A_m v - A_{m-1} v = a_m z_m. So |a_m| ||z_m|| <= 2 ||v||,
whence |a_m| <= 4 ||v||.)

With [COEF BOUND] in hand, for any finite sum v = sum_i a_i z_i,
   || V v ||  =  || sum_i a_i h_i ||
              <=  || sum_i a_i z_i ||  +  || sum_i a_i (h_i - z_i) ||
              <=  ||v||  +  (max_i |a_i|)  sum_i ||h_i - z_i||
              <=  ||v||  +  4 ||v|| (sum_i epsilon_i)
              <=  (1 + eta) ||v||,                        eta := 1/8000,
              [ using sum_i epsilon_i <= 1/32000, so 4 sum_i epsilon_i = eta ]
and
   || (V - I) v ||  <=  4 ||v|| (sum_i ||h_i - z_i||)
                    <=  eta ||v||.
Continuity extends V to a bounded linear map V: Z -> E with ||V - I|| <= eta
and ||V|| <= 1 + eta. The image lies in H because H is closed and V z_i = h_i
in H.

7.4  Binary tree construction.

Fix F as in Lemma 31. Choose a family t, H subset F, U: H -> E, R = R_t: E -> E
as in Lemma 31, and let Z, V: Z -> H be as in 7.3 with ||V - I|| <= eta = 1/8000
and ||V|| <= 1 + eta. Every path functional we build will be in the FAMILY t.

The tree of exact pairs. Let W = {0,1}^* be the set of all finite binary words,
and r denote the empty word (root). We construct, for each s in W, data
   ( y_s, phi_s, j_s, p_s, code_s )
where y_s is a finite block of the z-sequence, phi_s is a Type I piece of
weight j_s in family t, p_s is a metadata integer, and code_s encodes the
prefix r -> ... -> s (the pieces with their weights and metadata up to and
including s, at their order positions, no ordinal labels). The pieces along
any branch form an actual path of the family t.

Level 0 (root). Set j_r = 1. Apply Proposition pair:exact (6.5) to the
z-sequence and weight j_r = 1: get a finite block y_r and a Type I piece phi_r
of weight j_r = 1 with
   ||y_r|| <= 500,    phi_r(y_r) >= 1/2,    support(phi_r) in range(y_r)
(and in the color range of y_r in the mixed case).

Choose p_r as the least positive integer satisfying
   p_r >= j_r = 1,
   p_r >= max rho(supp(phi_r)),
no predecessor condition at the root. Set code_r to be the code of the
length-1 prefix phi_r with weight j_r and metadata p_r.

Inductive step. Suppose every node of W at every level < n has been chosen,
and let M_n denote the maximum of all z-indices used at levels < n.
(The set of nodes at each finite level is finite, so M_n is a finite integer.)

Fix a node s at level n with data (y_s, phi_s, j_s, p_s, code_s). Let s0 and
s1 denote its two children at level n+1. Both children receive the SAME
weight
   j_{s0}  =  j_{s1}  :=  sigma( code_s ).              [SIBLING WEIGHT]
Since sigma is an injection with sigma(code_s) > p_s (by the choice of sigma
and the metadata of code_s) and p_s >= j_s, the weights strictly increase:
   j_s  <  j_{s0}  =  j_{s1}.

For each child s' in {s0, s1}, apply Proposition pair:exact to the tail of the
z-sequence past M_n, with target weight j_{s'}, to get a finite block y_{s'}
and a Type I piece phi_{s'} of weight j_{s'} satisfying
   || y_{s'} || <= 500,    phi_{s'}(y_{s'}) >= 1/2,    support(phi_{s'}) in
   the ordinal range of y_{s'}, and in its color range in the mixed case.

Choose p_{s'} as the least positive integer satisfying
   p_{s'} > p_s                          [META-INCREASE]
   p_{s'} >= j_{s'}                       [META-VS-WEIGHT]
   p_{s'} >= max rho( union_{h on branch to s'} support(phi_h) )   [META-VS-RHO]
and set code_{s'} to be the code of the prefix through s'.

This completes the inductive step. The construction produces the whole tree,
since each level is finite (2^n nodes at level n) and the tree is locally
finite.

Every branch is a path. Fix b in {0, 1}^N, and consider its branch
   phi_r, phi_{b|1}, phi_{b|2}, phi_{b|3}, ...
with weights
   j_r, j_{b|1}, j_{b|2}, ...
and metadata
   p_r, p_{b|1}, p_{b|2}, ...
We verify the path rules:

   (i) Weight increase. j_r < j_{b|1} < j_{b|2} < ... strictly, by
       [SIBLING WEIGHT] and [META-VS-WEIGHT] with sigma increasing.

   (ii) Metadata increase. p_r < p_{b|1} < p_{b|2} < ... strictly, by
        [META-INCREASE].

   (iii) Metadata dominates weight. p_{b|n} >= j_{b|n} by [META-VS-WEIGHT].

   (iv) Metadata dominates max rho. p_{b|n} >= max rho of the union of
        supports through n, by [META-VS-RHO].

   (v) Coding rule. j_{b|n+1} = sigma(code of prefix through b|n) by
       [SIBLING WEIGHT].

   (vi) Succession. The blocks y_{b|n} come from successive tails of the
        z-sequence: each y_{b|n} is chosen past all previously used z-blocks,
        so the supports of phi_{b|n} form successive ordinal intervals (and
        mixed-successive color intervals in the mixed case).

   (vii) Weight-arrival check. The next weight j_{b|n+1} = sigma(code_{b|n})
         strictly exceeds p_{b|n}, which is at least the previously assigned
         metadata.

All path rules are therefore satisfied. The branch is an ACTUAL infinite path
of family t.

Caveat on siblings. Siblings s0 and s1 have the same weight and may have
overlapping supports (both drawn from the same tail past M_n). This causes no
conflict on any single path, because a path visits exactly one child (s0 or s1)
of s. The siblings occur at the same tree level but not on the same branch.

Type II disjointness. The disjoint-active-weight requirement in the Type II
rule places no restriction on INDIVIDUAL paths; it applies only when several
paths are combined in a Type II expression. The paths themselves are therefore
constructed independently; only when we use Type II (Lemma 20) do we discard
finitely many initial pieces to make the active weights disjoint.

The path functionals. For b in {0, 1}^N, define
   P_b  =  sum_{n=0}^{infty} phi_{b|n}.
The finite partial sums are Type II functionals with one path and coefficient
one, hence lie in the family t with norm at most one. By Lemma 19, the sum
converges on E and defines a member of B_{E^*}. Each phi_{b|n} is supported on
the ordinal interval of y_{b|n} (and in the color range of y_{b|n} in the mixed
case), and the whole path support sits below gamma (Lemma 30's [SUCC-SUPPORT])
with the pure-k or mixed-family structure. So the lift identity [LIFT] of
Lemma 31 applies to every P_b:

   P_b o U  =  P_b        (functionals on H).               [LIFT-BRANCH]

7.5  The separation theorem.

THEOREM (branch:separation). For every closed infinite-dimensional subspace
F subset E, there exist a family t, a number delta_F > 0, and path functionals
P_b in B_{E^*}, indexed by b in {0,1}^N, all of the family t, such that
   || P_b|_F  -  P_c|_F ||  >=  delta_F       for every b != c.

PROOF. Take family t, H, U, R from Lemma 31 and the tree of 7.4. Let
delta_F := 3 / (8 * 500 * (1 + eta)).

Fix b != c in {0, 1}^N. Let t_0 be their longest common initial word, so b
and c first diverge AFTER t_0 (say b through t_0 0 and c through t_0 1).
Choose a node s on branch b with level |s| strictly greater than |t_0|.

Cross-evaluation at y_s.
   - P_b(y_s). Look at the terms phi_{b|k}(y_s), k = 0, 1, 2, ...
       k < |s|: supp(y_s) sits in the tail past M_{|s|}, which is above all
                blocks at levels < |s|, so supp(phi_{b|k}) is below supp(y_s);
                cross evaluation is zero.
       k = |s|: phi_{b|k} = phi_s, and phi_s(y_s) >= 1/2 by construction.
       k > |s|: supp(y_{b|k}) sits in a tail past M_{|s|+k-|s|} > M_{|s|},
                above supp(y_s); so phi_{b|k}(y_s) = 0.
     Therefore P_b(y_s) = phi_s(y_s) >= 1/2.

   - P_c(y_s). For k = 0, 1, ..., |t_0|: supp(phi_{c|k}) = supp(phi_{b|k})
     below supp(y_s); cross evaluation is zero. For k > |t_0|: c diverges from
     b at level |t_0|+1, so phi_{c|k} is drawn from a tail disjoint from
     supp(y_s); cross evaluation is zero. Therefore P_c(y_s) = 0.

Perturbation. We test with V y_s in H subset F:
   (P_b - P_c)(V y_s)  =  (P_b - P_c)(y_s) + (P_b - P_c)(V y_s - y_s)
                       =  phi_s(y_s) + (P_b - P_c)(V y_s - y_s).
Bound the correction: ||P_b|| <= 1 and ||P_c|| <= 1 by Lemma 19; and
||V y_s - y_s|| <= eta ||y_s|| <= 500 eta. So
   |(P_b - P_c)(V y_s - y_s)|  <=  (||P_b|| + ||P_c||) ||V y_s - y_s||
                               <=  2 * 500 * eta
                               =  1000 / 8000
                               =  1/8.
And ||V y_s|| <= (1 + eta) ||y_s|| <= 500 (1 + eta). So
   |(P_b - P_c)(V y_s)| / ||V y_s||
     >= (phi_s(y_s) - 1/8) / (500 (1 + eta))
     = (1/2 - 1/8) / (500 (1 + eta))
     = 3 / (8 * 500 * (1 + eta))  =  delta_F.

Since V y_s is in H subset F, the left side equals at most ||P_b|_F - P_c|_F||:
   ||P_b|_F - P_c|_F||  >=  |(P_b - P_c)(V y_s)| / ||V y_s||
                          >=  delta_F.

This holds for every pair b != c. So Theorem branch:separation is proved.   []


==============================================================================
PART 8.  CHANGING THE PREDUAL: THE COUNTEREXAMPLE
==============================================================================

8.0  The idea in one paragraph.

Under CH, the space E of Part 4 is itself a dual of a coordinate predual X_0
(Proposition 18: E = X_0^* isometrically). But X_0 is "too nice"; on each of
its separable subspaces, the coordinate evaluations form a separable set. We
need a DIFFERENT predual of E whose evaluation image is NOT separable in any
separable F. The strategy is the following. Take the huge supply of path
functionals P_b in B_{E^*} produced by Part 7. They are separated by delta_F on
every infinite-dimensional F. Modify the quotient map Q: E^* -> E^*/X_0 by a
"small twist" B (bounded operator of norm at most 1/10) that captures the path
functionals: B(X_0) should be dense in the closed span V of path cosets.
The new predual X = ker(Q - B) is then a Banach space with X^* = E, and B(X)
is dense in V. Because path functionals map "generically" into V modulo X_0,
the evaluations of X on any separable F are essentially the same as path
functionals, and those are separated by delta_F; by the evaluation criterion,
X has no separable infinite-dimensional quotient.

The construction is technical but the idea is clean. Everything revolves
around the following Banach space lemma.

8.1  A small perturbation of a quotient map.

LEMMA 32 (twist:lemma). Let Y be a closed subspace of E^* such that the
evaluation map E -> Y^* is an isometric isomorphism. Set W = E^*/Y and let
Q: E^* -> W be the quotient map. Let B: E^* -> W be a bounded linear map
satisfying

   [TW-B-NORM]  ||B|| <= 1/10,
   [TW-B-ADJ ]  B^*(W^*) subset J_E(E),
   [TW-B-V   ]  B(E^*) subset V := norm closure of B(Y) in W.

Then X := ker(Q - B) is a closed subspace of E^*, hence a Banach space, and
the evaluation map E -> X^*, e |-> (x |-> x(e)), is an isomorphism of Banach
spaces. Furthermore, cl(B(X)) = V.

PROOF. Write L = Q - B and b = ||B||, so b <= 1/10.

Lift estimate. Every w in W has a Q-lift with norm at most (11/10)||w||.
(Indeed W = E^*/Y is the quotient of a Banach space by a closed subspace, and
the quotient norm gives Q-lifts of norm exactly ||w||; to allow the extra
bounded perturbation we only need the bound 11/10.) Starting with such a lift
y_0 of w, set e_0 = B y_0 and lift e_0 to y_1 with ||y_1|| <= (11/10)||e_0||;
set e_1 = B y_1 and lift it to y_2, and so on. The partial sums form a Cauchy
sequence because the ratio between consecutive blocks is at most (11/10) b <
1. Summing gives an element y = sum_{n=0}^{infty} y_n in E^* with
   Ly  =  sum_n (Q y_n - B y_n)  =  w  -  sum_n (e_n - e_{n+1})  =  w.
The norm bound is
   ||y||  <=  ||y_0|| sum_n ( (11/10) b )^n  <=  (11/10) ||w|| / (1 - (11/10) b).

Set
   C  :=  (11/10) / (1 - (11/10) b).
Then for every w in W there is an x in E^* with L x = w and ||x|| <= C ||w||.
This proves that L is a bounded surjection E^* -> W. In particular, L has
closed image and the first isomorphism theorem applies:
   X^perp  =  (ker L)^perp  =  image(L^*)  =  { Q^* w^* - B^* w^* : w^* in W^* }.
                                     [TW-XPERP]

Decomposition of E^{**}. The evaluation map E -> Y^* is an isometric
isomorphism by hypothesis. Thus every z in E^{**} restricts to an element of
Y^* which is the evaluation by a unique e in E; subtracting J_E(e) leaves an
element of Y^perp = { u in E^{**} : u(y) = 0 for all y in Y }. The two
subspaces are closed; their intersection is zero; and they sum to E^{**}.
Therefore
   E^{**}  =  Y^perp  +  J_E(E)   (direct sum).               [TW-DECOMP]
Moreover, since Q is surjective with kernel Y, the adjoint Q^*: W^* -> Y^perp
is an isometric isomorphism.

Subspace X^perp is a graph over Y^perp. By [TW-XPERP] and [TW-B-ADJ], each
element of X^perp has the form Q^* w^* - B^* w^* with the first summand in
Y^perp (via Q^*W^* = Y^perp) and the second summand in J_E(E) (by B^*W^* subset
J_E(E)). Conversely, for any u in Y^perp, u = Q^* w^* for a unique w^* in W^*,
and B^* w^* is in J_E(E). So
   X^perp  =  { (u, -B^* (Q^*)^{-1} u) : u in Y^perp }  subset  Y^perp + J_E(E).
This is the graph of a bounded linear map Y^perp -> J_E(E). Consequently
   E^{**} / X^perp  is  canonically isomorphic to  J_E(E) = E.       [TW-QUOT]

Identification of X^* with E. The quotient E^{**}/X^perp identifies with X^*
(the canonical isomorphism X^* = E^{**}/X^perp, valid for every Banach space X
via the double dual). Combined with [TW-QUOT], we get a canonical vector space
isomorphism X^* -> E. The quotient map E^{**} -> E^{**}/X^perp is bounded with
norm one, and the identification Y^perp -> J_E(E) is bounded with bounded
inverse (the graph map); by the open mapping theorem, the induced isomorphism
X^* -> E is bounded with bounded inverse. Therefore X^* and E are isomorphic
as Banach spaces. The map E -> X^* explicitly is e |-> (x |-> x(e)), and this
is the adjoint of the inclusion X -> E^*; it is the natural evaluation map.

Density of B(X) in V. First, B(X) subset B(E^*) subset V = cl(B(Y)) by
[TW-B-V], so cl(B(X)) subset V. For the reverse, fix y in Y subset E^* = X^{**}.
By Goldstine's theorem, there is a net x_i in X converging weak-star to y in
X^{**} (equivalently, in the weak topology of E^* = X^{**}). Now B is the
adjoint of the bounded map B^*|_{X^*}: W^* -> X^* (which is bounded into X^* by
[TW-B-ADJ]): B = (B^*|_{X^*})^*. An adjoint map is weak-star-to-weak
continuous on the double dual. So B x_i converges to B y weakly in W. Since
closed convex sets in Banach spaces are weakly closed, the limit By lies in the
weak closure, hence in the norm closure, of B(X). Thus B(Y) subset cl(B(X)),
so V = cl(B(Y)) subset cl(B(X)). Combining both inclusions, cl(B(X)) = V.
This proves Lemma 32.   []

8.2  Constructing the operator B.

We now build the operator B that the twist:lemma needs. The construction works
under CH (in Part 9 the hypothesis will be that CH holds), so aleph_1 = c and
there are aleph_1 many path functionals per family.

8.2.1  Labels for the paths.

For each family t (pure k or mixed *), let P_t denote the set of ACTUAL
infinite paths of family t, i.e., the paths constructed in Section 5.2. Under
CH, |P_t| <= aleph_1 (each path is determined by countably many rational data).

We need to assign to each path P in P_t a distinct ordinal label. Assign:
   - for pure family k: labels in C_{k+1};
   - for the mixed family *: labels in C_1.

But C_1 also picks up labels for pure family 0. Split C_1 into two disjoint
sets of cardinality aleph_1 and use one for the mixed family. Then define
injections
   iota_k: P_k -> C_{k+1},        iota_*: P_* -> C_1,
whose ranges are mutually disjoint.

Set
   s_src(k) = s_{k+1}   for pure family k,
   s_src(*) = s_1       for the mixed family *.
By the choice of parameters in 4.2, s_src(t)' <= q_t for every family t.

8.2.2  The family-specific maps b_t and S_t.

For y in E^* define the vector of "path-coordinate evaluations"
   b_t(y)  =  ( y(e_{iota_t(P)}) )_{P in P_t}.              [B-DEF]
This is a scalar-valued function on the path set P_t.

The evaluation bound. In the pure case, b_t(y) is the restriction of the C_{k+1}
coordinate evaluations y |-> (y(e_alpha))_{alpha in C_{k+1}} to the image
iota_k(P_k) subset C_{k+1}; so by the pure-coordinate estimate of Lemma 17
(ch:coordinates) followed by finite-dim duality (extending a functional from
the indices iota_k(P_k) to all of C_{k+1}) and passing to a supremum over
finite subsets, we get
   || b_t(y) ||_{s_src(t)'}  <=  || y ||_{E^*}.             [B-COORD]
Since s_src(t)' <= q_t (monotonicity of l_p norms), it follows that
   || b_t(y) ||_{q_t}  <=  || y ||_{E^*}.                   [B-Q]
In the mixed case the argument is identical, using that C_1 is partitioned
between labels of family * and labels that are not yet in use.

The map S_t: l_{q_t}(P_t) -> W. Define S_t on the finitely supported vectors
by
   S_t( (c_P) )  =  sum_P c_P QP,      c_P = 0 for all but finitely many P.
Here Q: E^* -> W = E^*/X_0 is the quotient map of 8.1 (with Y = X_0).

Boundedness of S_t. By the Type II construction of Part 5 and by the tail
estimate of Lemma 20, finite sums satisfy
   || sum_P c_P QP ||_W  <=  || (c_P) ||_{q_t}
for rational coefficients unit in l_{q_t}, and then for real coefficients by
approximation. Consequently S_t extends by continuity to a bounded linear map
   S_t: l_{q_t}(P_t) -> W,   || S_t || <= 1.               [S-BOUND]
Its image lies in the closed span V of {QP : P in P_t, t a family}.

8.2.3  The operator B.

Choose positive numbers (tau_t) over the countably many families t with
   sum_t tau_t  <=  1/10.                                  [TAU-2]
Define B: E^* -> W by
   B y  =  sum_t tau_t S_t b_t(y),          y in E^*.        [B-SUM]
This series converges because each ||S_t b_t(y)|| <= ||b_t(y)||_{q_t} <= ||y||
and sum tau_t <= 1/10.

Norm bound. For y in E^*,
   ||B y||_W  <=  sum_t tau_t || S_t b_t(y) ||_W
              <=  sum_t tau_t || b_t(y) ||_{q_t}
              <=  (sum_t tau_t) ||y||_E^*
              <=  (1/10) ||y||.
So ||B|| <= 1/10.  [TW-B-NORM] holds.

Adjoint condition. Since B is the sum over paths of (P |-> QP) multiplied by
coordinate projections (y |-> y(e_{iota_t(P)})) and the scalar tau_t, the
adjoint B^*: W^* -> E^{**} is a sum of terms of the form
   w^* |-> sum_P tau_t <w^*, QP> e_{iota_t(P)}^{**}.
Each e_{iota_t(P)}^{**} is the canonical image J_E(e_{iota_t(P)}) ∈ J_E(E). So
the image of B^* lies in J_E(E):
   B^*(W^*)  subset  J_E(E).                                [TW-B-ADJ]

Codomain condition. For y in E^*, each term S_t b_t(y) lies in V (by finite
approximation and closedness of V). Summing with the bounded coefficients
tau_t keeps us in V, so
   B(E^*)  subset  V.                                       [TW-B-V]

Density of B(X_0) in V. For a coordinate functional e_alpha^* ∈ X_0, the
path-coordinate evaluation is b_t(e_alpha^*) = (delta_{alpha, iota_t(P)})_P,
and S_t applied to it is
   S_t b_t(e_alpha^*)  =  sum_{P : iota_t(P) = alpha} QP  =  QP_alpha
where P_alpha is the (unique) path of family t with label alpha (when alpha is
in the range of iota_t), and 0 otherwise. Thus B(e_alpha^*) equals tau_{t(alpha)}
QP_alpha, with t(alpha) determined by which family's label set contains alpha.

Take the linear span of {B(e_alpha^*) : alpha in Gamma}:
   span{ tau_t QP : P in P_t, t a family }.
Since each tau_t > 0, this is the same span as span{QP : P in P_t, t a family},
whose closure is V. Hence
   cl( B(X_0) )  =  V.                                       [B-X0-DENSE]

That will turn out to be exactly [TW-B-V] upgraded to an equality: B(X_0) is
already dense in V.

8.2.4  Verifying the twist:lemma, and the predual X.

Take Y = X_0 (a closed subspace of E^*). By Proposition 18 the evaluation map
E -> Y^* = X_0^* is an isometric isomorphism. Take W = E^*/X_0 and the quotient
map Q as in 8.1. Take B as constructed in 8.2.3.

The three conditions of Lemma 32 are verified by [TW-B-NORM], [TW-B-ADJ], and
[TW-B-V], so we may set
   X  =  ker(Q - B)  subset  E^*,                           [B-X-DEF]
a closed subspace of E^*, and Lemma 32 gives an isometric isomorphism
   ev: E  ->  X^*,  e |-> (x |-> x(e)).                     [B-EVAL]

Every element of X is a specific functional on E = X^*. Thus X is a predual of
E. We now show that X has no separable infinite-dimensional quotient.

8.3  The counterexample (no separable quotient under CH).

THEOREM (twist:counterexample). Under CH there is an infinite-dimensional real
Banach space X with no separable infinite-dimensional quotient.

PROOF. Construct X = ker(Q - B) as in 8.2.4. We have the isometric isomorphism
[B-EVAL] identifying E with X^*. Since E is infinite-dimensional, so is X.

We show that every closed infinite-dimensional separable F subset E = X^* has
a NON-separable evaluation image R_F(X) in F^*. By the evaluation criterion
(Proposition 2), this excludes all separable infinite-dimensional quotients.

Setup for F. Fix F, a closed infinite-dimensional separable subspace of
E = X^*. Put
   C_F  :=  norm closure of { y|_F : y in X_0 }  in F^*.
Because X_0 is the closed span of the coordinate functionals (e_alpha^*) and a
countable dense subset of F is supported on a common countable set of
coordinates, all coordinate functionals vanish on the complement of a countable
set. So X_0|_F ⊆ cl span of a countable family, and C_F is separable.

The map T_F. Define
   T_F: W -> F^*/C_F,     T_F( Qy )  =  y|_F + C_F          [T-F-DEF]
for y in E^*. This is well-defined because Qy_1 = Qy_2 iff y_1 - y_2 in X_0,
and (y_1 - y_2)|_F ∈ C_F for y_1 - y_2 ∈ X_0. And it is a bounded linear map
(T_F is the composition of the restriction E^* -> F^* with the quotient map
F^* -> F^*/C_F, with kernel X_0).

T_F(V) is nonseparable. Recall V = cl span{ QP : P in P_t, t a family }. By
Theorem branch:separation (Part 7), applied to F, there is a family t and
delta_F > 0 and path functionals P_b in B_{E^*}, one for each b in {0, 1}^N,
all of family t, with
   || P_b|_F  -  P_c|_F ||  >=  delta_F       for every b != c.

Suppose T_F(V) were separable with closure M ⊆ F^*/C_F. Let Y_M ⊆ F^* denote
the inverse image of M under the quotient map pi: F^* -> F^*/C_F. We claim
Y_M is separable. Indeed: lift a countable dense subset (m_n) of M to elements
u_n ∈ F^*, and fix a countable dense subset (c_j) of C_F. For any z ∈ Y_M,
first pi(z) is close to some m_n, and then z - u_n is close to an element of
C_F (because both have the same image under pi and the quotient norm equals
infimum distance), which in turn is close to some c_j. So the countable set
{u_n + c_j} is dense in Y_M.

Now: every path restriction P_b|_F lies in Y_M, because T_F(QP_b) ∈ M by
definition of M (T_F(QP_b) is the image of QP_b in T_F(V) ⊆ M). Since P_b|_F
and P_c|_F are delta_F-separated in F^*, and Y_M is separable, we have a
contradiction (a separable metric space cannot contain an uncountable set of
pairs at mutual distance at least delta_F). Therefore T_F(V) is nonseparable.

R_F(X) is nonseparable. We have B(X) dense in V by [twist:lemma] and 8.2.3.
So T_F(B(X)) is dense in T_F(V), which is nonseparable; hence T_F(B(X)) is
nonseparable.

On the other hand, for x ∈ X, we have (Q - B)x = 0, i.e. Qx = Bx, so
   T_F(Qx)  =  (Qx)|_F + C_F  =  (x|_F) + C_F.
And Bx = Qx (as elements of W = E^*/X_0). Thus B(X) = Q(X) = X + X_0 (mod X_0).

Therefore
   T_F(B(X))  =  { x|_F + C_F : x in X }  =  R_F(X) + C_F,
where R_F(X) ⊆ F^* is the image of X under evaluation at F, and + C_F means
sum in the quotient F^*/C_F.

If R_F(X) were separable (in F^*), then R_F(X) + C_F would be separable
(sum of two separable sets). But T_F(B(X)) = R_F(X) + C_F (as elements of
F^*/C_F) is nonseparable. Contradiction.

Hence R_F(X) is nonseparable. Since F was arbitrary, the evaluation criterion
(Proposition 2) gives: X has no separable infinite-dimensional quotient.
This proves Theorem twist:counterexample.   []

8.4  The counterexample has norm density aleph_1.

To close Part 8, we note that the permissive structure of B gives X the
smallest possible nonseparable density.

COROLLARY (twist:density). Under CH, the space X of Theorem twist:counterexample
has norm density aleph_1.

PROOF. Define the map Phi: X -> X_0 as follows. For x ∈ X, set
   Phi(x)  =  x  -  lift(Bx),
where lift(w) ∈ E^* is a "short" Q-lift of w (with norm at most (11/10)||w||,
as in the lift lemma of 8.1). Then
   Q(Phi(x))  =  Qx - Q(lift(Bx))  =  Bx - Bx  =  0,
so Phi(x) ∈ ker Q = X_0.

Bounded linearity. The map x |-> lift(Bx) is bounded linear (lift is bounded
linear "up to choice", and B, Q are bounded linear); so Phi is a bounded linear
map X -> X_0.

Lower bound. For x ∈ X, by the triangle inequality,
   ||Phi(x)||  >=  ||x||  -  ||lift(Bx)||
              >=  ||x||  -  (11/10)||Bx||
              >=  ||x||  -  (11/10)(1/10)||x||
              =  (89/100) ||x||.
So Phi is injective and has bounded inverse Phi^{-1}: X_0 -> X bounded by
(100/89)||.|| on its image. Combined with the open mapping theorem (or the
explicit bound), Phi is a Banach space isomorphism X -> X_0.

Density. Since Phi is a Banach space isomorphism, X and X_0 have the same
density. And X_0 = closed span{e_alpha^* : alpha in Gamma} has density aleph_1:
its countable-dense sets contain 1-separated families of size aleph_1
(distinct coordinate functionals e_alpha^* are 1-separated in the dual norm).
Therefore density(X) = aleph_1.   []

This closes the negative direction over the reals. By Corollary 13
(complexification), the corresponding complex Banach space X_C is a complex
counterexample. This completes the proof of the CH half of the main theorem
over both fields.


==============================================================================
PART 9.  SET-THEORETIC MODELS: PUTTING THE TWO SIDES TOGETHER
==============================================================================

9.0  What this part does.

We have two model-theoretic inputs to build:

(A) In a model of ZFC with a real-valued measurable cardinal, the measure
    hypothesis of Part 2 holds at kappa = c, giving the POSITIVE side.

(B) In a model of CH (any model), the negative side of Parts 4-8 gives a
    counterexample.

Both of these are relative consistency statements. We first record Solovay's
preservation theorem, which produces a model satisfying (A) from a measurable
cardinal.

9.1  Solovay's preservation.

The following is proved in Solovay's 1971 paper "Real-valued measurable
cardinals", in the formulation recorded in Caicedo 2006 (Fact 1.27).

THEOREM (Solovay). If kappa is real-valued measurable, then forcing with a
measure algebra preserves its real-valued measurability. In particular, in the
extension there is a kappa-additive probability measure on the FULL power set
of kappa in that extension, vanishing on singletons.

Here a measure algebra is the Boolean algebra of measurable sets modulo null
sets of a probability space, with zero omitted when it is used as a forcing
notion. The special case of the theorem used below also has a direct proof in
Fuchino-Greenberg-Shelah (2006, Section 2, Lemmas 2.1-2.4). That construction
measures every subset of kappa in the extension, is countably additive, and
makes unions of fewer than kappa null sets null. These properties give the
stated additivity: in a disjoint family of size less than kappa, only countably
many members have positive measure, and the union of the remaining members is
null.

9.2  From a measurable cardinal to a real-valued measurable continuum.

PROPOSITION (model:positive). If ZFC with a measurable cardinal is consistent,
then ZFC with a real-valued measurable continuum is consistent.

PROOF. Let us first extract the cardinal structure we will need. Work in a
ground model of ZFC with a measurable cardinal kappa. A kappa-complete
nonprincipal ultrafilter on kappa gives a {0, 1}-valued probability measure
witnessing its real-valued measurability.

Cardinal structure of kappa.

(a) kappa is a regular cardinal. Indeed, sets of size less than kappa are null,
so a cofinal union of fewer than kappa such sets cannot cover kappa (that union
would be null, and kappa is not null).

(b) kappa is a strong limit. Suppose some lambda < kappa had an injection
e: kappa -> P(lambda) into its power set. For each xi < lambda, the ultrafilter
chooses one of the two sets on which the statement "xi is in e(alpha)" is
constant; their intersection belongs to the ultrafilter by kappa-completeness,
although injectivity of e makes that intersection have at most one element,
which contradicts kappa > 1.

(c) Every countable sequence of ordinals below kappa is bounded, and hence
   kappa^{aleph_0}  =  kappa.
    For each lambda < kappa, lambda^{aleph_0} <= 2^{max(lambda, aleph_0)} <
    kappa, so the sum over lambda < kappa of lambda^{aleph_0} is at most kappa.
    The reverse inequality kappa <= kappa^{aleph_0} is immediate.

The forcing. Let P be the measure algebra of the ordinary product measure on
2^kappa (equivalently, on the countable-support cylinder sigma-algebra). Force
with P. The forcing is ccc (it is a measure algebra of a probability space),
hence preserves cardinals. In the extension:

   - kappa remains a cardinal;
   - forcing with a measure algebra preserves real-valued measurability by
     Solovay's theorem above, so kappa remains real-valued measurable;
   - since the forcing is ccc hence preserves cardinals and cofinalities, and
     since the continuum c becomes at most kappa in the extension (the forcing
     has size <= kappa, so c <= kappa), we have c <= kappa.

Two cases. If c = kappa, then c is real-valued measurable in the extension; we
are done. If c < kappa, then kappa is not the continuum. But the measure
hypothesis we used in Part 2 concerns the full power set of c. We must check
that the c-additive measure on P(c) survives.

Actually, the measure hypothesis needed for Part 2 is on c, not on kappa. The
key point: kappa remains real-valued measurable, and c <= kappa. The natural
map c -> kappa identifies c with an initial segment of kappa, and the
kappa-additive measure restricted to this initial segment gives a
kappa-additive probability measure on P(c) that still lives in the extension.

However, the c-additive measure from Step (c) requires the measure on subsets
of c, not just kappa. In the forcing extension, by the direct construction of
Fuchino-Greenberg-Shelah, every subset of kappa is measurable with the
kappa-additive measure. Therefore, every subset of c (which is a subset of
kappa) is measurable with the same measure, and the restriction of the
kappa-additive measure to P(c) is a kappa-additive probability measure.

The crucial point: on the cardinal c, a kappa-additive probability measure is
also c-additive (finite c is well inside kappa, and c-additive is implied by
kappa-additive whenever kappa >= c: for a disjoint family of size < c, the
union is a disjoint family of size < c <= kappa, so fewer than kappa many
positive-measure sets, so the additivity passes down to c).

So in the extension, the cardinal c carries a c-additive probability measure on
its full power set that vanishes on singletons. This is exactly the measure
hypothesis (M1)-(M4) needed in Part 2. Part 2 then gives the positive side:
every infinite-dimensional real Banach space has a separable
infinite-dimensional quotient. Combined with Proposition 11 (positive
transfer), this gives the same over the complex field as well.

Connecting the relative-consistency statement. Solovay's theorem needs a
ground model with a real-valued measurable cardinal, which we only get from a
measurable cardinal. So the consistency hypothesis is exactly
"ZFC + measurable cardinal", and the output model is "ZFC + real-valued
measurable continuum". This proves Proposition model:positive.   []

9.3  Martin's axiom and b > aleph_1.

The positive direction at the smaller density aleph_1 uses a combinatorial
fact worth recording.

PROPOSITION (b-under-MA). Under Martin's axiom MA and c = aleph_2, the bounding
number b satisfies b > aleph_1.

PROOF. Suppose, for contradiction, that A = {f_alpha : alpha < aleph_1} is an
unbounded family of functions N -> N in the mod-finite order.

Conditions. A condition is a pair (s, F) where s is a finite partial function
N -> N, identified with its sequence (s(0), ..., s(l_s - 1)) for l_s = |dom s|,
and F is a finite subset of aleph_1. Say (s', F') extends (s, F), written
(s', F') <= (s, F), when s' end-extends s (so l_{s'} >= l_s and s' agrees with
s on dom s), F' contains F, and for every alpha in F and every n with
l_s <= n < l_{s'} one has f_alpha(n) < s'(n).

This is a partial order: transitivity is checked directly, because the
domination clause for a composite extension splits into the two steps.

ccc. Let {(s_i, F_i) : i < aleph_1} be any family of conditions. Thinning by
the pigeonhole principle, all s_i may be assumed to have the same length l and
all F_i the same cardinality m. For fixed l there are only countably many
possible stems s, so thin again until all s_i equal one fixed stem s. Now take
any two, (s, F) and (s, F'). The condition (s, F union F') extends both: the
domination clause only tests coordinates n with l_s <= n < l_s, and there are
none. So any two conditions with equal stems are compatible, hence the poset is
ccc.

Dense sets. For alpha < aleph_1 the set D_alpha of conditions with alpha in F
is dense: pass from (s, F) to (s, F union {alpha}). For n in N the set E_n of
conditions with l_s >= n is dense: extend s to a longer stem, enlarging F as
needed and meeting the domination clause by choosing the new values of s' large.

Filter. Under MA with c = aleph_2 > aleph_1, Martin's axiom at aleph_1 holds,
so the aleph_1 many dense sets {D_alpha : alpha < aleph_1} and {E_n : n in N}
can all be met by one filter G.

The dominating function. Since G is a filter, any two conditions in it have a
common lower bound in G extending both, so the stems occurring in G are
pairwise compatible end-extensions and their union g: N -> N is a well-defined
function. Fix alpha < aleph_1. By density of D_alpha choose p = (s, F) in G
with alpha in F, and put l = l_s. For m >= l, density of E_{m+1} gives
q = (t, F') in G with l_t > m, and directedness gives r = (u, F'') in G with
r <= p and r <= q. The domination clause of r <= p applies to n = m, since
l_s = l <= m < l_u, so f_alpha(m) < u(m); and u(m) = t(m) = g(m) because u
end-extends both s and t. Hence f_alpha <=* g for every alpha < aleph_1, so A is
bounded. This contradiction shows b > aleph_1.   []

COROLLARY (density criterion at aleph_1). Assume MA + c = aleph_2. Then every
infinite-dimensional Banach space of norm density aleph_1 has a separable
infinite-dimensional quotient.

PROOF. Saxon and Sanchez-Ruiz (1994) proved that every infinite-dimensional
Banach space X whose norm density d(X) is strictly less than the bounding
number b admits a separable infinite-dimensional quotient. Under MA together
with c = aleph_2 we have b = c = aleph_2, and Proposition b-under-MA upgrades
this to b = aleph_2 > aleph_1. Every infinite-dimensional Banach space of norm
density aleph_1 therefore satisfies d(X) = aleph_1 < b, so the Saxon-Sanchez
Ruiz criterion supplies a separable infinite-dimensional quotient.   []

9.4  The CH model: failure of SQ.

CH is consistent with ZFC. In Godel's constructible universe L one has GCH,
hence CH, giving
   Con(ZFC)  =>  Con(ZFC + CH)
(Kunen 1980, Chapter IV; the same via the forcing interpretation).

Work in a model of ZFC + CH. Then c = aleph_1, and Parts 4-8 build an
infinite-dimensional real Banach space X with no separable infinite-dimensional
quotient (Theorem twist:counterexample). Corollary 13 (complexification) turns
X into an infinite-dimensional complex Banach space X_C with no separable
infinite-dimensional complex quotient. So in this model both SQ_R and SQ_C
fail.

9.5  The main theorem.

THEOREM (intro:main). For each field F in {R, C}, ZFC proves the following
two implications.

   (i)  If the continuum c is real-valued measurable, then every
        infinite-dimensional Banach space over F has a separable
        infinite-dimensional quotient. Denote this assertion SQ_F.

   (ii) If the continuum hypothesis holds, then there is an
        infinite-dimensional Banach space over F with no separable
        infinite-dimensional quotient, i.e. SQ_F fails.

Consequently, if ZFC together with a measurable cardinal is consistent, then
SQ_F is independent of ZFC. Consistency of its failure requires only Con(ZFC).

PROOF. (i) over R is Theorem 9 of Part 2. The transfer from R to C is
Proposition 11 of Part 3. (ii) over R is Theorem twist:counterexample of Part 8;
over C it is Corollary 13 (complexification). For the consistency consequences:
Proposition model:positive of 9.2 produces, from a measurable cardinal, a model
of ZFC in which c is real-valued measurable, so that (i) holds there; and 9.4
produces, from Con(ZFC) alone, a model of CH in which (ii) holds, i.e. SQ_F
fails. Therefore SQ_F is independent of ZFC relative to a measurable cardinal,
and its failure is consistent with ZFC alone.   []

9.6  Independence at the smallest nonseparable density.

Write SQ_F^{aleph_1} for the assertion: every infinite-dimensional Banach space
over F of norm density exactly aleph_1 has a separable infinite-dimensional
quotient.

COROLLARY (intro:small-density). If ZFC is consistent, then SQ_F^{aleph_1} is
independent of ZFC for each F in {R, C}.

PROOF. Positive side. Starting from a model of ZFC and GCH, the forcing
construction of Kunen (1980, Chapter VIII, Theorem 6.3) gives a model of
   MA + c = aleph_2.
In that model, the density criterion at aleph_1 (9.3) applies: every
infinite-dimensional Banach space of norm density aleph_1 has a separable
infinite-dimensional quotient. This is the real statement; for complex spaces,
Proposition 11 applies, because a complex Banach space has the same norm
density as its underlying real space. So SQ_F^{aleph_1} holds in this model.
Relative consistency: Godel's constructible-universe theorem together with the
forcing interpretation gives
   Con(ZFC)  =>  Con(ZFC + MA + c = aleph_2).

Negative side. In a model of CH (which exists from Con(ZFC) alone), the space
X of Theorem twist:counterexample has no separable infinite-dimensional
quotient and, by Corollary twist:density, has norm density aleph_1. Its
complexification has the same two properties over C. So SQ_F^{aleph_1} fails in
this model.

These are two models, both relative to Con(ZFC) alone, that satisfy the two
sides. Hence, as a relative-consistency statement, SQ_F^{aleph_1} is independent
of ZFC. Explicitly, for each F in {R, C},
   Con(ZFC) => Con(ZFC + SQ_F^{aleph_1}),
   Con(ZFC) => Con(ZFC + not SQ_F^{aleph_1}).   []

9.7  Remarks.

(a) The counterexamples of (ii) already occur at norm density aleph_1, the
smallest possible nonseparable density (Corollary twist:density and Corollary
intro:small-density). So the failure side is as economical as a nonseparable
space can be: every witnessed violation lives at the very first density where a
space can fail to be separable.

(b) The positive side genuinely needs the strong measure on c: with Con(ZFC)
alone, the CH model shows that failure is consistent. So Theorem intro:main (i)
cannot be proved in ZFC without the measure hypothesis.

(c) The construction of E in Part 4 does two jobs at once. The pure-family
lengths satisfy s_{k+1}' <= q_k < s_k' and s_k = k + 2, so that on one hand the
coordinate evaluations obey the pure-coordinate estimate in l_{s_k} while the
paths obey their l_{q_k} estimate modulo the coordinate span. The rigid coding
map sigma (Section 4.5) is what makes path combinations possible at all: two
distinct paths with a common weight share the same preceding compressed code
and hence coincide (Lemma 20), so two distinct paths share only finitely many
weights. That rigidity is exactly what lets the exact-pair Proposition of Part 6
supply a finite block y and a Type I functional phi of the PRESCRIBED weight J
with ||y|| <= 500 and phi(y) >= 1/2, uniformly over any tail; it is iterated
along the binary tree of Part 7.

(d) The evaluation criterion (Proposition 2, Part 1) is the single hinge of both
halves of the paper. On the positive side (Part 2), a small (separable)
evaluation image of a separable F forces a quotient. On the negative side
(Part 8), a nonseparable evaluation image on every separable F blocks every
quotient. The two halves of the main theorem are therefore the same criterion
applied in opposite directions.

(e) The problem is not stated in Banach's 1932 book, and Rosenthal's 1969 paper
is an early written formulation (Brech 2025, p. 74). Prior positive results
cover dual spaces (Argyros, Dodos, Kanellopoulos 2008, Theorem 15) and the
Johnson-Rosenthal result that every separable infinite-dimensional Banach space
has an infinite-dimensional quotient with a Schauder basis. The present paper
places the general separable quotient problem in its proper place: independent
of ZFC for the unrestricted statement, and independent at density aleph_1
already.

This completes the proof of the main theorem.

                                                END OF THE PAPER