Uniqueness of the tracial state

MathlibAnnex.CStarAlgebra.CAR.existsUnique_tracial_state

theorem

Proves uniqueness among normalized positive traces on each shell-family algebra.

Statement

For every representative shell family F, the associated C*-algebra A_F has exactly one tracial state.

Assumptions

Let C be the completed CAR algebra, φ₀ its distinguished pure state, φᵢ one selected pure state in each GNS-equivalence class, and eₙ the fixed root shell projections. Fix a representative shell family F: for each i, an automorphism αᵢ and elements wᵢ,ₙ of C satisfying φᵢ ∘ αᵢ = φ₀, wᵢ,ₙ* wᵢ,ₙ = αᵢ(eₙ), and wᵢ,ₙ wᵢ,ₙ* = eₙ. At the root class, α₀ is the identity and w₀,ₙ = eₙ. Let A_F ⊆ B(Hₐₜ) be the norm-closed unital *-algebra generated by the atomic image of C and the shell-link unitaries constructed from F; write j_F: C → A_F for the source map. States are continuous positive complex-linear functionals normalized by φ(1) = 1.

Conclusion

There exists exactly one state φ: A_F → ℂ satisfying φ(ab) = φ(ba) for all a, b ∈ A_F. It is the constructed extension of the normalized CAR trace.

Proof route

The constructed extension is tracial. Any tracial state on A_F restricts to the unique normalized CAR trace, so uniqueness of the state extension identifies it with the constructed extension.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.eq_traceExtension_of_mem_stateSpace_of_mul_comm

  Exact source attribution.

Lean source declaration (exact)

/-- The existing target has exactly one tracial state. Faithfulness is proved
separately above; uniqueness ranges over all states, not just selected extensions. -/
theorem existsUnique_tracial_state (family : RepresentativeShellFamily) :
    ∃! φ : ShellFamilyTarget family →L[ℂ] ℂ,
      φ ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace (ShellFamilyTarget family) ∧
        ∀ a b, φ (a * b) = φ (b * a) := by
  refine ⟨traceExtension family,
    ⟨traceExtension_mem_stateSpace family, traceExtension_mul_comm family⟩, ?_⟩
  intro φ hφ
  exact eq_traceExtension_of_mem_stateSpace_of_mul_comm family φ hφ.1 hφ.2

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

Lean realization notes

The theorem states unique existence of a state satisfying the trace identity, not uniqueness of all states. Its displayed conclusion does not itself assert faithfulness. The latter is proved separately and included for the fixed A in the counterexample theorem with its faithful separable tracial model.