MATHLIBANNEX / CANONICAL DECLARATION CARD

Choosing the CAR shell family from proved homogeneity

MathlibAnnex.CStarAlgebra.CAR.homogeneityShellFamily

def

CAR homogeneity and exact shell matching supply one family whose distinguished component is fixed by an explicit identity choice.

Statement

Let be the completed CAR algebra, the norm completion of the matrix stages under , with the fixed coordinate reindexing. Write for the canonical inclusion, for the root state, for its decreasing root projections, and for the difference shells. Each is a self-adjoint projection. Let be the set of unitary-equivalence classes of pure-state Gelfand–Naimark–Segal (GNS) representations of . Choose a representative pure state for each , with the distinguished class represented by . Fix the following representative shell family. At , choose and . At every other , choose an automorphism from CAR homogeneity for the pair , and then choose shell links for that same automorphism. Thus , , and . This fixed choice is the homogeneity shell family.

Definition

The component supplier branches on . On the root branch, the root-state representative is exactly and , so identity and the shells themselves satisfy all component equations. On a non-root branch, homogeneity gives one with and approximate innerness. Apply the arbitrary-family shell-matching theorem to this and , and choose its link sequence. The two root lemmas certify the explicit branch, and the displayed definition assembles these data into one family.

Assumptions

The selected states are pure, including the root state. CAR homogeneity is a proved result, and the difference shells are projections. No external KOS proposition or pre-existing shell family is an input to this definition.

Conclusion

The definition supplies a value of the representative-family structure, including both root equations. The same selected value can be carried into later constructions without making a fresh choice at each use.

Main citations

Lean source signature (exact)

noncomputable def homogeneityShellFamily : RepresentativeShellFamily where
  data := representativeShellDataOfHomogeneity
  root_alpha := representativeShellDataOfHomogeneity_root_alpha
  root_link := representativeShellDataOfHomogeneity_root_link

Here data := representativeShellDataOfHomogeneity is the component choice just described. The two named root lemmas provide the root_alpha and root_link fields. homogeneityShellFamily is a fixed value, not a new existentially chosen family each time it is referenced. The component supplier is linked separately and is not concatenated into this definition’s signature.

Lean realization notes

This is a fixed choice, not a uniqueness theorem for all possible families. In particular, the non-root links need not be unique. The subsequent structural theorem uses this very family. The present definition does not itself prove uniqueness of the irreducible representation class, the rank-one identities, simplicity, or the exclusion of compact-operator algebras.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 1 · SHA-256: 0c6be805b079b4f1f3684090433f578eb030424b9ee394db71a7878007910ea2

Exposition revision: 1 · SHA-256: 9492e07b809016d2fd2c22d67477e86af56995dfdd6ff012451b4c4e428ac1ac

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: a56097c4380f01acd0958eca116ae10b0bd4b28d6bc5ed4e225f768a53748020

Back to top ↑