The atomic Hilbert space has norm density continuum

MathlibAnnex.CStarAlgebra.CAR.hasDensityCharacter_atomicCounterexampleHilbert

theorem

Determines the size of a smallest norm-dense set in the irreducible Hilbert model.

Statement

The Hilbert space Hₐₜ of the atomic inclusion of the fixed CAR-based algebra A has norm density character exactly 𝔠 = 2^ℵ₀.

Assumptions

Let A ⊆ B(Hₐₜ) be the fixed unital C*-algebra obtained by adjoining the chosen shell-link unitaries to the atomic representation of the CAR algebra C, and then taking the norm-closed unital *-algebra they generate. Let πₐₜ be its distinguished atomic inclusion on Hₐₜ. This theorem concerns Hₐₜ, not the separable trace-GNS space Hτ.

Conclusion

There is a norm-dense subset D ⊆ Hₐₜ of cardinality 𝔠, and every norm-dense E ⊆ Hₐₜ satisfies 𝔠 ≤ |E|. Thus dens(Hₐₜ) = 𝔠.

Proof route

The representation-space density obstruction supplies the lower bound. For the upper bound, take the cyclic orbit of a nonzero vector under A and use |A| = 𝔠.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.continuum_le_cardinalMk_dense_atomicCounterexampleHilbert

  Exact source attribution.

• MathlibAnnex.Analysis.CStarAlgebra.Representation.denseRange_orbitMap_of_isIrreducible

  Exact source attribution.

Lean source declaration (exact)

theorem hasDensityCharacter_atomicCounterexampleHilbert :
    HasDensityCharacter
      (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)
      Cardinal.continuum := by
  let H := MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState
  let pi : Representation AtomicCounterexampleAlgebra H :=
    shellFamilyInclusion homogeneityShellFamily
  have hirr : Representation.IsIrreducible pi :=
    isIrreducible_shellFamilyInclusion homogeneityShellFamily
  letI : Nontrivial H := Representation.nontrivial_of_isNonzero pi hirr.1
  obtain ⟨x, hx⟩ : ∃ x : H, x ≠ 0 := exists_ne 0
  let s : Set H := Set.range (fun a : AtomicCounterexampleAlgebra => pi a x)
  have hs : Dense s := Representation.denseRange_orbitMap_of_isIrreducible pi hirr hx
  have hupper' : Cardinal.lift.{0} (#s) ≤
      Cardinal.lift.{0} (#AtomicCounterexampleAlgebra) := Cardinal.mk_range_le_lift
  have hupper : #s ≤ Cardinal.continuum := by
    simpa [cardinalMk_atomicCounterexampleAlgebra] using hupper'
  refine ⟨⟨s, hs, le_antisymm hupper
    (continuum_le_cardinalMk_dense_atomicCounterexampleHilbert s hs)⟩,
    continuum_le_cardinalMk_dense_atomicCounterexampleHilbert⟩

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

Lean realization notes

This is a norm-density statement, not a carrier-cardinality or Hamel-rank computation. The usual infinite-dimensional Hilbert-space theorem then identifies the cardinality of an orthonormal basis with 𝔠; that consequence is not a dedicated Lean endpoint of this declaration. No Project level is fabricated for this scope-external declaration.