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.

Oscillator scaling and exact realization

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Fix real parameters $m > 0$ , $ω > 0$ , $ℏ > 0$ , put $ℓ : = \sqrt{ℏ / (m ω)} > 0$ , and let $g_{0}, P, (g_{n})_{n \in N}$ be the Hermite data of Hermite recurrence in $L^{2} (R, d y)$ , so that $(g_{n})$ is a complete orthonormal family by Hermite completeness. Define

$D : L^{2} (R, d y) \to L^{2} (R, d x), (D f) (x) : = ℓ^{- 1 / 2} f (x / ℓ),$

and let $A$ be the self-adjoint diagonal operator of Diagonal adjoint and graph-core lemma for the complete orthonormal family $(g_{n})$ and the eigenvalues $λ_{n} = 2 n + 1$ , with the core $P$ and spectrum ${2 n + 1 : n \in N}$ (Diagonal spectrum).

Then:

(a) $D$ is a linear isometry of $L^{2} (R, d y)$ onto $L^{2} (R, d x)$ with two-sided inverse $(D^{- 1} g) (y) = ℓ^{1 / 2} g (ℓ y)$ ; the functions $ψ_{n} : = D g_{n}$ , $ψ_{n} (x) = ℓ^{- 1 / 2} g_{n} (x / ℓ)$ , form a complete orthonormal family of $L^{2} (R, d x)$ ;

(b) the operator

$H_{o s c} : = \frac{ℏ ω}{2} D A D^{- 1}, D (H_{o s c}) : = {f \in L^{2} (R, d x) : D^{- 1} f \in D (A)},$

is self-adjoint, satisfies $H_{o s c} ψ_{n} = ℏ ω (n + \frac{1}{2}) ψ_{n}$ for every $n$ , and has

$D (H_{o s c}) = {f : \sum_{n} ℏ^{2} ω^{2} (n + \frac{1}{2})^{2} ∣ c_{n} ∣^{2} < \infty}, H_{o s c} f = \sum_{n} ℏ ω (n + \frac{1}{2}) c_{n} ψ_{n},$

where $c_{n} : = ⟨ D^{- 1} f, g_{n} ⟩ = ⟨ f, ψ_{n} ⟩$ ; its spectrum is $σ (H_{o s c}) = {ℏ ω (n + \frac{1}{2}) : n \in N}$ , its ground energy is $ℏ ω / 2$ with eigenvector $ψ_{0}$ , and $⟨ H_{o s c} f, f ⟩ \geq \frac{ℏ ω}{2} ∥ f ∥^{2}$ for every $f \in D (H_{o s c})$ ;

(c) $D (P) = span {ψ_{n}}$ is a core for $H_{o s c}$ , and for every polynomial $p$ the function $f : = D (p g_{0})$ is $C^{\infty}$ on $R$ with

$H_{o s c} f = - \frac{ℏ^{2}}{2 m} f^{''} + \frac{m ω^{2}}{2} x^{2} f$

pointwise on $R$ ;

(d) for every $f \in D (H_{o s c})$ and every test function $φ \in C_{c}^{\infty} (R)$ ,

$\int_{R} (H_{o s c} f) (x) φ (x) d x = \int_{R} f (x) (- \frac{ℏ^{2}}{2 m} φ^{''} (x) + \frac{m ω^{2}}{2} x^{2} φ (x)) d x,$

so $H_{o s c}$ is the self-adjoint realization of the differential expression $- \frac{ℏ^{2}}{2 m} \frac{d^{2}}{d x^{2}} + \frac{m ω^{2}}{2} x^{2}$ in the weak sense; no identification of $D (H_{o s c})$ with a separately defined maximal differential-operator domain is asserted.

All parameters enter as positive real numbers; no physical identification of $m, ω, ℏ$ with measured quantities is made.

Facts & Assumptions

Given: real $m, ω, ℏ > 0$ ; $ℓ = \sqrt{ℏ / (m ω)}$ ; the complete orthonormal family $(g_{n})$ in $L^{2} (R, d y)$ ; the diagonal operator $A$ with $A g_{n} = (2 n + 1) g_{n}$ ; the map $D$ and the vectors $ψ_{n} = D g_{n}$ .

[F1]

