The separable quotient assertion under CH

The separable quotient assertion under CH

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 323; 2026-09-23), the asserted result is that the general separable-quotient assertion is independent of ZFC relative to a measurable cardinal, with a ZFC-only relative-independence result at density $\aleph_1$.

Mathematical statement of the claimed result

Manuscript 1.

For $\mathbb F=\mathbb R$ or $\mathbb C$, write $\mathrm{SQ}_{\mathbb F}$ for the following assertion: each Banach space of infinite dimension over $\mathbb F$ admits a bounded linear quotient whose range is separable and remains infinite dimensional. In ZFC, the manuscript claims \[ \mathfrak c\text{ real-valued measurable}\Rightarrow\mathrm{SQ}_{\mathbb F}, \qquad\mathrm{CH}\Rightarrow\neg\mathrm{SQ}_{\mathbb F}. \] Here real-valued measurable means a probability measure on every subset of the cardinal $\mathfrak c=2^{\aleph_0}$, vanishing on singletons and additive on disjoint families of size less than $\mathfrak c$. If ZFC plus a measurable cardinal is consistent, the separable quotient assertion is therefore claimed independent of ZFC. Relative consistency of its failure needs only consistency of ZFC.

Outline of the argument

For manuscript 1 (family 323; 2026-09-23), a coded coordinate predual uses norming paths to prevent separable evaluation images in the counterexample model. Block restrictions and strictly singular estimates establish the obstruction, while a continuum measure hypothesis supplies the positive-model direction.

Formal verification

For manuscript 1 (family 323; 2026-09-23), the documented Lean scope is under CH, real and complex Banach counterexamples with no infinite-dimensional separable quotient; the positive-model direction and complete relative-independence assertion are outside the selected theorem.

The selected statement includes the clause used for this problem.

The linked family Comparator checks are SeparableQuotientNegative.lean.

Their named declarations include OAI.SeparableQuotient.negative_main.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

• OpenAI, Relative independence of the separable quotient problem, 2026-09-23; citation key OAI:Relative-independence-of-the-separable-quotient-problem-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: intro:main.
• Family 323: Lean scope.
• Comparator SeparableQuotientNegative.json.
• Comparator SeparableQuotientNegative.lean.
• OpenAI catalogue entry.