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.

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.

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
In the source Mathematical meaning
H; rho; hrho is a complete nonzero complex Hilbert space and is the irreducible unital representation of the CAR algebra.
F : Finset Limit; hepsilon : 0 < epsilon First fix the finite protected set and error .
∃ n, ∃ delta > 0, ∀ (xi eta : H) Choose a stage and tolerance depending on those inputs, before the subsequent pair . The same choices work for every pair satisfying the following tests.
‖xi‖ = 1 → ‖eta‖ = 1 → Both later vectors must have norm . There is no hypothesis that is small.
∀ i j : Fin (2 ^ n) Test all ordered matrix-unit indices , including off-diagonal entries.
‖Representation.vectorFunctional rho xi (...) - Representation.vectorFunctional rho eta (...)‖ < delta The test is for every , where .
∃ u : unitary Limit; rho (u : Limit) xi = eta One unitary transports the first vector exactly: .
∃ p : Path 1 u For that same , a norm-continuous unitary path starts at and ends at .
∀ t, ∀ a ∈ F; (p t : Limit); star (p t : Limit) For every path time and every protected , read as an element of and star as its adjoint .
‖(p t : Limit) * a * star (p t : Limit) - a‖ < epsilon The forward protection bound .
‖star (p t : Limit) * a * (p t : Limit) - a‖ < epsilon The inverse protection bound . The conjunction requires both bounds for the same path, at all times; only the endpoint vector transport is exact.

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.exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt

Accepted content SHA-256: 4ecae37fb3730b21e78322eac8be7116da10bce283a2a5933d6221cf29568ce0

Accepted source guide SHA-256: 863815c7f5df11510bf9144042514a61a6de3932c77fc5badbda8170be1532c7

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