Relative independence of the separable quotient problem

Follow-up works

• Tomasz Kania and Jerzy Kąkol, Separable quotients of pointwise function spaces and relative consistency (arXiv:2609.19351, v1 16 Sep 2026, v2 17 Oct 2026). The v2 cites this preprint as [28] and compares its methods with it in Section 11, saying that [28, Lemma 3.2]'s small-density sampling idea carries over to $C_p(K)$ but that the Borel-coding/Fubini step [28, Lemma 3.4] and the final contradiction [28, Section 3] do not. The authors state that they did not verify the preprint's construction and use none of its theorems.

Formalization

• OpenAI math release, Lean scope notes for family 323 (lean/docs/323.md, 6 Oct 2026). The release's Lean development covers only the negative direction: under CH, over $\mathbb R$ and $\mathbb C$, an infinite-dimensional Banach space with no bounded linear surjection onto an infinite-dimensional separable Banach space (comparator file SeparableQuotientNegative.lean). The positive direction from a real-valued measurable continuum and the relative-consistency conclusions are out of scope. [family-level]
• anxkhn, Add the separable quotient counterexample under CH (google-deepmind/formal-conjectures issue #6996, opened 8 Oct 2026). Proposes adding the statement of Theorem 1.1(ii), over the reals with CH as an explicit hypothesis, to formal-conjectures. The positive direction and relative-consistency claims are excluded.
• anxkhn, feat(Paper): add the separable quotient counterexample under CH (google-deepmind/formal-conjectures PR #7001, opened 8 Oct 2026, open at time of collection). Adds a statement-only Lean formulation of Theorem 1.1(ii) over $\mathbb R$, without a formal_proof attribute. A reviewer approved it on 10 Oct 2026, noting that it matches the paper's real universe-zero instance.

Possibly relevant literature (found by the agent, not checked)

• Stevo Todorčević, Biorthogonal systems and quotient spaces via Baire category methods (Math. Ann. 335 (2006), 687–715, doi:10.1007/s00208-006-0762-7). Shows that nonseparable Banach spaces of density below the Baire category number have quotients with a long Schauder basis of length $\omega_1$. This is another forcing-axiom route to the positive side at density $\aleph_1$ in Corollary 1.2, where the paper uses Saxon–Sánchez Ruiz and Martin's axiom instead.
• Gustavo Araújo, Anderson Barbosa and Juan B. Seoane-Sepúlveda, The Separable Quotient Problem and the Lotz Property in Banach Spaces (arXiv:2610.00584, 30 Sep 2026). Theorem 3.4 gives a positive separable-quotient criterion for infinite-dimensional Banach spaces lacking the Lotz property, which bears on the class of spaces the CH counterexamples must belong to; it does not mention this preprint.

Digests and expositions

• Gradient Damage, Tingley's Problem, Separable Quotient Problem and 8 More in Functional Analysis (video and accompanying description, 16 Oct 2026). The chapter beginning at 0:20 illustrates the separable quotient problem and presents the release's independence claim, with the source explicitly distinguishing its animations from proofs. [family-level]