MATHLIBANNEX / CANONICAL DECLARATION CARD

Purity of the completed root state

MathlibAnnex.CStarAlgebra.CAR.isPureState_rootState

theorem

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

Statement

Let be the completed CAR algebra with stage embeddings . Let be the continuous linear functional characterized by for every stage matrix . Then is a pure state: it is an extreme point of the convex set of continuous positive unital complex-linear functionals on .

Assumptions

The embeddings come from . The index is the distinguished first coordinate in each stage. The coordinate functionals are compatible and bounded by the matrix norm, so they extend to the specified functional on the completion. Positivity and are established before the purity argument. Convex combinations use real coefficients.

Conclusion

If and are states on , , and , then . Thus completion has not introduced a nontrivial convex decomposition of this state.

Proof route

Restrict a proposed convex decomposition of to each finite matrix stage. The restriction of a state is again a state, because is unital and preserves positivity. The root coordinate state is pure on each matrix algebra, so both restricted states equal it. The two continuous functionals therefore agree with on the dense union of stages, and hence on all of .

Proof steps

  1. Write with states and .

  2. For each , compose with to obtain a convex decomposition of into states on .

  3. Finite-stage purity forces .

  4. Continuity and density imply . The source uses the equivalent one-sided extreme-point criterion, establishing the first equality, which suffices.

Main citations

Lean source signature (exact)

theorem isPureState_rootState : MathlibAnnex.CStarAlgebra.IsPureState Limit rootState

Here Limit denotes the completed CAR algebra , rootState denotes , and IsPureState expresses the extreme-point property stated above.

Lean realization notes

The purity asserted here is extremality in the state space. The proof uses the pure finite-stage restrictions and density; it makes no assertion that all states on are pure.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:8912c6847bfbf0613b2e5a5cbc237cd963d23dfa67344c472ffe179105411424

Card revision: 1 · SHA-256: 1073c8bcb6fc6b854ea9e7724a24c5bf7b47a5f19c3e725042cd2645f38e7f5d

Exposition revision: 1 · SHA-256: 319bda4c63b7243662b17ac9d3a5ed6aafef8164b2cc0ff568cdb559b3d3ba86

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: fd3476399b91ec3d1ad2a65b7dbcb19919223d9642e130dbb2d8cb71ef485ae6

Back to top ↑