The normalized trace on a finite CAR stage

MathlibAnnex.CStarAlgebra.CAR.stageTrace

def

The normalized matrix trace provides a positive tracial functional compatible with the CAR inclusions.

Statement

For , let with its operator norm. The finite-stage trace is the continuous complex-linear functional whose value is . The factor makes .

Definition

Take the normalized diagonal sum as a linear map. Each diagonal entry satisfies , so the triangle inequality gives . This bound supplies continuity. Positivity follows by expanding the diagonal of into sums of squared absolute values; the trace identity follows by interchanging the two finite summations. Amplification repeats every diagonal entry twice, exactly cancelling the change in normalization.

Assumptions

The index may be zero, in which case . No representation, choice of vector, or limiting operation enters this definition.

Conclusion

The functional is bounded by , is positive on , and satisfies . Under the standard CAR inclusion , given by and coordinate reindexing, . These are the separately proved properties cited below.

Main citations

Lean source signature (exact)

noncomputable def stageTrace (n : ℕ) : Stage n →L[ℂ] ℂ :=
  (stageTraceLinear n).mkContinuous 1 fun a ↦ by
    simpa only [one_mul] using norm_stageTraceLinear_le n a

Here Stage n is , stageTraceLinear n is the normalized diagonal sum, and mkContinuous 1 equips it with the bound . The displayed right-hand side is the full definition of stageTrace. The formula for its underlying linear map and the proofs of its properties are separate exact citations.

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

Lean realization notes

The root projection has trace ; the root-coordinate functional instead takes value there. Thus the trace and the product-vector functional serve different purposes. The declaration here defines a finite-stage functional, not a new assertion about a trace on the completion.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:0047cafd9294f990a20362b56c9f7b905407ae2c02f2b9df80a3dba01bf1254b

Card revision: 1 · SHA-256: 45e6017f58cbdedcc1be3088d3b58abd517ca8d0efe97b5f8680a335352d7ccd

Exposition revision: 2 · SHA-256: 0383e61e8449db7d28fa9398e2ae0163b6b0a2d391263673f75789b3ad736e58

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 2343c37755c623f18598332050ca73a4628ed407fb235b9322a900929e20e2c1