ExampleConstruction: AI-generatedVerification: 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.

Ground energy units

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Fix $m, ω, ℏ > 0$ and let $ℓ = \sqrt{ℏ / (m ω)}$ , $ψ_{n}$ , $H_{o s c}$ be as in Oscillator scaling and exact realization. Then:

(a) the spectrum of $H_{o s c}$ is exactly ${ℏ ω (n + \frac{1}{2}) : n \in N}$ ; measured in units of $ℏ ω$ the eigenvalues are $n + \frac{1}{2}$ , the ground energy is

$\frac{E_{0}}{ℏ ω} = \frac{1}{2},$

and every consecutive gap is $1$ unit: $\frac{E_{n + 1} - E_{n}}{ℏ ω} = 1$ ;

(b) the ground eigenvector is the Gaussian

$ψ_{0} (x) = π^{- 1 / 4} ℓ^{- 1 / 2} e^{- x^{2} / (2 ℓ^{2})},$

and it satisfies the eigenvalue equation pointwise:

$- \frac{ℏ^{2}}{2 m} ψ_{0}^{''} (x) + \frac{m ω^{2}}{2} x^{2} ψ_{0} (x) = \frac{ℏ ω}{2} ψ_{0} (x) (x \in R);$

(c) for the isotropic $d$ -dimensional oscillator of Multidimensional oscillator completeness(d) with common frequency $ω$ , the ground energy is $\frac{d}{2} ℏ ω$ in the same units, in particular $\frac{3}{2} ℏ ω$ for $d = 3$ , and all gaps within one coordinate direction are $ℏ ω$ ;

(d) no other value of the ground energy is compatible with the displayed spectrum: $E_{0}$ is the infimum of $σ (H_{o s c})$ .

No physical identification of $ℏ ω$ with a measured energy is made; the statements are about the operator $H_{o s c}$ built from the positive parameters.

Facts & Assumptions

Given: positive reals $m, ω, ℏ$ ; $ℓ = \sqrt{ℏ / (m ω)}$ ; the oscillator operator $H_{o s c} = \frac{ℏ ω}{2} D A D^{- 1}$ with basis $(ψ_{n})$ .

[F1]

$H_{o s c}$ is self-adjoint with complete orthonormal eigenbasis $(ψ_{n})$ , $H_{o s c} ψ_{n} = ℏ ω (n + \frac{1}{2}) ψ_{n}$ , and $σ (H_{o s c}) = {ℏ ω (n + \frac{1}{2}) : n \in N}$ (Oscillator scaling and exact realization(b)).

[F2]

$ψ_{0} = D g_{0}$ with $g_{0} (y) = π^{- 1 / 4} e^{- y^{2} / 2}$ , $ℓ = \sqrt{ℏ / (m ω)}$ , and for every $f = D (p g_{0})$ one has $H_{o s c} f = - \frac{ℏ^{2}}{2 m} f^{''} + \frac{m ω^{2}}{2} x^{2} f$ pointwise (Oscillator scaling and exact realization(a),(c), Hermite recurrence(a)).

[F3]

$(e^{- x^{2} / (2 ℓ^{2})})^{'} = - \frac{x}{ℓ^{2}} e^{- x^{2} / (2 ℓ^{2})}$ and $(e^{- x^{2} / (2 ℓ^{2})})^{''} = (- \frac{1}{ℓ^{2}} + \frac{x^{2}}{ℓ^{4}}) e^{- x^{2} / (2 ℓ^{2})}$ by the product rule, the chain rule and $(\exp)^{'} = \exp$ (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$ , 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)$ , The exponential function is smooth and $(\exp)^{'} = \exp$ , The complex exponential by its power series).

[F4]

$\frac{ℏ^{2}}{2 m ℓ^{2}} = \frac{ℏ ω}{2}$ and $\frac{ℏ^{2}}{2 m ℓ^{4}} = \frac{m ω^{2}}{2}$ , because $ℓ^{2} = ℏ / (m ω)$ (Oscillator scaling and exact realization).

Verification

1.1F1algebra

[(a) levels] By [F1], each $ψ_{n}$ is a unit eigenvector with eigenvalue $ℏ ω (n + \frac{1}{2})$ , and $σ (H_{o s c})$ is exactly the set of these numbers. Hence $E_{0} = ℏ ω / 2$ , so $E_{0} / (ℏ ω) = \frac{1}{2}$ , and $E_{n + 1} - E_{n} = ℏ ω$ for every $n$ , so $(E_{n + 1} - E_{n}) / (ℏ ω) = 1$ .

1.2F1algebra

[(c) $d$ -dimensional ground energy] In the isotropic $d$ -dimensional operator $H$ of Multidimensional oscillator completeness(d), the eigenvalues are $ℏ ω (M + \frac{d}{2})$ , $M \in N$ , so the smallest is $ℏ ω \cdot \frac{d}{2}$ : the ground energy is $\frac{d}{2} ℏ ω$ , equal to $\frac{3}{2} ℏ ω$ for $d = 3$ , and the increment of $M$ by one raises the energy by $ℏ ω$ .

2.1step 1.1F2F3F4algebra

[(b) ground eigenfunction] By [F2], $ψ_{0} (x) = ℓ^{- 1 / 2} π^{- 1 / 4} e^{- x^{2} / (2 ℓ^{2})}$ . Using [F3], $- \frac{ℏ^{2}}{2 m} ψ_{0}^{''} + \frac{m ω^{2}}{2} x^{2} ψ_{0} = [\frac{ℏ^{2}}{2 m ℓ^{2}} + (- \frac{ℏ^{2}}{2 m ℓ^{4}} + \frac{m ω^{2}}{2}) x^{2}] ψ_{0}$ , and by [F4] the coefficient of $x^{2}$ vanishes while the constant term is $\frac{ℏ ω}{2}$ ; hence $H_{o s c} ψ_{0} = \frac{ℏ ω}{2} ψ_{0}$ pointwise, in agreement with $H_{o s c} ψ_{0} = ℏ ω (0 + \frac{1}{2}) ψ_{0}$ from [F1].

3.1step 1.1F1∎

[(d) minimality] By [F1] the spectrum is the closed discrete set ${ℏ ω (n + \frac{1}{2}) : n \in N}$ , whose infimum is its least element $ℏ ω / 2 = E_{0}$ ; no smaller value belongs to the spectrum.

Ground energy units

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources