Enflo's space without the approximation property

Enflo's Theorem 1 constructs, in the ordinary ZFC setting, a separable reflexive Banach space without the approximation property. The theorem's own quantitative conclusion is stronger: there are finite-dimensional subspaces $M_n$, with $\dim M_n\to \mathrm{\infty }$, and $C>0$ such that every finite-rank $T$ satisfies

$\mathrm{\parallel }T-I{\mathrm{\parallel }}_{(M_n)}\ge 1-\frac{C\mathrm{\parallel }T\mathrm{\parallel }}{\log \dim M_n}\mathrm{.}$

This recorded item is non-load-bearing. Under DC, the locally proved implication from a Schauder basis to BAP shows that Enflo's space has no Schauder basis. The pair supplies the Grothendieck reflexive-AP-implies-MAP theorem locally, so the AP conclusion is no longer blocked on a missing external prerequisite; the proof-bearing retirement above carries its own review record, and this historical leaf does not substitute for it.