TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Single-mode thermal trace

Statement

Assume the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The Axiom of Choice). Let $ω > 0$ and $β > 0$ be real parameters, let $F (C)$ be the one-mode Fock space with its complete orthonormal family $(e_{n})_{n \in N}$ and number operator $N$ as in Fixed-mode number law and Number operator domain, and define the operator $G_{β} \in B (F (C))$ by $G_{β} e_{n} : = e^{- β ω n} e_{n} (n \in N)$ together with bounded linear extension. Then:

(a) $G_{β}$ is a bounded self-adjoint positive operator with $∥ G_{β} ∥ = 1$ , and $G_{β} = ⨁_{n \in N} e^{- β ω n} i d$ on the Fock sectors (A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum);

(b) the series of weights converge, $Z (β) : = \sum_{n \in N} e^{- β ω n} = \frac{1}{1 - e^{- β ω}}, \sum_{n \in N} n e^{- β ω n} = \frac{e^{- β ω}}{(1 - e^{- β ω})^{2}};$

(c) $G_{β}$ is trace class with $∥ G_{β} ∥_{1} = tr G_{β} = Z (β)$ (Trace class operator, Trace of a trace class operator);

(d) $ρ_{β} : = G_{β} / Z (β)$ is a density operator on $F (C)$ (Density operators and scalar spectral probability), and its number expectation, defined by the absolutely convergent spectral sum $⟨ N ⟩_{β} : = \sum_{n} n e^{- β ω n} / Z (β)$ , equals $⟨ N ⟩_{β} = \frac{e^{- β ω}}{1 - e^{- β ω}} = \frac{1}{e^{β ω} - 1};$ more generally $\sum_{n} n^{k} e^{- β ω n} < \infty$ for every $k \geq 1$ .

The parameter $β$ is a positive real parameter of the model; its identification with an inverse temperature, and the interpretation of $ρ_{β}$ as a physical thermal state, are additional physical assumptions not asserted here.

Facts & Assumptions

Given: the real parameters $ω > 0$ , $β > 0$ , the one-mode Fock space $F (C)$ with complete orthonormal family $(e_{n})_{n \in N}$ and number operator $N$ , and the bounded operator $G_{β}$ defined on the orthonormal family by $G_{β} e_{n} = e^{- β ω n} e_{n}$ .

[F1]

$(e_{n})_{n \in N}$ is a complete orthonormal family of the Hilbert space $F (C)$ ; $N$ is self-adjoint with $N e_{n} = n e_{n}$ (Fixed-mode number law, Number operator domain).

[F2]

