Fixed subspaces and reconstruction of the generators

For the supplied family, write . On the matching fiber its common fixed projection is the projection onto ; on an inequivalent fiber it is zero. Coordinatewise reasoning therefore identifies the common range in with . These are strong, vectorwise consequences of decreasing projections, not operator-norm limits.

In an arbitrary representation of the generated algebra, shell sums and their adjoints are reconstructed on that representation's own Hilbert space. The generator splits into a strong shell sum and its residual corner. Nonzero irreducibility prevents every transported fixed space from vanishing. A surviving index may be different from the root class ; its vector is transported to a common root vector , then pulled back to the compatible vectors . No equality is imposed until the additional root-generator normalization is available.

Exact Card references

• Shell matching fixes the trace of transported flags — MathlibAnnex.CStarAlgebra.CAR.trace_transportedFlag
• Transported flags vanish on vectors generated by a trace vector — MathlibAnnex.CStarAlgebra.CAR.tendsto_transportedFlag_orbit_zero
• The matching GNS fiber retains exactly its cyclic line — MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_rankOne
• An inequivalent GNS fiber has no residual common range — MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_zero
• The atomic common range is one embedded GNS line — MathlibAnnex.CStarAlgebra.CAR.iInf_range_atomic_transportedFlag_eq_span
• Reconstructing a represented unitary from its shells and residual corner — MathlibAnnex.CStarAlgebra.CAR.exists_targetShellReconstruction
• An irreducible target representation has a surviving fixed space — MathlibAnnex.CStarAlgebra.CAR.exists_nonzero_targetFixedSpace
• A common root vector realizes every selected state through the generators — MathlibAnnex.CStarAlgebra.CAR.exists_targetDefectVectorFamily