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.

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

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

Supporting route explanation

Lean source signature (exact)

theorem continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity :
    (Cardinal.continuum : Cardinal.{0}) = Cardinal.aleph 1 ↔
      ExistsNaimarkCounterexampleOfDensity (Cardinal.aleph 1 : Cardinal.{0})
In the source Mathematical meaning
(Cardinal.continuum : Cardinal.{0}) = Cardinal.aleph 1 The left proposition is CH: , with both cardinals at universe level zero. The annotation is not a cardinal-zero condition.
↔︎ The conclusion asserts both implications. CH gives the stated existence, and any witness to the stated existence gives CH. CH is not an input hypothesis of the equivalence theorem.
ExistsNaimarkCounterexampleOfDensity The linked exact existential predicate chooses one nonzero possibly nonunital complex C*-algebra , its spectral order, one complete complex Hilbert space , and one star representation in the indicated universe. Source letters A, H, pi in that definition denote here.
NonUnitalCStarRepresentation.IsSingletonIrreducibleModel pi That same is nonzero irreducible, and every nonzero irreducible possibly nonunital on any complete complex Hilbert space in the comparison universe is unitarily equivalent to . This means a surjective complex-linear isometry satisfies for every .
¬ IsCompactOperatorModel pi The same does not simultaneously have all three properties: injectivity, compactness of every , and coverage of every compact operator on . It is the full compact-operator model that is excluded, not a single compact image.
HasDensityCharacter A κ The same has a norm-dense subset of cardinality , and every norm-dense subset has cardinality at least . This is exact norm density of the existential algebra; no faithful separable model is imposed.

Further source notes: (Cardinal.continuum : Cardinal.{0}) is the continuum in the universe of cardinalities of Type 0 types; .{0} specifies the universe, not the value zero. 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.

Separate complete definition of the existential result predicate, from the fixed source, lines 56–72. Its letters A, H, pi denote the same explained in the table; this is not a continuation of the theorem signature.

def ExistsNaimarkCounterexampleOfDensity (κ : Cardinal.{u}) : Prop :=
  ∃ (A : Type u) (iA : NonUnitalCStarAlgebra A),
    letI := iA
    ∃ (oA : PartialOrder A),
      letI := oA
      ∃ (sA : StarOrderedRing A) (nA : Nontrivial A),
        letI := sA
        letI := nA
        ∃ (H : Type u) (nH : NormedAddCommGroup H),
          letI := nH
          ∃ (iH : InnerProductSpace ℂ H),
            letI := iH
            ∃ (cH : CompleteSpace H),
              letI := cH
              ∃ pi : NonUnitalCStarRepresentation A H,
                NonUnitalCStarRepresentation.IsSingletonIrreducibleModel.{u, u, u} pi ∧
                (¬ IsCompactOperatorModel pi) ∧ HasDensityCharacter A κ

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

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity

Accepted content SHA-256: af847aaea6b518301f9dbc23d58f0245b983e48e72b4792c81df03c74440fb6c

Accepted source guide SHA-256: f5b32ca0f64d6b413a8d4d2f0768556c291ca130ae7cdc4e065b1c6155bc1cd5

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