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.

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.

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 : ℂ)⁻¹
In the source Mathematical meaning
family : RepresentativeShellFamily The fixed shell family with the support and root identities in the assumptions, in the completed CAR algebra .
i : GNSClass Limit; n : ℕ The source index i is the pure-GNS class of the statement, and is the matrix stage. The same is used for every .
transportedFlag family i n The projection , where is the first diagonal matrix projection at stage .
trace (transportedFlag family i n) The normalized CAR trace evaluated on that projection: .
(2 ^ n : ℂ)⁻¹ The complex scalar , the reciprocal of . Thus the entire conclusion is ; it is not a norm estimate or a different trace.

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

Accepted content SHA-256: 02f1c27aed575feb2cdc51875db9628f600760d4193bfd1892dd0da4503470e1

Accepted source guide SHA-256: dc5162fe0f69e0168370cfd0740e6474d04f946cdfb1c3e3c144610693d3ae50

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