Back to Project mathematical routes
Finite Gram matrices and matrix units purify vector states on a chosen finite stage. Corner amplification turns this transport into almost-central unitary paths, with different stage choices for protected-set and unrestricted approximation.
6 direct Cards + 8 reused prerequisites = 14 unique Cards. This count is a selected Card closure, not a source-declaration count.
Route reading PDF · Preserved source exploration
Read this route with prerequisites
Direct references: 13 — Realizing a finite Gram matrix in a represented CAR corner · 15 — Lifting a corner involution to an ambient CAR unitary · 14 — Purifying a vector state on a finite CAR stage · 16 — Exact vector transport along an almost central unitary path · 17 — Cross-representation state approximation with a protected finite set · 18 — Approximating another vector state along a unitary path
Reused prerequisites: 3 — The product-vector state on the completed CAR algebra · 10 — Root compression becomes scalar in norm · 6 — A finite-row average centralizes its matrix stage · 9 — The decreasing root projections in the CAR completion · 2 — The CAR algebra as a completion of finite matrix stages · 12 — An irreducible CAR representation has no nonzero compact image · 11 — Simplicity of the completed CAR algebra · 5 — The completed CAR algebra is infinite-dimensional
A represented root corner has enough Hilbert-space dimension to realize any finite Gram matrix. Matrix-unit reconstruction then purifies a vector state on a selected finite stage. Supported self-adjoint interpolation and corner amplification turn finite vector transport into unitary paths; the approximate state tests concern every matrix entry, not only diagonal entries.
The protected-set theorem chooses its stage and tolerance before the later state-approximation request. The unrestricted theorem instead purifies on a large stage and transports at stage zero, where the sole unit-vector test is automatic. These are different stages. The fixed-stage abbreviation , the finite-dimensional interpolation space , and the amplification are local objects, not the later shell links or trace-GNS unitary .
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.
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
Used by in this scope: 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 · The completed CAR algebra is infinite-dimensional
Compatible evaluation at the distinguished matrix coordinate extends continuously to the CAR completion.
MathlibAnnex.CStarAlgebra.CAR.rootState
Immediate Card prerequisites: The CAR algebra as a completion of finite matrix stages
Used by in this scope: Root compression becomes scalar in norm
Rules out finite dimension by retaining matrix subalgebras of unbounded dimension.
MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional
Immediate Card prerequisites: The CAR algebra as a completion of finite matrix stages
Used by in this scope: An irreducible CAR representation has no nonzero compact image
The distinguished stage corners give a nested sequence of projections supporting the root state.
MathlibAnnex.CStarAlgebra.CAR.rootFlag
Immediate Card prerequisites: The CAR algebra as a completion of finite matrix stages
Used by in this scope: Root compression becomes scalar in norm
Turns an arbitrary element of the completed CAR algebra into one commuting with a prescribed finite matrix stage.
MathlibAnnex.CStarAlgebra.CAR.ofStage_commute_rowAverage
Immediate Card prerequisites: The CAR algebra as a completion of finite matrix stages
Used by in this scope: Exact vector transport along an almost central unitary path · Approximating another vector state along a unitary path
Extends an exact rank-one compression identity on finite stages to a pointwise norm limit on the completed algebra.
MathlibAnnex.CStarAlgebra.CAR.tendsto_norm_compressionError
Immediate Card prerequisites: The product-vector state on the completed CAR algebra · The decreasing root projections in the CAR completion
Used by in this scope: Simplicity of the completed CAR algebra
Every nonzero closed two-sided ideal of the CAR algebra contains the identity.
MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_limit
Immediate Card prerequisites: Root compression becomes scalar in norm
Used by in this scope: An irreducible CAR representation has no nonzero compact image
Simplicity and infinite dimensionality rule out compact operators coming from nonzero CAR elements.
MathlibAnnex.CStarAlgebra.CAR.eq_zero_of_isCompactOperator_image
Immediate Card prerequisites: Simplicity of the completed CAR algebra · The completed CAR algebra is infinite-dimensional
Used by in this scope: Lifting a corner involution to an ambient CAR unitary · Realizing a finite Gram matrix in a represented CAR corner
A prescribed unitary involution on a represented root corner can be realized on finitely many vectors by one lifted corner exponential.
MathlibAnnex.CStarAlgebra.CAR.exists_liftedCornerExponential_apply_eq_involution
Immediate Card prerequisites: An irreducible CAR representation has no nonzero compact image
Used by in this scope: Exact vector transport along an almost central unitary path · Approximating another vector state along a unitary path
The infinite-dimensional root corner contains an isometric copy of any finite family of vectors.
MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerFamily_with_gram
Immediate Card prerequisites: An irreducible CAR representation has no nonzero compact image
Used by in this scope: Purifying a vector state on a finite CAR stage
Every finite-stage restriction of a unit vector state can be realized by a unit vector in any irreducible CAR representation.
MathlibAnnex.CStarAlgebra.CAR.exists_unitVector_vectorFunctional_eq_on_stage
Immediate Card prerequisites: Realizing a finite Gram matrix in a represented CAR corner
Used by in this scope: Approximating another vector state along a unitary path · Cross-representation state approximation with a protected finite set
Finite matrix-state tests ensure exact transport while protecting a prescribed finite set throughout the path.
MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt
Immediate Card prerequisites: Lifting a corner involution to an ambient CAR unitary · A finite-row average centralizes its matrix stage
Used by in this scope: Cross-representation state approximation with a protected finite set
A fixed irreducible CAR representation can approximate any vector state on finitely many elements by moving a given unit vector.
MathlibAnnex.CStarAlgebra.CAR.exists_unitary_crossRepresentation_path_approx
Immediate Card prerequisites: Purifying a vector state on a finite CAR stage · Lifting a corner involution to an ambient CAR unitary · A finite-row average centralizes its matrix stage
Used by in this scope: None in this selected scope
Finite entrywise tests allow new state approximation while an entire unitary path nearly fixes earlier data.
MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_crossRepresentation_path_approx
Immediate Card prerequisites: Purifying a vector state on a finite CAR stage · Exact vector transport along an almost central unitary path
Used by in this scope: None in this selected scope