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.

Coherent-state convergence

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H = L^{2} (R, d y)$ with inner product linear in the first argument, let $(g_{n})_{n \in N}$ be the Hermite family of Hermite recurrence, and let $a, a^{†}, N$ be the closed ladder operators and number operator of Closed ladder domains with domains $D (a), D (a^{†}), D (N)$ and $N = a^{†} a$ on $D (N)$ . For $z \in C$ put

$ψ_{z} : = e^{- ∣ z ∣^{2} / 2} \sum_{n = 0}^{\infty} \frac{z^{n}}{\sqrt{n!}} g_{n},$

the series being taken in $L^{2}$ . Then:

(a) the series converges in $L^{2}$ , $∥ ψ_{z} ∥ = 1$ , and $ψ_{z} = e^{- ∣ z ∣^{2} / 2} \sum_{n = 0}^{\infty} \frac{z^{n}}{\sqrt{n!}} g_{n}$ is the unique element of $L^{2}$ with coefficients $c_{n} = e^{- ∣ z ∣^{2} / 2} z^{n} / \sqrt{n!}$ in the basis $(g_{n})$ ;

(b) $ψ_{z} \in D (N^{k})$ for every $k \in N$ , where $N^{k}$ is the $k$ -fold iterate of $N$ with domain $D (N^{k}) = {x : \sum_{n} n^{2 k} ∣ ⟨ x, g_{n} ⟩ ∣^{2} < \infty}$ ; in particular

$\sum_{n} n^{2 k} ∣ c_{n} ∣^{2} = e^{- ∣ z ∣^{2}} \sum_{n = 0}^{\infty} \frac{n^{2 k} ∣ z ∣^{2 n}}{n!} < \infty;$

(c) $a ψ_{z} = z ψ_{z}$ (so $ψ_{z}$ is a unit eigenvector of the annihilation operator with eigenvalue $z$ ), and $∥ a ψ_{z} ∥^{2} = ∣ z ∣^{2}$ ;

(d) $⟨ ψ_{z}, ψ_{w} ⟩ = e^{- (∣ z ∣^{2} + ∣ w ∣^{2}) / 2 + z \overline{w}} = e^{- ∣ z - w ∣^{2} / 2} e^{i Im (z \overline{w})}$ for all $z, w \in C$ , so $∥ ψ_{z} - ψ_{w} ∥^{2} = 2 (1 - e^{- ∣ z - w ∣^{2} / 2} \cos (Im (z \overline{w})))$ and the map $z \mapsto ψ_{z}$ is injective;

(e) $⟨ N ψ_{z}, ψ_{z} ⟩ = ∣ z ∣^{2}$ and $∥ a^{†} ψ_{z} ∥^{2} = ∣ z ∣^{2} + 1$ , and $ψ_{0} = g_{0}$ .

The completeness of $(g_{n})$ (Hermite completeness) is used for uniqueness from the prescribed coefficients in (a) and to invoke the closed ladder operators of Closed ladder domains on a complete orthonormal family. Series convergence and normalization use orthonormality and Hilbert-space completeness; the operator and moment conclusions use the supplied closed ladder domains.

Facts & Assumptions

Given: the Hermite family $(g_{n})$ with its ladder operators $a, a^{†}, N$ ; a complex number $z$ ; the numbers $c_{n} = e^{- ∣ z ∣^{2} / 2} z^{n} / \sqrt{n!}$ .

[F1]

$⟨ g_{n}, g_{m} ⟩ = δ_{n m}$ (Hermite orthogonality(a)), and $L^{2}$ is a complex Hilbert space under Countable Choice ( $L^{2}$ with the integral pairing is a Hilbert space). Finite orthogonal sums satisfy $∥ \sum_{n \in E} a_{n} g_{n} ∥^{2} = \sum_{n \in E} ∣ a_{n} ∣^{2}$ . Thus a series $\sum_{n} a_{n} g_{n}$ converges exactly when $\sum_{n} ∣ a_{n} ∣^{2} < \infty$ : finite tail norms give the Cauchy criterion and Hilbert-space completeness gives the limit; conversely convergence bounds the partial norms. Continuity of the norm and inner product gives the sum's squared norm and its coefficients.

[F2]