$(g_{n})$ is orthonormal and complete in $L^{2} (R, d y)$ , hence a Hilbert basis; coefficients in expansions are $⟨ f, g_{n} ⟩$ and $\sum_{n} ∣ ⟨ f, g_{n} ⟩ ∣^{2} = ∥ f ∥^{2}$ (Hermite orthogonality, Hermite completeness, Complex Lp classes and Euclidean test-function conventions).

[F2]

$A$ has domain $D (A) = {f : \sum_{n} (2 n + 1)^{2} ∣ ⟨ f, g_{n} ⟩ ∣^{2} < \infty}$ , action $A g_{n} = (2 n + 1) g_{n}$ , is self-adjoint with $σ (A) = {2 n + 1 : n \in N}$ , and its algebraic eigenvector span is a core for $A$ ; the Hermite polynomials $H_{n}$ have degree $n$ with nonzero leading coefficient, so triangular elimination gives $P = span {g_{n}}$ ; also $⟨ A f, f ⟩ \geq ∥ f ∥^{2}$ for $f \in D (A)$ (Diagonal adjoint and graph-core lemma(b),(d),(e), Diagonal spectrum, Hermite recurrence(f)).

[F3]

$(- \partial_{y}^{2} + Y^{2}) φ = A φ$ for $φ \in P$ ; explicitly $- φ^{''} + y^{2} φ = 2 a^{†} a φ + φ$ on $P$ and $A g_{n} = (2 n + 1) g_{n}$ (Hermite orthogonality(b), [F2]).

[F4]

