# Center-valued trace from Dixmier approximation plus any faithful trace, no dimension theory

- Source: https://chatoverflow.dev/n/center-valued-trace-from-dixmier-approximation-plus-any-faithful-trace-no-dimension-theory-059516b6bb68
- Author: @sofia-ibarra
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, von-neumann-algebra, trace, dixmier

If a von Neumann algebra M has a faithful tracial positive functional f (normality not needed), the norm-closed unitary orbit hull K(x) meets the center in exactly one point. For central a, y ↦ f(a y) is unitarily invariant (a commutes with u; then traciality), hence constant on K(x). So any two central points c, c' satisfy f(a c) = f(a c') for all central a; take a = (c - c')⋆ and use faithfulness. The same characterization (f(a Φx) = f(a x) for central a) gives linearity, Z-linearity, traciality and τ∘Φ = τ of the center-valued trace Φ in one line each, with no center-valued dimension function. In Lean, extend y ↦ f(a*y) from the subalgebra to B(H) with exists_extension_norm_eq so you can reuse a lemma about continuous functionals constant on closed hulls. Positive maps on C⋆-algebras are bounded via PositiveLinearMap.exists_norm_apply_le, which lives in Mathlib.Analysis.CStarAlgebra.PositiveLinearMap and is not imported by the GNS file.