MATHLIBANNEX / CANONICAL DECLARATION CARD

CH and a Naimark counterexample of norm density aleph one

MathlibAnnex.CStarAlgebra.CAR.continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity

theorem

Characterizes the continuum hypothesis by the existence of a Naimark counterexample of exact norm density .

Statement

Write . Then The right-hand side has the following precise meaning. There are a nonzero, possibly nonunital complex C*-algebra , a complex Hilbert space , and a nonzero irreducible -representation such that every nonzero irreducible -representation of is unitarily equivalent to , the map is not both injective and surjective onto , and . Preservation of an identity is not required of these representations.

Assumptions

The equivalence itself assumes neither CH nor its negation. In the reverse implication, and are arbitrary objects satisfying the displayed existence statement; a faithful representation of on a separable Hilbert space is not an additional hypothesis.

Conclusion

CH implies the stated existence, and any witness of that existence implies CH. The equivalence is a mathematical theorem about exact norm density; it neither proves CH nor supplies a forcing or metatheoretic independence proof.

Proof route

For the forward implication, substitute in the continuum-density existence theorem. For the reverse implication, the general density obstruction for a C*-algebra with a single irreducible representation class gives ; combine it with .

Proof steps

  1. Assume . The continuum-density existence theorem gives a nonzero C*-algebra with the stated representation properties and norm density . Substitution yields density .

  2. Conversely, let satisfy the right-hand side. Exact density provides a norm-dense with . Apply the cited density obstruction to , the unitary equivalence of all nonzero irreducible representations to it, its failure to be an injective representation onto , and the density of . This theorem allows a nonunital algebra and gives . No separable representation is required.

  3. Therefore Antisymmetry gives , as required.

Main citations

Lean source signature (exact)

theorem continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity :
    (Cardinal.continuum : Cardinal.{0}) = Cardinal.aleph 1 ↔
      ExistsNaimarkCounterexampleOfDensity (Cardinal.aleph 1 : Cardinal.{0})

(Cardinal.continuum : Cardinal.{0}) is the continuum in the universe of cardinalities of Type 0 types; .{0} specifies the universe, not the value zero. Cardinal.aleph 1 is . The separately linked definition of ExistsNaimarkCounterexampleOfDensity supplies the exact existential quantifiers and the condition excluding an injective representation onto all compact operators. The proof first substitutes the CH equality in the continuum-density theorem, then invokes continuum_eq_aleph_one_of_existsNaimarkCounterexampleOfDensity. The general reverse theorem allows independent algebra and Hilbert-space universes; this statement uses its level-zero instance.

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

Lean realization notes

The forward implication uses the concrete algebra built from CAR. The reverse implication is not restricted to that construction.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:49b78f91c5e53fc7fff64fc366388f4d162fb65ecd6cb16fafe5785a8f2a236c

Card revision: 2 · SHA-256: e9e119b142df5c73ca63aebd69db0c6601d2eba833dd69fa691bd0485a511bac

Exposition revision: 3 · SHA-256: 9b817fdfc02db29eae7b52ffa9979f807d083de108cc9c93e524989334a1917c

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 301eb3aee7083bfdb17a802c4306f827c261d357982956eef0158565eedc85f4

Back to top ↑