On $D (N)$ one has $a^{†} a = N$ , $a a^{†} = N + I$ ; $D (a a^{†}) = D (a^{†} a) = D (N)$ ; and $a$ is closed with $a^{*} = a^{†}$ (Closed ladder domains(b),(d)).

[F3]

$e^{t} = \sum_{n \geq 0} t^{n} / n!$ for complex $t$ , the series converging absolutely (The complex exponential by its power series, The complex exponential series converges absolutely for every complex argument); powers and integer powers of complex numbers are those of the library's power conventions. The addition law $e^{v + w} = e^{v} e^{w}$ and agreement with the real exponential are $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential; for real $x, y$ , $e^{x + i y} = e^{x} (\cos y + i \sin y)$ and $∣ e^{x + i y} ∣ = e^{x}$ are $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ . Positivity and $e^{- x} = 1 / e^{x}$ are The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , and strict increase is The exponential function is strictly increasing.

[F4]

If $0 \leq a_{n + 1} \leq \frac{1}{2} a_{n}$ for all $n \geq N$ , then $\sum_{n \geq N} a_{n} \leq 2 a_{N}$ , by comparison with the geometric series $\sum_{k} 2^{- k} = 2$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

[F5]

$a g_{n} = \sqrt{n} g_{n - 1}$ for $n \geq 1$ with $a g_{0} = 0$ ; $a^{†} g_{n} = \sqrt{n + 1} g_{n + 1}$ (Hermite recurrence(e)).

[F6]

The Hermite family is complete: any $h \in L^{2}$ with $⟨ h, g_{n} ⟩ = 0$ for every $n$ is zero (Hermite completeness(b)).

Proof

1.1givenF1F3F6

[Convergence and normalization] For $N \geq M$ , the partial sums $S_{N} : = e^{- ∣ z ∣^{2} / 2} \sum_{n \leq N} \frac{z^{n}}{\sqrt{n!}} g_{n}$ satisfy $∥ S_{N} - S_{M} ∥^{2} = e^{- ∣ z ∣^{2}} \sum_{M < n \leq N} \frac{∣ z ∣^{2 n}}{n!}$ by [F1]. As $N, M \to \infty$ the right side tends to $0$ because $\sum_{n} \frac{∣ z ∣^{2 n}}{n!} = e^{∣ z ∣^{2}} < \infty$ by [F3]; hence $(S_{N})$ is Cauchy and $ψ_{z} : = \lim_{N} S_{N} \in L^{2}$ exists, and taking limits in the same identity gives $∥ ψ_{z} ∥^{2} = e^{- ∣ z ∣^{2}} \sum_{n} \frac{∣ z ∣^{2 n}}{n!} = 1$ . For fixed $n$ , inner-product continuity gives $⟨ ψ_{z}, g_{n} ⟩ = \lim_{M \to \infty} ⟨ S_{M}, g_{n} ⟩ = c_{n}$ . If $x \in L^{2}$ has these same coefficients, then $⟨ x - ψ_{z}, g_{n} ⟩ = 0$ for every $n$ , so $x = ψ_{z}$ by completeness [F6].

2.1step 1.1F1F2F4algebra

[Number domains] For $k = 0$ use $N^{0} = I$ , $D (N^{0}) = H$ and $n^{0} = 1$ , including $n = 0$ ; step 1.1 proves the assertion. Now fix $k \geq 1$ and let $a_{n} : = n^{2 k} ∣ z ∣^{2 n} / n! \geq 0$ . If $z = 0$ , $ψ_{0} = g_{0}$ , which lies in every $D (N^{k})$ and all terms $a_{n}$ with $n \geq 1$ vanish. If $z \neq 0$ , for $n \geq 1$ , $\frac{a_{n + 1}}{a_{n}} = (\frac{n + 1}{n})^{2 k} \frac{∣ z ∣^{2}}{n + 1} \to 0$ , so there is $N$ with $a_{n + 1} \leq \frac{1}{2} a_{n}$ for $n \geq N$ ; by [F4], $\sum_{n \geq N} a_{n} \leq 2 a_{N} < \infty$ , and the finitely many initial terms are finite. Hence $\sum_{n} n^{2 k} ∣ c_{n} ∣^{2} = e^{- ∣ z ∣^{2}} \sum_{n} a_{n} < \infty$ . Since $D (N^{k}) = {x : \sum_{n} n^{2 k} ∣ ⟨ x, g_{n} ⟩ ∣^{2} < \infty}$ (inducting the domain formula of Closed ladder domains(a): $N^{j} x$ has coefficients $n^{j} ⟨ x, g_{n} ⟩$ , and the weight $n^{2 k}$ dominates every lower weight for $n \geq 1$ ), this says $ψ_{z} \in D (N^{k})$ .

2.2step 1.1F2F5algebra

[ $a ψ_{z} = z ψ_{z}$ ] Each partial sum $S_{N}$ is a finite combination of the $g_{n}$ , so $S_{N} \in D (N) \subseteq D (a)$ ; by [F5], $a S_{N} = e^{- ∣ z ∣^{2} / 2} \sum_{n = 1}^{N} z^{n} \sqrt{n} g_{n - 1} / \sqrt{n!} = z e^{- ∣ z ∣^{2} / 2} \sum_{m = 0}^{N - 1} \frac{z^{m}}{\sqrt{m!}} g_{m} = z S_{N - 1}$ . As $N \to \infty$ , $S_{N} \to ψ_{z}$ and $a S_{N} \to z ψ_{z}$ by step 1.1; since $a$ is closed [F2], $ψ_{z} \in D (a)$ and $a ψ_{z} = z ψ_{z}$ . Taking norms, $∥ a ψ_{z} ∥ = ∣ z ∣$ by (a).

2.3step 1.1F1F3algebra

[Inner products] For $z, w \in C$ , $⟨ ψ_{z}, ψ_{w} ⟩ = e^{- (∣ z ∣^{2} + ∣ w ∣^{2}) / 2} \sum_{n} \frac{z^{n} {\overline{w}}^{n}}{n!}$ by [F1] applied to the two convergent series, and $\sum_{n} \frac{(z \overline{w})^{n}}{n!} = e^{z \overline{w}}$ by [F3] applied to the series of the complex number $z \overline{w}$ ; hence $⟨ ψ_{z}, ψ_{w} ⟩ = e^{- (∣ z ∣^{2} + ∣ w ∣^{2}) / 2 + z \overline{w}} = e^{- ∣ z - w ∣^{2} / 2} e^{i Im (z \overline{w})}$ . Its modulus is $e^{- ∣ z - w ∣^{2} / 2}$ . Then $∥ ψ_{z} - ψ_{w} ∥^{2} = ∥ ψ_{z} ∥^{2} + ∥ ψ_{w} ∥^{2} - 2 Re ⟨ ψ_{z}, ψ_{w} ⟩ = 2 (1 - e^{- ∣ z - w ∣^{2} / 2} \cos (Im (z \overline{w})))$ . When $z \neq w$ the overlap modulus is strictly less than $1$ , so this distance is positive; when $z = w$ it is zero; the map is injective.

3.1step 1.1step 2.1F1F2F3algebra∎

[Number and creation moments] By step 2.1 with $k = 1$ , $ψ_{z} \in D (N)$ and $N ψ_{z}$ has coefficients $n c_{n}$ ; hence $⟨ N ψ_{z}, ψ_{z} ⟩ = \sum_{n} n ∣ c_{n} ∣^{2} = e^{- ∣ z ∣^{2}} \sum_{n} \frac{n ∣ z ∣^{2 n}}{n!}$ . The series reindexes as $∣ z ∣^{2} \sum_{m \geq 0} \frac{∣ z ∣^{2 m}}{m!} = ∣ z ∣^{2} e^{∣ z ∣^{2}}$ by [F3], so the value is $∣ z ∣^{2}$ . Next, $∥ a^{†} ψ_{z} ∥^{2} = ⟨ a^{†} ψ_{z}, a^{†} ψ_{z} ⟩ = ⟨ ψ_{z}, a a^{†} ψ_{z} ⟩ = ⟨ ψ_{z}, (N + I) ψ_{z} ⟩ = ∣ z ∣^{2} + 1$ using [F2] and $ψ_{z} \in D (N)$ . Finally $ψ_{0} = g_{0}$ since all coefficients with $n \geq 1$ vanish and $∥ ψ_{0} ∥ = 1$ .

Coherent-state convergence

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources