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.

Fock Creation and Annihilation Operators Satisfy the CAR

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a complex Hilbert space with inner product linear in the first variable, and let $F_{-} (H)$ be its fermionic Fock space. The creation rule $C (f) ξ = f \land ξ$ extends to a bounded operator on $F_{-} (H)$ with $∥ C (f) ∥ = ∥ f ∥$ . Writing $A (f) = C (f)^{*}$ for its adjoint, one has, for all $f, g \in H$ ,

${C (f), C (g)} = 0, {A (f), A (g)} = 0, {A (f), C (g)} = ⟨ g, f ⟩ I .$

Thus $f \mapsto C (f)$ is a bounded complex-linear CAR family in the convention of Finite-Dimensional CAR Algebra over an Inner-Product Space.

Facts & Assumptions

Given: Countable Choice, a complex Hilbert space $H$ , its fermionic Fock space, and vectors $f, g \in H$ .

[F1]

The Fock space is the Hilbert completion of the orthogonal direct sum of the Hilbert exterior powers; the vacuum is $1 \in Λ^{0} H$ (Fermionic Fock Space over a Complex Hilbert Space).

[F2]

The local tensor powers use the product pairing, their antisymmetrizers are the signed permutation averages $A_{n}$ , and $x_{1} \land \dots \land x_{n} = \sqrt{n!} A_{n} (x_{1} \otimes \dots \otimes x_{n})$ . Wedges of decomposable vectors have inner product $⟨ x_{1} \land \dots \land x_{k}, y_{1} \land \dots \land y_{k} ⟩ = \det [⟨ x_{i}, y_{j} ⟩]$ (Hilbert exterior powers and induced operators).

[F3]

The inner product on $H$ is linear in its first variable and conjugate-linear in its second (Real and complex inner-product spaces and their induced length).

[A1]

Countable Choice is assumed for the canonical Hilbert tensor/Fock construction and Hilbert-space adjoints (The Axiom of Countable Choice ( ${A C}_{ω}$ ), Schwartz/distribution spaces and Hilbert Fock conventions, The Hilbert-space adjoint of a bounded operator).

[F4]

Under [A1], every bounded operator on a Hilbert space has a bounded adjoint, and $∥ T^{*} ∥ = ∥ T ∥$ (The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities).

[F5]

Under Countable Choice, the canonical fermionic Fock creation and annihilation operators are bounded adjoints with norms $∥ f ∥$ and satisfy the CAR on the whole Fock space, using the second-variable-linear pairing $⟨ f, g ⟩_{2}$ (Bosonic and fermionic Fock operators with exact domains).

[F6]

The canonical Fock space is the square-summable direct sum of antisymmetric tensor sectors; its pairing is $⟨ f, g ⟩_{2} = ⟨ g, f ⟩$ , its vacuum is $(1, 0, \dots)$ , and sector creation is $c^{†} (f) ξ = \sqrt{n + 1} A_{n + 1} (f \otimes ξ)$ (Schwartz/distribution spaces and Hilbert Fock conventions).

[F7]

Completed Hilbert tensor products have the product pairing and dense elementary tensors; completions are identified by the unique surjective linear isometry fixing the dense algebraic tensor product (Hilbert tensor construction: inner product, completion and product bases).

Proof

1.1givenA1F1F2F3F5F6F7construct

Reverse the canonical second-variable pairing as in [F6], so all tensor pairings are linear in the first variable. The identity on elementary tensors preserves the product pairings of [F2, F7]; by their dense spans and completion uniqueness it extends, degree by degree, to a surjective linear isometry between the local and canonical tensor powers. It intertwines every permutation on the dense elementary tensors and hence the finite averages $A_{n}$ , so it restricts to an isometry $J_{n}$ of their antisymmetric sectors; set $J_{0} = I_{C}$ . Their orthogonal direct sum is an isometry on finite sector sums. The local Fock space is its completion by [F1], and finite sector sums are dense in the canonical square-summable Fock space by [F5, F6]. Thus it extends to a surjective linear isometry $J$ between the Fock spaces, taking the local vacuum to the canonical vacuum.

2.1F1F2F6step 1.1algebra

The permutation averages satisfy $A_{n + 1} (I \otimes A_{n}) = A_{n + 1}$ : applying any permutation of the last $n$ factors before $A_{n + 1}$ multiplies it by that permutation's sign, and the signed average cancels this sign. Hence, for $n \geq 1$ , on a decomposable $n$ -wedge $ξ = x_{1} \land \dots \land x_{n}$ , the normalization in [F2] gives $c^{†} (f) J_{n} ξ = \sqrt{n + 1} \sqrt{n!} A_{n + 1} (f \otimes A_{n} (x_{1} \otimes \dots \otimes x_{n})) = J_{n + 1} (f \land ξ)$ by [F6]. For $n = 0$ , both sides send the scalar vacuum to $f$ . Thus the local creation rule on its dense decomposable subspace is $J^{- 1} c^{†} (f) J$ .

3.1givenA1F1F4F5F6step 1.1step 2.1algebra∎

By [F5] and step 2.1, $C (f)$ extends to $J^{- 1} c^{†} (f) J$ with norm $∥ f ∥$ . The adjoint identity and uniqueness in [F4] give $A (f) = J^{- 1} c (f) J$ . Transporting the canonical CAR of [F5] through $J$ gives the two zero anticommutators and ${A (f), C (g)} = ⟨ f, g ⟩_{2} I = ⟨ g, f ⟩ I$ by [F6]. Creation is complex-linear in $f$ on the dense wedge subspace and therefore after bounded extension. This includes $f = 0$ and $H = {0}$ , whose Fock space retains the vacuum line.

Remarks

This proof transports the canonical published mathematical Fock result through the explicit normalization and pairing identification; it does not reprove that supplier. The annihilation map $f \mapsto A (f)$ is conjugate-linear under the stated first-variable-linear inner-product convention. The creation map $f \mapsto C (f)$ is complex-linear.

Depends on

Used by

CAR over a Hilbert Space Has the Universal Inductive-Limit Norm Theorem

Dependency tree · two levels

57 results within two dependency steps 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 and 6.7 (standard reference, not scraped)
Jan Dereziński, Introduction to Representations of the Canonical Commutation and Anticommutation Relations, §§4.1 and 5.7 (standard reference, not scraped)