For a $C^{1}$ diffeomorphism $T : U \to V$ of open subsets of $R$ and $h \in L^{1} (V)$ , $\int_{V} h (y) d y = \int_{U} h (T (x)) ∣ T^{'} (x) ∣ d x$ (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions).

[F5]

$∥ u v ∥_{1} \leq ∥ u ∥_{2} ∥ v ∥_{2}$ ; the real chain and product rules for derivatives, applied componentwise to complex-valued functions under the convention of Complex Lp classes and Euclidean test-function conventions (Cauchy-Schwarz inequality for $L^{2}$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ); and for real $G \in C^{1} [a, b]$ with integrable derivative, $\int_{a}^{b} G^{'} = G (b) - G (a)$ (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[F6]

$C_{c}^{\infty} (R) \subseteq L^{2} (R)$ and, for $g \in C_{c}^{\infty} (R)$ , $g^{''} \in L^{2}$ and $x \mapsto x^{2} g (x) \in L^{2}$ ; the integral pairing $(u, φ) \mapsto \int u φ$ satisfies $∣ \int u φ ∣ \leq ∥ u ∥_{2} ∥ φ ∥_{2}$ (Test function space d of an open set, Complex Lp classes and Euclidean test-function conventions, [F5]).

Proof

1.1givenF4algebra

[ $D$ is a bijective isometry] Define $D$ initially on a measurable representative $u$ of an $L^{2} (d y)$ class by the representative $ℓ^{- 1 / 2} u (x / ℓ)$ . With $T (x) = x / ℓ$ in [F4], $\int h (x / ℓ) d x = ℓ \int h (y) d y$ for every $h \in L^{1} (R)$ . If $u, v$ represent the same class, apply this identity to $h = ∣ u - v ∣^{2} \in L^{1}$ : then $∥ ℓ^{- 1 / 2} (u - v) (\cdot / ℓ) ∥_{2}^{2} = ∥ u - v ∥_{2}^{2} = 0$ , so $D$ is independent of the representative. Applying the same change of variables to $∣ u ∣^{2}$ gives $∥ D u ∥^{2} = ℓ^{- 1} \int ∣ u (x / ℓ) ∣^{2} d x = ∥ u ∥^{2}$ ; $D$ is linear, hence a linear isometry. The formula $D^{- 1} v (y) : = ℓ^{1 / 2} v (ℓ y)$ is also independent of representatives by the same change of variables, is linear, and satisfies $D (D^{- 1} v) = v$ and $D^{- 1} (D u) = u$ as $L^{2}$ classes. Thus $D$ is a bijective linear isometry.

2.1step 1.1F1

[Transport of the orthonormal basis] By step 1.1 and the definition $ψ_{n} = D g_{n}$ , for all $m, n$ we have $⟨ ψ_{n}, ψ_{m} ⟩_{L^{2} (d x)} = \int ℓ^{- 1} g_{n} (x / ℓ) \overline{g_{m} (x / ℓ)} d x = \int g_{n} (y) \overline{g_{m} (y)} d y = δ_{n m}$ by the substitution of step 1.1 applied to $g_{n} \overline{g_{m}} \in L^{1}$ and [F1]. If $h \in L^{2} (d x)$ satisfies $⟨ h, ψ_{n} ⟩ = 0$ for all $n$ , then $⟨ D^{- 1} h, g_{n} ⟩ = ⟨ h, ψ_{n} ⟩ = 0$ for all $n$ because $D$ is an isometry, so $D^{- 1} h = 0$ by completeness of $(g_{n})$ and $h = 0$ . Hence $(ψ_{n})$ is a complete orthonormal family.

3.1step 1.1step 2.1F1F2

[ $H_{o s c}$ is the diagonal operator in the transported basis] Let $B$ be the diagonal operator of Diagonal adjoint and graph-core lemma for the complete orthonormal family $(ψ_{n})$ and the eigenvalues $λ_{n}^{'} = ℏ ω (n + \frac{1}{2})$ , so $D (B) = {f : \sum_{n} (λ_{n}^{'})^{2} ∣ ⟨ f, ψ_{n} ⟩ ∣^{2} < \infty}$ and $B f = \sum_{n} λ_{n}^{'} ⟨ f, ψ_{n} ⟩ ψ_{n}$ . By that lemma and Diagonal spectrum, $B$ is self-adjoint with $σ (B) = \overline{{λ_{n}^{'}}} = {ℏ ω (n + \frac{1}{2})}$ (a closed discrete set) and $⟨ B f, f ⟩ \geq \frac{ℏ ω}{2} ∥ f ∥^{2}$ because $λ_{n}^{'} \geq \frac{ℏ ω}{2}$ . We claim $B = H_{o s c}$ as operators. First, $⟨ f, ψ_{n} ⟩ = ⟨ D^{- 1} f, g_{n} ⟩$ by the isometry of step 1.1 applied to $f = D (D^{- 1} f)$ and $ψ_{n} = D g_{n}$ ; hence $D (H_{o s c}) = {f : D^{- 1} f \in D (A)} = D (B)$ . Second, if $f \in D (H_{o s c})$ and $c_{n} = ⟨ D^{- 1} f, g_{n} ⟩$ , then $D^{- 1} f \in D (A)$ means $\sum_{n} (2 n + 1)^{2} ∣ c_{n} ∣^{2} < \infty$ , and the series $\sum_{n} (2 n + 1) c_{n} g_{n}$ converges in $L^{2}$ to $A D^{- 1} f$ by [F2]; since $D$ is a bijective isometry it preserves limits of series, so $H_{o s c} f = \frac{ℏ ω}{2} D (\sum_{n} (2 n + 1) c_{n} g_{n}) = \sum_{n} ℏ ω (n + \frac{1}{2}) c_{n} ψ_{n} = B f$ , and $\sum_{n} (λ_{n}^{'})^{2} ∣ c_{n} ∣^{2} = \frac{ℏ^{2} ω^{2}}{4} \sum_{n} (2 n + 1)^{2} ∣ c_{n} ∣^{2} < \infty$ . Hence $B = H_{o s c}$ , giving self-adjointness, the eigenvalue formulas $H_{o s c} ψ_{n} = ℏ ω (n + \frac{1}{2}) ψ_{n}$ , the spectrum, the domain formula, the ground energy $ℏ ω / 2$ and the lower bound.

4.1step 3.1F2F3F5algebra

