LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)

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.

Unitary lift to bosonic Fock space

Statement

Assume Countable Choice The Axiom of Countable Choice ( ${A C}_{ω}$ ). Let $H$ and $K$ be complex Hilbert spaces and let $U : H \to K$ be unitary. The sector maps $U^{\otimes n}$ restrict to unitaries $U_{s}^{(n)} : H_{s}^{(n)} \to K_{s}^{(n)}$ ; their direct sum $Γ_{s} (U) = ⨁_{n = 0}^{\infty} U_{s}^{(n)}$ is unitary, maps vacuum to vacuum, and maps the finite-particle domain $D_{f i n} (H)$ onto $D_{f i n} (K)$ . It intertwines the creation and annihilation maps: $Γ_{s} (U) a_{H}^{†} (h) Γ_{s} (U)^{- 1} = a_{K}^{†} (U h), Γ_{s} (U) a_{H} (h) Γ_{s} (U)^{- 1} = a_{K} (U h)$ on the finite-particle domain. If $G$ is a topological space and $g \mapsto U_{g}$ is a family of unitaries such that $g \mapsto U_{g} h$ is norm-continuous for every $h \in H$ , then $g \mapsto Γ_{s} (U_{g})$ has the same continuity property on $F_{s} (H)$ .

Facts & Assumptions

Given: Countable Choice; the symmetric tensor-sector Fock conventions and creation/annihilation formulas of Schwartz/distribution spaces and Hilbert Fock conventions.

[A1]

Countable Choice is the choice assumption used for the completed tensor and sector constructions. The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

Fock space is the Hilbert direct sum of symmetric tensor powers, the vacuum is the zeroth sector, finite-particle vectors are dense, and creation and annihilation are the symmetrized tensor-insertion and contraction maps. Schwartz/distribution spaces and Hilbert Fock conventions

[F2]

Hilbert tensor products are completed from elementary tensors, and permutation averaging is the orthogonal projection onto the symmetric subspace. Hilbert tensor construction: inner product, completion and product bases Permutation sector projections on the n-fold tensor power

Proof

1.1A1F1F2givenalgebra

Since $U$ is unitary, $U^{\otimes n}$ is unitary on the completed tensor power by its isometric action on elementary tensors and its inverse $(U^{- 1})^{\otimes n}$ . It commutes with every tensor-factor permutation, because both compositions send an elementary tensor to $U h_{π (1)} \otimes \dots \otimes U h_{π (n)}$ . It therefore commutes with the symmetric averaging projection of [F2] and restricts to a unitary $U_{s}^{(n)}$ on its range. The zeroth sector is the identity on $C$ .

2.1F1F2step 1.1givenalgebra

The direct sum of the sector unitaries preserves the sum of squared sector norms and has inverse $⨁_{n} (U^{- 1})_{s}^{(n)}$ , so it is unitary. It fixes the zeroth-sector vacuum and preserves finite sums of sectors in both directions. On an elementary symmetric tensor, applying the Fock creation formula before or after this direct sum gives the symmetrization of $U h$ together with the images of the original tensor factors; hence the two creation maps intertwine. The annihilation formula is its adjoint contraction and the same tensor calculation replaces each contracted vector $h$ by $U h$ . Linearity, boundedness on each fixed sector, and density of elementary tensors extend both identities to $D_{f i n}$ .

3.1F1step 1.1givenalgebra∎

Fix $n$ . For an elementary tensor, $∥ U_{g}^{\otimes n} (h_{1} \otimes \dots \otimes h_{n}) - U_{g_{0}}^{\otimes n} (h_{1} \otimes \dots \otimes h_{n}) ∥ \leq \sum_{r = 1}^{n} \prod_{s \neq r} ∥ h_{s} ∥ ∥ (U_{g} - U_{g_{0}}) h_{r} ∥,$ by the telescoping expansion of the tensor difference and unitary norm preservation. Strong continuity of $U_{g}$ makes the right side tend to zero. Density of elementary tensors and the uniform norm bound $1$ extend continuity to the completed sector and its closed symmetric subspace. Finite sector sums are dense by [F1]; approximating an arbitrary Fock vector by such a sum and using $∥ Γ_{s} (U_{g}) ∥ = 1$ proves strong continuity on the whole direct sum.

Depends on

Dependency tree · 2 levels

Sources

David Tong, Quantum Field Theory, section 2.4