# Independence of the separable quotient problem

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Relative independence of the separable quotient problem](../../preprints/Relative-independence-of-the-separable-quotient-problem-September-23-2026/paper.pdf)

## Scope

The separable quotient problem asks whether every infinite-dimensional Banach space has an infinite-dimensional separable quotient. The linked formalization proves the negative direction under the continuum hypothesis: over both the real and complex fields, there is an infinite-dimensional Banach space admitting no bounded linear surjection onto an infinite-dimensional separable Banach space.

This is the conditional counterexample direction. The positive consistency direction and the paper's full relative-independence conclusions are outside the selected statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Failure of the separable quotient assertion under the continuum hypothesis | [SeparableQuotientNegative.lean](../ComparatorChallenges/SeparableQuotientNegative.lean) |