Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.CStarAlgebra.CAR.existsNaimarkCounterexampleOfDensity_continuum
MathlibAnnex/Analysis/CStarAlgebra/CAR/ContinuumHypothesis.lean · lines 18–32
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Cardinality 2 3/-! 4# CH and a Naimark counterexample of norm density aleph one 5 6The forward direction uses the same concrete algebra and faithful separable 7representation as the existing endpoint. The reverse direction is the general 8(possibly nonunital) density obstruction, without a separable-representation 9assumption. This is a mathematical biconditional, not a metatheoretic forcing 10or independence certificate. 11-/ 12set_option autoImplicit false 13open scoped Cardinal ComplexOrder 14namespace MathlibAnnex.CStarAlgebra.CAR 15universe v 16open MathlibAnnex.Analysis.CStarAlgebra MathlibAnnex.Topology 17 18/-- The fixed construction supplies an ordinary counterexample of exact 19norm density continuum. This existence assertion has no CH premise. -/ 20theorem existsNaimarkCounterexampleOfDensity_continuum : 21 ExistsNaimarkCounterexampleOfDensity (Cardinal.continuum : Cardinal.{0}) := by 22 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 · exact 29 Representation.IsSingletonIrreducibleModelAmongNonUnital.isSingletonIrreducibleModel_toNonUnitalStarAlgHom 30 (isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion.{0} 31 homogeneityShellFamily).2 32 · exact not_isCompactOperatorModel_shellFamilyTarget homogeneityShellFamily _ 33 34/-- CH is equivalent to the existence of an ordinary possibly nonunital 35Naimark counterexample of exact norm density aleph one. Carriers in this closed 36existence 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}) := by 40 constructor 41 · intro hCH 42 rw [← hCH] 43 exact existsNaimarkCounterexampleOfDensity_continuum 44 · exact continuum_eq_aleph_one_of_existsNaimarkCounterexampleOfDensity 45 46/-- 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_one 49 (hCH : (Cardinal.continuum : Cardinal.{0}) ≠ Cardinal.aleph 1) : 50 ¬ ExistsNaimarkCounterexampleOfDensity (Cardinal.aleph 1 : Cardinal.{0}) := by 51 intro h 52 exact hCH (continuum_eq_aleph_one_iff_existsNaimarkCounterexampleOfDensity.mpr h) 53 54/-- 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⟩ 62 63end MathlibAnnex.CStarAlgebra.CAR