For real scalars $c_{n}$ on every sector $ran P_{+}^{(n)}$ , including $c_{0}$ on $C$ , the direct-sum theorem makes $⨁_{n} c_{n} i d$ bounded and self-adjoint when $\sup_{n} ∣ c_{n} ∣ < \infty$ , with norm $\sup_{n} ∣ c_{n} ∣$ (Hilbert direct-sum construction (f)); when $c_{n} \geq 0$ , positivity follows from $⟨ (⨁_{n} c_{n} i d) ψ, ψ ⟩ = \sum_{n} c_{n} ∥ ψ_{n} ∥^{2} \geq 0$ . A bounded operator agreeing with another bounded operator on a complete orthonormal family agrees everywhere (A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[F3]

Geometric series: $\sum_{n \geq 0} q^{n} = 1 / (1 - q)$ for $∣ q ∣ < 1$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges); Tonelli for nonnegative double series permits the interchange of the summation order, even for the extended value $+ \infty$ (Tonelli's theorem for double series of nonnegative extended real numbers).

[F4]

The Fourier-coefficient map $Φ : F (C) \to ℓ^{2} (N, C)$ , $Φ (ψ) = (⟨ ψ, e_{n} ⟩)_{n}$ , is a linear bijection with $∥ Φ (ψ) ∥_{2} = ∥ ψ ∥$ (A Hilbert space with a given orthonormal basis is $ℓ^{2}$ of the index set).

[F5]

Bounded finite-rank operators are compact, norm limits of compact operators into a Hilbert space are compact, and a compact operator with a nuclear representation of summable rank-one norms is trace class with trace norm no greater than that sum (Bounded finite rank operators are compact, Norm limit of compact operators is compact, Nuclear series characterizes trace norm).

[F6]

If $(u_{n})$ is a countable orthonormal family and $w_{n} \geq 0$ with $\sum_{n} w_{n} = 1$ , then $ρ : = \sum_{n} w_{n} T_{u_{n}, u_{n}}$ converges in trace norm to a density operator with $tr ρ = 1$ (Density operators and scalar spectral probability (a)).

[F7]

The complex exponential satisfies $\exp (z + w) = \exp (z) \exp (w)$ for all complex $z, w$ and agrees with the real exponential on real inputs ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

[F8]

For a trace-class operator $T$ and a supplied Hilbert basis $(e_{n})$ , $tr T = \sum_{n} ⟨ T e_{n}, e_{n} ⟩$ and $∣ tr T ∣ \leq ∥ T ∥_{1}$ (Trace is absolutely convergent and basis independent).

Proof

1.1F1F2algebra

[The diagonal weights] For every $n$ the operator $c_{n} i d$ on the nonzero complex Hilbert space $ran P_{+}^{(n)} = C$ has the single real eigenvalue $e^{- β ω n} \in (0, 1]$ , so the direct sum $⨁_{n} e^{- β ω n} i d$ is bounded and self-adjoint with norm $\sup_{n} e^{- β ω n} = 1$ by [F2]; its quadratic form is $\sum_{n} e^{- β ω n} ∥ ψ_{n} ∥^{2} \geq 0$ , so it is positive. By [F1] this direct sum agrees with $G_{β}$ on the complete orthonormal family $(e_{n})$ and therefore equals $G_{β}$ : a bounded operator vanishing on all $e_{n}$ is zero. This proves (a).

1.2F3F7algebra

[The weight sums] Put $q : = e^{- β ω} \in (0, 1)$ . The geometric series [F3] gives $Z (β) = \sum_{n \geq 0} q^{n} = 1 / (1 - q)$ . For the first moment, $\sum_{n \geq 1} n q^{n} = \sum_{n \geq 1} \sum_{m = 1}^{n} q^{n} = \sum_{m \geq 1} \sum_{n \geq m} q^{n}$ , where the interchange of the nonnegative double series is licensed by [F3]; the inner sum is $\sum_{n \geq m} q^{n} = q^{m} / (1 - q)$ by the geometric series, so the total is $\frac{1}{1 - q} \sum_{m \geq 1} q^{m} = \frac{q}{(1 - q)^{2}} < \infty$ . The identity $q / (1 - q) = 1 / (e^{β ω} - 1)$ follows from $e^{β ω} e^{- β ω} = e^{0} = 1$ by [F7]. This proves (b).

2.1F4F5F8step 1.2algebra

[Trace class and its trace] Put $q_{n} : = e^{- β ω n}$ and $R_{N} : = \sum_{n = 0}^{N} q_{n} T_{e_{n}, e_{n}}$ . Each $R_{N}$ is finite rank and compact by [F5]. Parseval [F4] gives $∥ (G_{β} - R_{N}) ψ ∥^{2} = \sum_{n > N} q_{n}^{2} ∣ ⟨ ψ, e_{n} ⟩ ∣^{2} \leq q_{N + 1}^{2} ∥ ψ ∥^{2}$ , so $R_{N} \to G_{β}$ in operator norm and [F5] makes $G_{β}$ compact. The expansion $G_{β} ψ = \sum_{n \geq 0} ⟨ ψ, e_{n} ⟩ (q_{n} e_{n})$ is a nuclear representation with sum $\sum_{n} ∥ e_{n} ∥ ∥ q_{n} e_{n} ∥ = \sum_{n} q_{n} = Z (β)$ ; [F5] therefore gives $∥ G_{β} ∥_{1} \leq Z (β)$ and trace class. By [F8], $tr G_{β} = \sum_{n} ⟨ G_{β} e_{n}, e_{n} ⟩ = \sum_{n} q_{n} = Z (β)$ and $Z (β) = ∣ tr G_{β} ∣ \leq ∥ G_{β} ∥_{1}$ . Thus $∥ G_{β} ∥_{1} = tr G_{β} = Z (β)$ , proving (c).

2.2F3F6step 1.1step 1.2algebra

[The density operator and its number expectation] With $w_{n} : = e^{- β ω n} / Z (β) \geq 0$ and $\sum_{n} w_{n} = 1$ by step 1.2, [F6] gives that $ρ_{β} = \sum_{n} w_{n} T_{e_{n}, e_{n}}$ is a density operator; since $T_{e_{n}, e_{n}}$ is the rank-one projection onto $C e_{n}$ and $G_{β} = \sum_{n} e^{- β ω n} T_{e_{n}, e_{n}}$ (agreement on the complete orthonormal family, step 1.1), one has $ρ_{β} = G_{β} / Z (β)$ . The display defines $⟨ N ⟩_{β}$ as the absolutely convergent sum $\sum_{n} n w_{n}$ ; by step 1.2, $⟨ N ⟩_{β} = \frac{e^{- β ω}}{(1 - e^{- β ω})^{2}} / \frac{1}{1 - e^{- β ω}} = \frac{e^{- β ω}}{1 - e^{- β ω}} = \frac{1}{e^{β ω} - 1}$ . For each integer $k \geq 1$ , put $a : = β ω / 2 > 0$ and $b_{n} : = n^{k} e^{- a n}$ for $n \geq 1$ . Then $b_{n + 1} / b_{n} = (1 + 1 / n)^{k} e^{- a} \to e^{- a} < 1$ , so for some $N$ and $r < 1$ this ratio is at most $r$ for all $n \geq N$ ; hence $(b_{n})$ is bounded. Thus $n^{k} e^{- β ω n} = b_{n} e^{- a n} \leq C_{k} e^{- a n}$ for a finite $C_{k}$ , and the geometric series with ratio $e^{- a} < 1$ gives $\sum_{n} n^{k} e^{- β ω n} < \infty$ .

3.1step 1.1step 1.2step 2.1step 2.2algebra∎

[Conclusion and scope] Steps 1.1-2.2 prove (a)-(d); the displayed series are ordinary absolutely convergent real series and the trace statements use only the supplied spectral data. The closing paragraph of the statement records that the physical reading of $β$ and $ρ_{β}$ requires additional assumptions, so no physical interpretation is asserted here.

Single-mode thermal trace

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources