MATHLIBANNEX / PROJECT LFH

CH and the existence of a counterexample of norm density aleph one

This separate route has one direct Card: the CH equivalence. It reuses the two density Cards as references; they remain members of the main route and are not duplicated as new selected Cards.

The forward implication substitutes into the continuum-density existence result. The reverse applies the density obstruction to an arbitrary witness and obtains . It does not assume that this witness has a faithful separable representation. The equivalence itself assumes neither CH nor its negation and is not a forcing or independence proof.

Exact Card references

Density references reused from the main route

Boundary Inputs

The displayed edges preserve dependency paths through omitted helpers. Levels count selected predecessors within this scope. Mathematical citations remain distinct from formal dependencies.

Exact source and provider boundary · Earlier 466-declaration Project view and PDF

Dependency-first reading route

Levels belong to this reading scope. Follow prerequisites or uses to focus the route.

3 declarations

Level 0

Level 0Focus target

Exact norm density of the fixed atomic algebra

MathlibAnnex.CStarAlgebra.CAR.hasDensityCharacter_atomicCounterexampleAlgebra

Combines a cardinality bound from a faithful representation on a separable Hilbert space with a lower bound for every norm-dense subset.

Immediate prerequisites in this Project
None in this scope

Used by in this Project
A Naimark counterexample of continuum norm density

Open Declaration CardRead exact source

Level 1

Level 1Focus target

A Naimark counterexample of continuum norm density

MathlibAnnex.CStarAlgebra.CAR.existsNaimarkCounterexampleOfDensity_continuum

Gives a C*-algebra of norm density whose nonzero irreducible representations form one unitary-equivalence class, without an identification with the compact operators.

Immediate prerequisites in this Project
Exact norm density of the fixed atomic algebra

Used by in this Project
CH and a Naimark counterexample of norm density aleph one

Open Declaration CardRead exact source

Level 2

Level 2Focus target

CH and a Naimark counterexample of norm density aleph one

MathlibAnnex.CStarAlgebra.CAR.continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity

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

Immediate prerequisites in this Project
A Naimark counterexample of continuum norm density

Used by in this Project
None in this scope

Open Declaration CardRead exact source
Back to top ↑