MATHLIBANNEX / CANONICAL DECLARATION CARD

Exact vector transport along an almost central unitary path

MathlibAnnex.CStarAlgebra.CAR.exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt

theorem

Finite matrix-state tests ensure exact transport while protecting a prescribed finite set throughout the path.

Statement

Let be the completed CAR algebra: the norm completion of the increasing union of under the unital embeddings (with the fixed coordinate reindexing). Write for the canonical isometric inclusion and for its matrix units. A representation is a unital complex star homomorphism into the bounded operators on a complex Hilbert space. Irreducibility means nonzero action and no proper nonzero closed reducing subspace. We use the inner product conjugate linear in its first argument and write for the vector functional. Fix an irreducible representation on a nonzero complex Hilbert space. Given a finite set and , one can choose a stage and such that the following holds for every pair of unit vectors . If for all , there is with and a norm-continuous path from to . At every time and for every , both and hold.

Assumptions

The representation is unital and irreducible, and is complete and nonzero. The finite set and positive error are fixed first. The stage and tolerance are chosen before either unit vector; there is no hypothesis that the two vectors are already close in norm.

Conclusion

The endpoint transport is exact. The protection of is approximate, in both conjugation directions, uniformly for the entire path. The stage tests compare vector states, not the vectors themselves.

Proof route

Approximate inside one finite stage. Close stage states give close Gram matrices of the root-corner components. Corner involutions yield a stage-central path moving the first vector near the second; a short final unitary correction makes the transport exact. Quantitative commutator bounds then transfer to the original finite set.

Proof steps

  1. For fixed stage , decompose a unit vector as , where . The sums of squared component norms equal , and . Thus entrywise state tests are Gram-matrix tests.

  2. The corner Gram-perturbation result uses an auxiliary isometric family orthogonal to both input families. Two unitary involutions move through that family with small errors. Lifting them to corner exponentials gives a path centralizing the whole stage at every time. Reconstructing the vectors converts small component errors into a small vector error.

  3. The fixed-stage exact-transport lemma follows by correcting this endpoint with a unitary near and concatenating its short path with the stage-central path. For any prescribed , its path satisfies for all stage elements and all times, while the endpoint sends exactly to .

  4. Choose stage approximants to each within , and choose small relative to their common norm bound. The commutator of with is bounded by twice the approximation error plus the stage commutator bound, which is strictly below . Multiplication by the appropriate unitary converts that commutator bound into each of the two conjugation inequalities.

Main citations

Lean source signature (exact)

theorem exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] [Nontrivial H]
    (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho)
    (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :
    ∃ n, ∃ delta > 0, ∀ (xi eta : H), ‖xi‖ = 1 → ‖eta‖ = 1 →
      (∀ i j : Fin (2 ^ n),
        ‖Representation.vectorFunctional rho xi (limitMatrixUnit n i j) -
          Representation.vectorFunctional rho eta (limitMatrixUnit n i j)‖ < delta) →
      ∃ u : unitary Limit,
        rho (u : Limit) xi = eta ∧
        ∃ p : Path 1 u, ∀ t, ∀ a ∈ F,
          ‖(p t : Limit) * a * star (p t : Limit) - a‖ < epsilon ∧
          ‖star (p t : Limit) * a * (p t : Limit) - a‖ < epsilon

Here rho is , F and epsilon are the protected set and error, and n, delta are chosen before xi, eta. limitMatrixUnit n i j is . A witness p : Path 1 u is the norm-continuous unitary path. The two conjuncts under ∀ t ... are forward and inverse conjugation control at every time.

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

Lean realization notes

The path need not centralize exactly. The tolerance is an existential modulus and no numerical value is claimed. The conditions require all the matrix entries at the chosen stage, not only the diagonal ones.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 1 · SHA-256: 1e9fb7fc9b494074a274a3ff8761c90c7e53a2912f3e44d0d802a187b38fd865

Exposition revision: 1 · SHA-256: 53f094249210aff8dbd7bdefe8255d2592b33fb7f88a190d5b324139b5025f34

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 0caf0d8a7930bf2d085fd18437214ef182e3258384dc824ca8959c40de7bcbde

Back to top ↑