OAI.SeparableQuotient.negative_main

Open

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that, under the continuum hypothesis CH (the defined proposition that the cardinality of ℝ equals ℵ₁), the separable quotient assertion fails over both the real and the complex numbers, at any universe level u. Here SQ over a scalar field 𝕜 (ℝ or ℂ) asserts that every complete normed space X over 𝕜 in Type u that is not finite-dimensional has a separable quotient in the following sense: there exist a complete, separable, infinite-dimensional normed space Y over 𝕜, also in Type u, and a bounded 𝕜-linear map T from X to Y that is surjective. The conclusion is the conjunction of ¬SQ(ℝ) and ¬SQ(ℂ), so for each field there is an infinite-dimensional Banach space with no such bounded surjection onto an infinite-dimensional separable Banach space. The statement is admitted without proof in the source.

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/SeparableQuotientNegative.lean; bytes 888..968
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_SeparableQuotientNegative

namespace OAI

namespace SeparableQuotient

open MeasureTheory Cardinal

universe u

Formal statement

theorem negative_main (hCH : CH) : ¬ SQ.{u} ℝ ∧ ¬ SQ.{u} ℂ := by
  sorry

end SeparableQuotient
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/SeparableQuotientNegative.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by marwahaha · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph