MATHLIBANNEX / PROJECT LFH

CAR foundations and canonical states

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.

Exact Card references

Boundary Inputs

The displayed edges preserve dependency paths through omitted helpers. Levels count selected predecessors within this scope. Mathematical citations remain distinct from formal dependencies.

Exact source and provider boundary · Earlier 466-declaration Project view and PDF

Dependency-first reading route

Levels belong to this reading scope. Follow prerequisites or uses to focus the route.

12 declarations

Level 0

Level 0Focus target

The normalized trace on a finite CAR stage

MathlibAnnex.CStarAlgebra.CAR.stageTrace

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

Immediate prerequisites in this Project
None in this scope

Used by in this Project
Constructing the normalized trace on the completed CAR algebra

Open Declaration CardRead exact source
Level 0Focus target

The CAR algebra as a completion of finite matrix stages

MathlibAnnex.CStarAlgebra.CAR.Limit

Names the completed CAR algebra in which finite matrix calculations can be extended by norm approximation.

Immediate prerequisites in this Project
None in this scope

Used by in this Project
The product-vector state on the completed CAR algebra, A finite-row average centralizes its matrix stage, The decreasing root projections in the CAR completion, Constructing the normalized trace on the completed CAR algebra, The completed CAR algebra is infinite-dimensional

Open Declaration CardRead exact source

Level 1

Level 1Focus target

The product-vector state on the completed CAR algebra

MathlibAnnex.CStarAlgebra.CAR.rootState

Compatible evaluation at the distinguished matrix coordinate extends continuously to the CAR completion.

Immediate prerequisites in this Project
The CAR algebra as a completion of finite matrix stages

Used by in this Project
Root compression becomes scalar in norm, Purity of the completed root state

Open Declaration CardRead exact source
Level 1Focus target

The completed CAR algebra is infinite-dimensional

MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional

Rules out finite dimension by retaining matrix subalgebras of unbounded dimension.

Immediate prerequisites in this Project
The CAR algebra as a completion of finite matrix stages

Used by in this Project
An irreducible CAR representation has no nonzero compact image

Open Declaration CardRead exact source
Level 1Focus target

A finite-row average centralizes its matrix stage

MathlibAnnex.CStarAlgebra.CAR.ofStage_commute_rowAverage

Turns an arbitrary element of the completed CAR algebra into one commuting with a prescribed finite matrix stage.

Immediate prerequisites in this Project
The CAR algebra as a completion of finite matrix stages

Used by in this Project
None in this scope

Open Declaration CardRead exact source
Level 1Focus target

Constructing the normalized trace on the completed CAR algebra

MathlibAnnex.CStarAlgebra.CAR.trace

Carries compatible bounded matrix traces through the algebraic limit, normed union and completion.

Immediate prerequisites in this Project
The normalized trace on a finite CAR stage, The CAR algebra as a completion of finite matrix stages

Used by in this Project
Normalization and the trace identity determine the CAR trace

Open Declaration CardRead exact source
Level 1Focus target

The decreasing root projections in the CAR completion

MathlibAnnex.CStarAlgebra.CAR.rootFlag

The distinguished stage corners give a nested sequence of projections supporting the root state.

Immediate prerequisites in this Project
The CAR algebra as a completion of finite matrix stages

Used by in this Project
Root compression becomes scalar in norm

Open Declaration CardRead exact source

Level 2

Level 2Focus target

Purity of the completed root state

MathlibAnnex.CStarAlgebra.CAR.isPureState_rootState

Passes extremality of the root vector states from every finite matrix stage to the completed CAR algebra.

Immediate prerequisites in this Project
The product-vector state on the completed CAR algebra

Used by in this Project
None in this scope

Open Declaration CardRead exact source
Level 2Focus target

Normalization and the trace identity determine the CAR trace

MathlibAnnex.CStarAlgebra.CAR.eq_trace_of_apply_one_of_mul_comm

Proves uniqueness without assuming positivity of the competing continuous functional.

Immediate prerequisites in this Project
Constructing the normalized trace on the completed CAR algebra

Used by in this Project
None in this scope

Open Declaration CardRead exact source
Level 2Focus target

Root compression becomes scalar in norm

MathlibAnnex.CStarAlgebra.CAR.tendsto_norm_compressionError

Extends an exact rank-one compression identity on finite stages to a pointwise norm limit on the completed algebra.

Immediate prerequisites in this Project
The product-vector state on the completed CAR algebra, The decreasing root projections in the CAR completion

Used by in this Project
Simplicity of the completed CAR algebra

Open Declaration CardRead exact source

Level 3

Level 3Focus target

Simplicity of the completed CAR algebra

MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_limit

Every nonzero closed two-sided ideal of the CAR algebra contains the identity.

Immediate prerequisites in this Project
Root compression becomes scalar in norm

Used by in this Project
An irreducible CAR representation has no nonzero compact image

Open Declaration CardRead exact source

Level 4

Level 4Focus target

An irreducible CAR representation has no nonzero compact image

MathlibAnnex.CStarAlgebra.CAR.eq_zero_of_isCompactOperator_image

Simplicity and infinite dimensionality rule out compact operators coming from nonzero CAR elements.

Immediate prerequisites in this Project
Simplicity of the completed CAR algebra, The completed CAR algebra is infinite-dimensional

Used by in this Project
None in this scope

Open Declaration CardRead exact source
Back to top ↑