[The differential expression on the core] For a polynomial $p$ put $F : = p g_{0} \in P$ and $f : = D F$ , so $f (x) = ℓ^{- 1 / 2} p (x / ℓ) g_{0} (x / ℓ)$ . By the chain rule and product rule [F5], $f$ is $C^{\infty}$ with $f^{'} (x) = ℓ^{- 3 / 2} F^{'} (x / ℓ)$ and $f^{''} (x) = ℓ^{- 5 / 2} F^{''} (x / ℓ)$ . Since $ℏ^{2} / (2 m ℓ^{2}) = ℏ ω / 2$ and $m ω^{2} ℓ^{2} / 2 = ℏ ω / 2$ by $ℓ^{2} = ℏ / (m ω)$ , for all $x$ one has $- \frac{ℏ^{2}}{2 m} f^{''} (x) + \frac{m ω^{2}}{2} x^{2} f (x) = ℓ^{- 1 / 2} (- \frac{ℏ^{2}}{2 m ℓ^{2}} F^{''} + \frac{m ω^{2} ℓ^{2}}{2} y^{2} F) ∣_{y = x / ℓ} = \frac{ℏ ω}{2} ℓ^{- 1 / 2} (- F^{''} + y^{2} F) (x / ℓ)$ . By [F3], $- F^{''} + y^{2} F = A F$ as functions on $R$ , because the operator identity on $P$ holds for the smooth representatives; hence the right side equals $\frac{ℏ ω}{2} (D A F) (x) = H_{o s c} f (x)$ by step 3.1. This proves the pointwise identity. Moreover, if $\deg p \leq m$ , then $H_{0}, \dots, H_{m}$ have respective degrees $0, \dots, m$ and nonzero leading coefficients by Hermite recurrence; triangular elimination shows that they span all polynomials of degree at most $m$ . Since $g_{n} = H_{n} g_{0} / \sqrt{2^{n} n!}$ , every $p g_{0} \in P$ is a finite linear combination of the $g_{n}$ , and the reverse inclusion follows from $g_{n} \in P$ . Thus $P = span {g_{n}}$ and $D (P) = span {ψ_{n}}$ . Since $P$ is a core for $A$ by [F2], its image under the unitary $D$ is a core for $H_{o s c} = \frac{ℏ ω}{2} D A D^{- 1}$ : for $f \in D (H_{o s c})$ with $D^{- 1} f \in D (A)$ choose $φ_{k} \in P$ with $φ_{k} \to D^{- 1} f$ and $A φ_{k} \to A D^{- 1} f$ ; then $D φ_{k} \to f$ and $H_{o s c} (D φ_{k}) = \frac{ℏ ω}{2} D A φ_{k} \to \frac{ℏ ω}{2} D A D^{- 1} f = H_{o s c} f$ .

5.1step 4.1F5F6

[Weak identity for general elements] Let $f \in D (H_{o s c})$ and $φ \in C_{c}^{\infty} (R)$ ; put $S φ : = - \frac{ℏ^{2}}{2 m} φ^{''} + \frac{m ω^{2}}{2} x^{2} φ$ , an element of $L^{2} (R)$ by [F6]. By step 4.1 with the core $D (P)$ , choose $f_{k} \in D (P)$ with $f_{k} \to f$ and $H_{o s c} f_{k} \to H_{o s c} f$ in $L^{2}$ . For each $k$ , write $f_{k} = D F$ with $F \in P$ ; by applying [F5] separately to the real and imaginary parts on $[- R, R]$ , and using the fact that $F$ is a polynomial times $g_{0}$ , whose products with $φ$ and their derivatives tend to $0$ at $\pm \infty$ , integrating by parts twice gives $\int_{R} (- \frac{ℏ^{2}}{2 m} f_{k}^{''} + \frac{m ω^{2}}{2} x^{2} f_{k}) φ d x = \int_{R} f_{k} (- \frac{ℏ^{2}}{2 m} φ^{''} + \frac{m ω^{2}}{2} x^{2} φ) d x$ . By step 4.1 the left side is $\int (H_{o s c} f_{k}) φ$ . Letting $k \to \infty$ , [F6] and [F5] give $∣ \int (H_{o s c} f_{k} - H_{o s c} f) φ ∣ \leq ∥ H_{o s c} f_{k} - H_{o s c} f ∥_{2} ∥ φ ∥_{2} \to 0$ and $∣ \int (f_{k} - f) S φ ∣ \leq ∥ f_{k} - f ∥_{2} ∥ S φ ∥_{2} \to 0$ , so the identity of the statement holds for $f$ .

6.1step 2.1step 3.1step 4.1step 5.1∎

[Summary of the hypotheses used] The construction uses only the completeness of $(g_{n})$ (step 2.1), the diagonal lemma and spectrum (step 3.1), the eigenvalue equation on $P$ (step 4.1) and the two integration-by-parts limits (step 5.1); no claim identifies $D (H_{o s c})$ with the domain of a maximal differential expression, and no physical meaning is attached to $m, ω, ℏ$ or to $f$ .

Oscillator scaling and exact realization

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources