# Theorem B proof route

This pass targets the unchanged `TheoremBSpec` in `PL1/Statements.lean`.
Every clause concerns the same actual constant-rate interval projection and
its inherited range norm. The real and complex targets include the reviewed
absence of an equivalent lattice norm on the underlying real space.

The proof takes a direct route through the concrete construction. It does
not require a general Enflo–Starbird extraction theorem or a full measure-space
representation theorem for every complemented Banach lattice in L1.
The older conditional reductions remain valid and separately identifiable.

## The lattice alternative

The finite Rademacher moment and clipping argument proves the real matrix
Grothendieck inequality with constant 128. The finite operator deductions
give one-summing estimates from finite ell1 into finite Hilbert space and
two-summing estimates from finite supremum-norm space into finite ell1.
The actual contractive dyadic analysis and synthesis maps transfer both
estimates to interval L1 by norm convergence of its dyadic averages.

The estimates transfer through an actual complemented embedding and
retraction. Localized positive dual functionals give a lower-one estimate
for disjoint lattice vectors without assuming principal band projections.
Finite disjoint refinement in the order-complete dual and approximate
primal disjointization extend the bound to every finite positive family.
The supremum over positive decompositions then defines an equivalent AL
norm, with proved upper and lower comparisons and positive additivity.

For a complete separable AL lattice, actual atomic coordinates give an
isometric embedding into scalar ell1 and hence the Schur property in the
atomic case. In the non-atomic case, actual equal-mass fragments give a
dyadic tree; its compatible finite maps extend by dyadic density to an
isometric interval-L1 embedding. This proves the precise consequence needed:
a separable Banach lattice complemented in real interval L1 is Schur or
contains a real interval-L1 copy.

## Direct exclusion of arbitrary L1 copies

For an operator T from interval L1 to a real L1 space, define U_m(T) as the
integral of the pointwise maximum of the absolute images of the 2^m dyadic
indicator functions. Define a_m(T) as the sum of their L1 norms. Both are
nonnegative, and U_m(T) ≤ a_m(T) ≤ norm(T).

A finite Rademacher second-moment estimate and Young's inequality show that
if T has lower bound c > 0 then c² ≤ U_m(T) norm(T) at every level. Thus
decay of U_m rules out a bounded-below operator and hence every closed
isomorphic interval-L1 copy, not merely complemented copies.

For any bounded S from interval L1 to Haar L1, the functions
g_m = sum_i abs(S indicator_i) increase almost everywhere under dyadic
refinement. Their integrals are at most norm(S). Actual monotone convergence
therefore supplies one integrable nonnegative majorant g for all levels.
This step does not assume weak compactness of S.

Clip each indicator image at a fixed height M. The sum of all clipping
errors is bounded in L1 by the integral of max(g-M,0), which tends to zero
as M tends to infinity. On the bounded part, positive-time constant-rate
noise maps Lp to L2 with p = 1+exp(-2u) < 2. The squared maximum mass is
bounded by

    M^(2(1-1/p)) (norm(S) 2^(-m))^(2/p-1) norm(S).

The exponent 2/p-1 is positive. Consequently every positive-time noise
operator composed with every such S has U_m tending to zero. All norms,
representatives, integrals, truncations and limit passages are actual Lean
objects in the construction.

This decay property is closed under addition, scalar multiplication and
operator-norm limits. The previously proved estimate
norm(C_u R_t - R_t) ≤ 2u/t therefore gives decay for each resolvent composed
with S. The intrinsic weighted-defect identity makes evaluation at zero an
operator-norm limit of the corresponding resolvent compositions; its error
is bounded by the geometric weight times the original operator norm.
Every higher graph coordinate is a scaled difference of these maps and
therefore has the same decay.

To pass from individual coordinates to the entire ell1 graph, the coordinate
variations a_(n,m) increase with m, and their sum over every finite set of n
is at most the original operator norm. Their coordinatewise suprema thus
form a summable majorant. Dominated convergence applies to the sum of the
maximum masses. Actual isometric flattening into L1 on counting measure
times Haar measure identifies this sum with the maximum mass of the whole
operator, contradicting the lower-bound inequality above.

Real and imaginary part maps intertwine the actual scalar convolution and
the intrinsic coordinate equations. The scalar graph norm is bounded by
the sum of the two real graph norms. Applying the same argument to both
parts together proves the stronger absence of real L1 copies even for the
underlying real space of the complex construction. Neither part is assumed
individually bounded below.

## Final combination and verification

The actual projection already has the reviewed norm bound 4+3sqrt(2), a
closed infinite-dimensional range, a closed scalar ell2 copy, and failure
of the Schur property. The direct exclusion above supplies the missing L1
clause. If the underlying real range admitted an equivalent lattice norm,
the actual complemented ambient maps and the proved lattice alternative
would force either the Schur property or a real L1 copy, giving the two
required contradictions.

The final 222-source native rebuild passed. Its exact endpoint checks, source
hashes and 154 standard-only axiom reports are recorded in
[THIRD_CONSTRUCTION_REPORT.md](verification/THIRD_CONSTRUCTION_REPORT.md).
The original reviewed statement sources and dependency pins are preserved;
auxiliary equivalent AL norms do not change the norm of the constructed witness.