CH and a Naimark counterexample of density ℵ₁

MathlibAnnex.CStarAlgebra.CAR.continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity

theorem

Relates CH to the general density-existence predicate, not only to separably represented examples.

Statement

The continuum hypothesis holds if and only if there exists a nontrivial, possibly nonunital complex C*-algebra of norm density ℵ₁ with one nonzero irreducible representation class and a displayed irreducible model that is not the full compact-operator algebra.

Assumptions

This is a biconditional with no extra hypothesis. CH means 𝔠 = ℵ₁, where 𝔠 = 2^ℵ₀. The existence predicate is the one described in the counterexample existence theorem, with density ℵ₁, and with carriers and comparison spaces in Type. No faithful separable representation is assumed for an arbitrary witness.

Conclusion

𝔠 = ℵ₁ ⇔ there exists a Naimark counterexample of exact norm density ℵ₁ in the stated sense.

Proof route

Under CH, use the continuum-density example. Conversely, the general representation-theoretic density obstruction applied to a density-ℵ₁ witness gives 𝔠 ≤ ℵ₁; combine this with ℵ₁ ≤ 𝔠.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.existsNaimarkCounterexampleOfDensity_continuum

  Exact source attribution.

• MathlibAnnex.Analysis.CStarAlgebra.continuum_eq_aleph_one_of_existsNaimarkCounterexampleOfDensity

  Exact source attribution.

Lean source declaration (exact)

/-- CH is equivalent to the existence of an ordinary possibly nonunital
Naimark counterexample of exact norm density aleph one. Carriers in this closed
existence statement lie in Type; the reverse obstruction is universe-polymorphic. -/
theorem continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity :
    (Cardinal.continuum : Cardinal.{0}) = Cardinal.aleph 1 ↔
      ExistsNaimarkCounterexampleOfDensity (Cardinal.aleph 1 : Cardinal.{0}) := by
  constructor
  · intro hCH
    rw [← hCH]
    exact existsNaimarkCounterexampleOfDensity_continuum
  · exact continuum_eq_aleph_one_of_existsNaimarkCounterexampleOfDensity

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Approved Card JSON

Lean realization notes

CH is a proposition in the biconditional, not an added axiom of the development. This is an object-level equivalence, not a forcing construction or a metatheoretic independence certificate. The supporting obstruction has broader universe parameters; the final biconditional here is its closed universe-zero form.