LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite CAR Occupation Operators Give All Matrix Units

Statement

For $n \geq 0$ , let $P_{n}$ be the set of subsets of ${1, \dots, n}$ , and let $F_{n} = ℓ^{2} (P_{n})$ with orthonormal basis $e_{S}$ for $S \in P_{n}$ . For $1 \leq j \leq n$ define operators on this finite-dimensional Hilbert space by

$c_{j} e_{S} = {\begin{cases} 0 & j \notin S, \\ (- 1)^{∣ {s \in S : s < j} ∣} e_{S ∖ {j}} & j \in S, \end{cases} c_{j}^{†} e_{S} = {\begin{cases} (- 1)^{∣ {s \in S : s < j} ∣} e_{S \cup {j}} & j \notin S, \\ 0 & j \in S . \end{cases}$

Then $c_{j}^{†}$ is the Hilbert-space adjoint of $c_{j}$ , and $a_{j} \mapsto c_{j}$ , $a_{j}^{†} \mapsto c_{j}^{†}$ defines a $*$ -representation $π_{n} : {C A R}_{n}^{a l g} \to End (F_{n})$ . Put $N_{j} = c_{j}^{†} c_{j}$ and $P_{\emptyset} = \prod_{j = 1}^{n} (I - N_{j})$ , with the empty product equal to $I$ . For $S = {i_{1} < \dots < i_{p}}$ and $T = {j_{1} < \dots < j_{q}}$ , set

$E_{S, T} = c_{i_{1}}^{†} \dots c_{i_{p}}^{†} P_{\emptyset} c_{j_{q}} \dots c_{j_{1}},$

with empty operator products equal to $I$ . Then $E_{S, T} e_{U} = δ_{T, U} e_{S}$ . Consequently the image of $π_{n}$ is all of $End (F_{n}) ≅ M_{2^{n}} (C)$ .

Facts & Assumptions

Given: An integer $n \geq 0$ , the finite-mode algebra ${C A R}_{n}^{a l g}$ , and the finite set $P_{n}$ .

[F1]

The algebra ${C A R}_{n}^{a l g}$ is generated by $a_{j}, a_{j}^{†}$ subject to ${a_{i}, a_{j}} = 0$ , ${a_{i}^{†}, a_{j}^{†}} = 0$ , and ${a_{i}, a_{j}^{†}} = δ_{i j} 1$ (Finite-Mode Complex CAR Algebra).

Proof

1.1givenconstructalgebra

On basis vectors, $c_{j}^{†}$ reverses exactly the same basis transition as $c_{j}$ and has the same real sign. Hence its matrix is the transpose-conjugate matrix of $c_{j}$ . Each of $c_{j}^{2}$ and $(c_{j}^{†})^{2}$ vanishes because after one allowed toggle, the second toggle of the same type is forbidden. On a basis vector containing $j$ , $c_{j}^{†} c_{j}$ is the identity and $c_{j} c_{j}^{†}$ is zero; when $j$ is absent these roles reverse. Thus ${c_{j}, c_{j}^{†}} = I$ .

2.1givenF1step 1.1algebra

Fix $j < k$ . Whether the $j$ -toggle is allowed depends only on membership of $j$ , and whether the $k$ -toggle is allowed depends only on membership of $k$ . Therefore, if either toggle is forbidden, both orders of the two distinct toggles give zero. If both are allowed, performing the $j$ -toggle first changes the number of occupied indices below $k$ by one, while the $k$ -toggle does not change the number below $j$ . The signs in the displayed formulas therefore differ by $- 1$ when the order is reversed. This proves every distinct-mode anticommutator among $c_{j}, c_{j}^{†}, c_{k}, c_{k}^{†}$ is zero. Along with step 1.1 these are exactly [F1], so the specified map extends through the quotient to a $*$ -representation $π_{n}$ .

2.2givenstep 1.1constructalgebra

The operator $N_{j}$ is diagonal in the basis $e_{S}$ , with eigenvalue $1$ when $j \in S$ and $0$ otherwise. Hence the commuting product $P_{\emptyset}$ is the projection onto $C e_{\emptyset}$ . For $T = {j_{1} < \dots < j_{q}}$ , the right-hand product $c_{j_{q}} \dots c_{j_{1}}$ removes the elements of $T$ in increasing order; on $e_{T}$ each sign is $+ 1$ , and on $e_{U}$ with $T ⊊ U$ its result is a scalar multiple of $e_{U ∖ T}$ . If $T \subseteq̸ U$ it gives zero. The middle projection therefore kills every $e_{U}$ except $e_{T}$ , and sends $e_{T}$ to $e_{\emptyset}$ . The left-hand creation product sends $e_{\emptyset}$ to $e_{S}$ , again with sign $+ 1$ because its indices are applied from largest to smallest. Thus $E_{S, T} e_{U} = δ_{T, U} e_{S}$ .

3.1step 2.2algebra∎

The operators $E_{S, T}$ are all standard matrix units relative to the basis $(e_{S})_{S \in P_{n}}$ , so their linear span is $End (F_{n})$ . Each lies in the $*$ -algebra generated by the $c_{j}, c_{j}^{†}$ , proving surjectivity. For $n = 0$ , the sole basis vector is $e_{\emptyset}$ , $P_{\emptyset} = I$ , and $E_{\emptyset, \emptyset} = I$ , so the same conclusion holds.

Remarks

The construction uses only the finite occupation basis. It does not import an infinite-particle-domain argument or a choice principle.

Depends on

Finite-Mode Complex CAR Algebra

Used by

Dependency tree · one level

1 result within one dependency step of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Günther Hörmann, C*-Algebras with Aspects of Quantum Physics, Chapter 6, §§6.1–6.3 (standard reference, not scraped)
Jan Dereziński, Introduction to Representations of the Canonical Commutation and Anticommutation Relations, §§4.2 and 5.7 (standard reference, not scraped)