MATHLIBANNEX / CANONICAL DECLARATION CARD

The matching GNS fiber retains exactly its cyclic line

MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_rankOne

theorem

Identifies the residual projection of a transported CAR flag in its matching pure-state representation.

Statement

For the fixed shell family and index described below, set and . The orthogonal projection onto satisfies for every . In particular, .

Assumptions

Let be the completed CAR algebra, the completion of the matrix stages under . Write for the image of the first diagonal matrix unit. These are decreasing projections with . Write for the canonical embedding of stage . The root state is determined by on every stage.

Choose one pure state from each unitary-equivalence class of pure-state Gelfand-Naimark-Segal (GNS) representations, retaining at the root index . Write for its complete complex GNS space, unital star representation and unit cyclic vector. Thus , and the vectors are dense in . Inner products are linear in the second argument.

A fixed shell family supplies unital complex star automorphisms and elements with , , and . At the root, is the identity and . Fix and put . The family is supplied; its existence is not an extra conclusion here.

Conclusion

The one-dimensional common range is a proved property of the transported flag, not a field imposed on the shell family. Since are decreasing orthogonal projections, the cited decreasing-projection theorem also gives in norm for each fixed .

Proof route

The state identity gives , so every fixes . The transported CAR compression estimate gives for each . Contractivity of and fixedness of vectors in yield . Applying this to determines on its dense cyclic orbit and hence on all of .

Proof steps

  1. For a projection , the identity implies . Therefore .

  2. On vectors fixed by every , the matrix coefficient of the represented compression error is independent of and tends to zero. This proves the displayed compressed-operator identity. The source error converges in the norm of .

  3. Consequently . Both sides are continuous linear maps of the orbit vector, and that orbit is dense. The unit norm of identifies the resulting rank-one map as an orthogonal projection.

Main citations

Lean source signature (exact)

theorem selected_commonFixedProjection_eq_rankOne
    (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :
    commonFixedProjection (fun n ↦
      MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i
        (transportedFlag family i n)) =
      InnerProductSpace.rankOne ℂ
        (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)
        (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)

Here Limit is and completedRootPureState is the root state , bundled with its purity proof. selectedRepresentation completedRootPureState i is , selectedVector completedRootPureState i is the unit vector , and transportedFlag family i n is . commonFixedProjection projects onto the vectors fixed by every ; for projections this is . The displayed rankOne sends to . The equality itself is not a filter-limit statement.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF

Lean realization notes

The exact declaration identifies the common fixed projection. The pointwise convergence just stated is a consequence using the separately cited decreasing-projection theorem. Neither statement asserts operator-norm convergence, and no strong limit is transported through a representation of a different algebra.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:d037e35eb7877cc000c8dd4c00542ec6472c63f14055ad12e94f5721e4fe6a61

Card revision: 1 · SHA-256: 749883080e4d77ab3a35f830c3d36c79dec17bf74468620f474c10df2a93b6e5

Exposition revision: 1 · SHA-256: f479404f3d58edd77d0a8d46d038cd052a401fd3bf0e1eff59721a397d3dc85b

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: ddd58c51cec1a788287284b0b83da5c462bb3ebd42750a7515442abbc749a3eb

Back to top ↑