Finite-stage purification and local transport

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 .

Exact Card references

• Realizing a finite Gram matrix in a represented CAR corner — MathlibAnnex.CStarAlgebra.CAR.exists_rootCornerFamily_with_gram
• Purifying a vector state on a finite CAR stage — MathlibAnnex.CStarAlgebra.CAR.exists_unitVector_vectorFunctional_eq_on_stage
• Lifting a corner involution to an ambient CAR unitary — MathlibAnnex.CStarAlgebra.CAR.exists_liftedCornerExponential_apply_eq_involution
• Exact vector transport along an almost central unitary path — MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt
• Cross-representation state approximation with a protected finite set — MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_crossRepresentation_path_approx
• Approximating another vector state along a unitary path — MathlibAnnex.CStarAlgebra.CAR.exists_unitary_crossRepresentation_path_approx