MATHLIBANNEX / PROJECT LFH

Pure-state homogeneity and shell matching

For pure states on CAR, the sequence construction controls both and the actual inverses . The limiting automorphism satisfies . The detailed alternating correction inequalities, the protected inverse images, and the substitution are retained in the key proof Card; this route does not duplicate that proof.

For one fixed approximately inner automorphism, shell matching gives and , where . At the root class , the chosen family uses and . Each other component uses one automorphism for all of its shells. The generic projection-matching theorem is not a new proof of the general KOS proposition. The same chosen homogeneity family is used in the construction of the algebra and in the classification of its irreducible representations.

Exact Card references

Boundary Inputs

The displayed edges preserve dependency paths through omitted helpers. Levels count selected predecessors within this scope. Mathematical citations remain distinct from formal dependencies.

Exact source and provider boundary · Earlier 466-declaration Project view and PDF

Dependency-first reading route

Levels belong to this reading scope. Follow prerequisites or uses to focus the route.

8 declarations

Level 0

Level 0Focus target

Approximately inner homogeneity of pure CAR states

MathlibAnnex.CStarAlgebra.CAR.PureStateHomogeneity

The homogeneity property asks for exact state transport by an automorphism that is locally approximable by inner automorphisms.

Immediate prerequisites in this Project
None in this scope

Used by in this Project
Two-sided inner sequences imply pure-state homogeneity

Open Declaration CardRead exact source
Level 0Focus target

A two-sided inner intertwining sequence for two states

MathlibAnnex.CStarAlgebra.CAR.HasInnerIntertwiningSequence

An inner sequence records both forward and actual inverse convergence data before any limiting automorphism is constructed.

Immediate prerequisites in this Project
None in this scope

Used by in this Project
Two-sided inner sequences imply pure-state homogeneity, Pure CAR states admit two-sided inner intertwining sequences

Open Declaration CardRead exact source
Level 0Focus target

Exact projection links for one approximately inner automorphism

MathlibAnnex.CStarAlgebra.exists_shell_family_of_approximately_inner

A point-norm approximation followed by close-projection conjugacy gives exact support identities for an arbitrary projection family.

Immediate prerequisites in this Project
None in this scope

Used by in this Project
Choosing the CAR shell family from proved homogeneity

Open Declaration CardRead exact source
Level 0Focus target

A fixed representative family of CAR shell data

MathlibAnnex.CStarAlgebra.CAR.RepresentativeShellFamily

One family records a transporting automorphism and exact shell links for each selected pure-state class, with an explicitly fixed root component.

Immediate prerequisites in this Project
None in this scope

Used by in this Project
Choosing the CAR shell family from proved homogeneity

Open Declaration CardRead exact source

Level 1

Level 1Focus target

Two-sided inner sequences imply pure-state homogeneity

MathlibAnnex.CStarAlgebra.CAR.homogeneity_of_innerIntertwiningSequences

The forward and inverse limits close the homogeneity argument once an intertwining sequence is supplied for every pure-state pair.

Immediate prerequisites in this Project
Approximately inner homogeneity of pure CAR states, A two-sided inner intertwining sequence for two states

Used by in this Project
Pure-state homogeneity of the completed CAR algebra

Open Declaration CardRead exact source
Level 1Focus target

Pure CAR states admit two-sided inner intertwining sequences

MathlibAnnex.CStarAlgebra.CAR.hasInnerIntertwiningSequence_of_pure

Finite-set vector-state transport supplies explicit corrections; their summable conjugation bounds and state estimates yield the required two-sided sequence.

Immediate prerequisites in this Project
A two-sided inner intertwining sequence for two states

Used by in this Project
Pure-state homogeneity of the completed CAR algebra

Open Declaration CardRead exact source

Level 2

Level 2Focus target

Pure-state homogeneity of the completed CAR algebra

MathlibAnnex.CStarAlgebra.CAR.homogeneity

The constructed inner intertwining sequences discharge the supplier hypothesis and give an approximately inner transporting automorphism.

Immediate prerequisites in this Project
Two-sided inner sequences imply pure-state homogeneity, Pure CAR states admit two-sided inner intertwining sequences

Used by in this Project
Choosing the CAR shell family from proved homogeneity

Open Declaration CardRead exact source

Level 3

Level 3Focus target

Choosing the CAR shell family from proved homogeneity

MathlibAnnex.CStarAlgebra.CAR.homogeneityShellFamily

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

Immediate prerequisites in this Project
Exact projection links for one approximately inner automorphism, A fixed representative family of CAR shell data, Pure-state homogeneity of the completed CAR algebra

Used by in this Project
None in this scope

Open Declaration CardRead exact source
Back to top ↑