Finite matrix stages enter the CAR completion with distinct root-state and normalized-trace roles. Pointwise root-compression estimates support later residual-space arguments, while simplicity and compact-image exclusion are separate conclusions.
12 direct Cards + 0 reused prerequisites = 12 unique Cards. This count is a selected Card closure, not a source-declaration count.
The finite matrix stages
enter their norm completion
through
.
The root state
and normalized trace
have different roles:
,
whereas
.
The root projections are
.
Here
belongs to
and
is its image in
;
that image need not have rank one in a representation of
.
The compression estimate
is pointwise in the fixed element
.
It supplies the later residual-space arguments. The simplicity proof
uses a sufficiently late fixed projection; it does not replace this norm
estimate by uniform convergence. Infinite dimension and the absence of
nonzero compact images in irreducible representations are separate
conclusions. Their proofs remain in the individual Cards.
Read selected Card prerequisites before their uses. Levels are recomputed from the selected reachability-preserving projection; omitted source helpers remain traceable in the source exploration.
No Cards match this search. Clear search to recover this reading scope.
Level 0 (2 Cards)
Level 0
The CAR
algebra as a completion of finite matrix stages
Names the completed CAR algebra in which finite matrix calculations
can be extended by norm approximation.
MathlibAnnex.CStarAlgebra.CAR.Limit
Immediate Card prerequisites: None in this selected scope