Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/ContinuumHypothesis.lean
Pinned GitHub source · Raw UTF-8 source
Back to CH and a Naimark counterexample of norm density aleph one
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Cardinality23/-!4# CH and a Naimark counterexample of norm density aleph one56The forward direction uses the same concrete algebra and faithful separable7representation as the existing endpoint. The reverse direction is the general8(possibly nonunital) density obstruction, without a separable-representation9assumption. This is a mathematical biconditional, not a metatheoretic forcing10or independence certificate.11-/12set_option autoImplicit false13open scoped Cardinal ComplexOrder14namespace MathlibAnnex.CStarAlgebra.CAR15universe v16open MathlibAnnex.Analysis.CStarAlgebra MathlibAnnex.Topology1718/-- The fixed construction supplies an ordinary counterexample of exact19norm density continuum. This existence assertion has no CH premise. -/20theorem existsNaimarkCounterexampleOfDensity_continuum :21 ExistsNaimarkCounterexampleOfDensity (Cardinal.continuum : Cardinal.{0}) := by22 refine ⟨AtomicCounterexampleAlgebra, inferInstance, inferInstance, inferInstance,23 inferInstance,24 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState,25 inferInstance, inferInstance, inferInstance,26 (shellFamilyInclusion homogeneityShellFamily).toNonUnitalStarAlgHom, ?_, ?_,27 hasDensityCharacter_atomicCounterexampleAlgebra⟩28 · exact29 Representation.IsSingletonIrreducibleModelAmongNonUnital.isSingletonIrreducibleModel_toNonUnitalStarAlgHom30 (isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion.{0}31 homogeneityShellFamily).232 · exact not_isCompactOperatorModel_shellFamilyTarget homogeneityShellFamily _3334/-- CH is equivalent to the existence of an ordinary possibly nonunital35Naimark counterexample of exact norm density aleph one. Carriers in this closed36existence statement lie in Type; the reverse obstruction is universe-polymorphic. -/37theorem continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity :38 (Cardinal.continuum : Cardinal.{0}) = Cardinal.aleph 1 ↔39 ExistsNaimarkCounterexampleOfDensity (Cardinal.aleph 1 : Cardinal.{0}) := by40 constructor41 · intro hCH42 rw [← hCH]43 exact existsNaimarkCounterexampleOfDensity_continuum44 · exact continuum_eq_aleph_one_of_existsNaimarkCounterexampleOfDensity4546/-- Under not-CH no such aleph-one-density counterexample exists.47This is the contrapositive, not an independence claim. -/48theorem not_existsNaimarkCounterexampleOfDensity_aleph_one_of_continuum_ne_aleph_one49 (hCH : (Cardinal.continuum : Cardinal.{0}) ≠ Cardinal.aleph 1) :50 ¬ ExistsNaimarkCounterexampleOfDensity (Cardinal.aleph 1 : Cardinal.{0}) := by51 intro h52 exact hCH (continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity.mpr h)5354/-- Cardinality and exact density augment the unchanged ordinary endpoint,55which still ranges over an arbitrary comparison universe. -/56theorem atomicCounterexampleEndpoint_and_cardinality_and_density :57 AtomicCounterexampleEndpoint.{v} ∧58 #AtomicCounterexampleAlgebra = Cardinal.continuum ∧59 HasDensityCharacter AtomicCounterexampleAlgebra Cardinal.continuum :=60 ⟨atomicCounterexampleEndpoint, cardinalMk_atomicCounterexampleAlgebra,61 hasDensityCharacter_atomicCounterexampleAlgebra⟩6263end MathlibAnnex.CStarAlgebra.CAR