MATHLIBANNEX / CANONICAL DECLARATION CARD

Pure CAR states admit two-sided inner intertwining sequences

MathlibAnnex.CStarAlgebra.CAR.hasInnerIntertwiningSequence_of_pure

theorem

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

Statement

Let be the completed CAR algebra, the norm completion of the matrix stages under , with the fixed coordinate reindexing. A state means a positive continuous complex-linear functional taking value at the identity; a pure state is an extreme point of this convex state space. For a unitary , write . For every pair of pure states on , there is a sequence such that, for every , both and are norm-Cauchy, and .

Assumptions

The input functionals are pure states on the fixed completed CAR algebra. Their GNS representations and unit cyclic vectors are constructed from these states; no identification of their Hilbert spaces, equivalence of their representations, or initial closeness of the two states is assumed.

Conclusion

The required inner intertwining sequence exists for every pure-state pair. Its inverse condition concerns the actual inverses of the produced automorphisms. This is the supplier used by the separate limit theorem.

The implementation also records paths for the local corrections, but this selected theorem only concludes the sequence property. Its proof does not presume a transporting endpoint automorphism or a general KOS principle. All choices below are made once within this construction.

Proof route

Use the finite-set vector-state transport theorem to construct unitaries . Put , , and choose a dense sequence . The corrections are chosen to give, for ,

The first estimates make the four sequences pointwise Cauchy. The second gives the state convergence for . The construction below records the local theorem’s hypothesis, the correction it supplies, and the inequality that enables the next application.

Proof steps

  1. The local estimate used in every correction. Put . Fix an irreducible representation , a finite set , and . The finite-set transport theorem gives a finite matrix-unit test set and . If is a unit vector state of and is a unit vector state of another representation, its hypothesis is

    Under this hypothesis, for every finite and , it gives a unitary such that

    Here is the state of when is the state of . The tests are chosen before . The path supplied by the theorem is not needed for this sequence conclusion.

  2. The quantities to be constructed and the induction hypothesis. Take the irreducible GNS representations with unit cyclic vectors . Choose a dense sequence in , and put and . For unitaries , write

    These are the vector states of and . To control both an automorphism and its inverse, use

    Apply the local theorem to , obtaining . The induction hypothesis is the explicit inequality

    It enables the local theorem to change toward with any later finite request. Purity is used to make both GNS representations irreducible; they will be used in separate applications of the theorem.

  3. Initialize the induction without assuming that and are close. First obtain from the local theorem for . The unrestricted approximation theorem supplies with

    Now is fixed. Obtain for . The displayed inequality enables the theorem with and . Request and . Its output satisfies

    With , this is exactly the induction hypothesis at .

  4. Construct and obtain the estimate that will imply state convergence. Assume the induction hypothesis at . First obtain from the local theorem for . Apply the already enabled theorem to , , with

    Let be its output, and define

    The theorem gives the two estimates

    In the first line both signs are required. Restricting the second line to gives

    which is precisely the hypothesis for the next application. Restricting it instead to gives

    This second restriction, not merely closeness on the matrix units, will give .

  5. Construct and verify the next induction hypothesis. Since is now fixed, obtain for . Apply the theorem enabled in the preceding step, using

    For its output , set

    The conclusions are

    The second line is the induction hypothesis at . Thus every correction is supplied by the finite-set transport theorem, and every required stage-test hypothesis is the preceding correction’s conclusion. The test sets are always chosen before the correction that must meet them.

  6. Derive all four Cauchy estimates. For , protection of and gives, respectively,

    The first equality uses that is isometric. The second explains why was included in . The estimates give the same two bounds for and . Consequently, for any of the four sequences and ,

    For arbitrary , isometry then gives

    First approximate by a fixed , then let . This proves the four pointwise Cauchy assertions. It does not assert norm convergence of the unitaries .

  7. Form the inner automorphisms and check their actual inverses. Define

    The previous step implies pointwise convergence of each of the four sequences, since is complete. To see explicitly that the two compositions are Cauchy, use the following estimate. If are pointwise Cauchy isometries, let and . Then

    Apply this once with and once with . It proves the required Cauchy conditions for and its actual inverse .

  8. Obtain the state convergence by substitution. For , the boxed estimate in the construction of becomes

    This is why the requested set contained and why the output pairs with , rather than with . For every , contractivity of the states and isometry of give

    Density, followed by , yields . Together with innerness and the two Cauchy conditions, this is exactly .

Main citations

Supporting route explanation

Lean source signature (exact)

theorem hasInnerIntertwiningSequence_of_pure
    (phi psi : Limit →L[ℂ] ℂ)
    (hphi : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) (hpsi : MathlibAnnex.CStarAlgebra.IsPureState Limit psi) :
    HasInnerIntertwiningSequence phi psi
In the source Mathematical meaning
phi psi : Limit →L[ℂ] ℂ Given continuous complex-linear functionals on the CAR completion .
hphi : IsPureState Limit phi; hpsi : IsPureState Limit psi Both are pure states: positive, normalized, and extreme in the real convex state space.
HasInnerIntertwiningSequence phi psi The output is one sequence of star automorphisms with all following requirements: for every , both and its actual inverse image are norm-Cauchy; for every , for a unitary ; and for every . No implementing-unitary convergence is required.
HasInnerIntertwiningSequence This conclusion imposes no initial closeness of the states, no supplied GNS representations and no path condition. The GNS vectors and alternating corrections described in the Proof steps are constructed inside the proof.

Further source notes: In the linked GNS proof, rho, sigma are , and xi, eta are their unit cyclic vectors. In the transition proof, s.move is the local theorem specialized using the displayed induction hypothesis. The proof hBclose verifies the inequality, and hAclose verifies the next inequality. These names occur in the linked proof, not in the displayed signature.

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

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.hasInnerIntertwiningSequence_of_pure

Accepted content SHA-256: c6d6fce2b9893aeedf2db10812f4fc28f8c84bdbc2748e40903266d7ddd1ee28

Accepted source guide SHA-256: a5cdfcdde49a35e0f0cd34d3ffbeb626e4124d9f646fc6d4a03980478a6e9bd2

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