MATHLIBANNEX / CANONICAL DECLARATION CARD

Shell matching fixes the trace of transported flags

MathlibAnnex.CStarAlgebra.CAR.trace_transportedFlag

theorem

Recovers exact trace values from the initial and final supports of shell links.

Statement

For the completed CAR algebra with normalized trace and a fixed shell family, the transported projection satisfies for every index and every . Here is the root projection at the matrix stage of size .

Assumptions

Let be the completed CAR algebra with matrix stages embedded by . Write for the image of the first diagonal matrix unit, , and for the root state characterized by on each stage, where is its canonical embedding.

Index chosen pure-state Gelfand-Naimark-Segal (GNS) representations by their unitary-equivalence classes , with root index and representative states .

A fixed shell family consists of complex-linear unital star automorphisms and elements satisfying , and .

At the root, is the identity and .

The functional is the normalized CAR trace defined in the trace construction. In particular . The same family and the same automorphism are used for all values of .

Conclusion

Transported flags and root flags have the same trace at each level. This supplies the decaying scalar values needed to estimate their action on vectors implementing the trace.

Proof route

For each shell link, traciality gives . Its support identities turn this into . Both flags start at , so induction forces equal trace values at every level. The root value is the normalized trace of a rank-one diagonal matrix projection.

Proof steps

  1. Use and in the trace identity.

  2. At both flags are . If their traces agree at , equality of the successive differences gives agreement at .

  3. At stage , the root projection has exactly one diagonal entry equal to . Dividing its matrix trace by gives the stated value.

Main citations

Lean source signature (exact)

@[simp]
theorem trace_transportedFlag (family : RepresentativeShellFamily)
    (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) :
    trace (transportedFlag family i n) = (2 ^ n : ℂ)⁻¹

Here Limit is , trace is , and rootFlag n is . The source index i is the index used here. The expression transportedFlag family i n is . The right-hand side is the reciprocal of , regarded as a complex scalar, so the source equality is precisely .

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

Lean realization notes

No new automorphism is chosen and trace-invariance of arbitrary automorphisms is not assumed. The proof uses the exact support identities of the given links and finite induction; it does not infer that the projections themselves converge in operator norm.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:6293f0d949a9d46a65ced9dd45fafd88ff8f5e06fc7a4ab38a0a439f8b1feb1e

Card revision: 1 · SHA-256: ff46ad6b268c1288820f831c4777d7514861ba16ddaf465dfce9eb69ffba7c69

Exposition revision: 1 · SHA-256: 85ba692bd237d55892f80c775d498013680ebb72282e8106668d7b36c051df9d

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 64a92b55ccdd7ee968984ae2784a9b88f70c7c41a5186a7f7fcd4bf2a0a04ab4

Back to top ↑