LemmaStatement: AI-adaptedProof: AI-adaptedprecheck pass

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.

Nondimensionalisation of the one-dimensional stationary equation and of the WKB exponent

Statement

Let $ℓ > 0$ and $E_{⋆} > 0$ be real reference scales, let $m > 0$ and $ℏ > 0$ be real, and define $h : = \frac{ℏ}{ℓ \sqrt{2 m E_{⋆}}} > 0.$ Let $I \subseteq R$ be a nonempty open interval, let $W \in C^{2} (I; R)$ , let $λ \in R$ , and let $u : I \to C$ be a function. Then:

(a) $u$ is of class $C^{2}$ on $I$ and satisfies $u^{''} (ξ) = \frac{W (ξ) - λ}{h^{2}} u (ξ) (ξ \in I)$ if and only if the function $ψ : ℓ I \to C$ , $ψ (x) : = u (x / ℓ)$ , is of class $C^{2}$ on the open interval $ℓ I = {ℓ ξ : ξ \in I}$ and satisfies $- \frac{ℏ^{2}}{2 m} ψ^{''} (x) + E_{⋆} W (x / ℓ) ψ (x) = E_{⋆} λ ψ (x) (x \in ℓ I);$

(b) if $a < b$ are points of $I$ , then each of the following identities holds under its indicated strict-sign hypothesis:

(i) if $W (ξ) - λ > 0$ for every $ξ \in [a, b]$ , then $\frac{1}{h} \int_{a}^{b} \sqrt{W (ξ) - λ} d ξ = \frac{1}{ℏ} \int_{ℓ a}^{ℓ b} \sqrt{2 m (E_{⋆} W (x / ℓ) - E_{⋆} λ)} d x;$

(ii) if $λ - W (ξ) > 0$ for every $ξ \in [a, b]$ , then $\frac{1}{h} \int_{a}^{b} \sqrt{λ - W (ξ)} d ξ = \frac{1}{ℏ} \int_{ℓ a}^{ℓ b} \sqrt{2 m (E_{⋆} λ - E_{⋆} W (x / ℓ))} d x .$

All square roots here are the nonnegative real square roots of strictly positive numbers. Part (i) is the forbidden-region exponent identity; part (ii) is the allowed-region phase identity.

The identities are statements about the displayed functions and integrals only. The number $h$ is dimensionless because $ℏ$ is in $J s$ and $ℓ \sqrt{2 m E_{⋆}}$ is in $k g m^{2} s^{- 1} = J s$ ; no physical interpretation, no approximation and no error estimate is asserted here.

Facts & Assumptions

Given: the scales $ℓ, E_{⋆}, m, ℏ$ , the interval $I$ , the functions $W, u$ , the number $λ$ , and the number $h > 0$ . For part (b), also take points $a < b$ in $I$ satisfying the strict-sign hypothesis for the part being proved.

[F1]

Chain rule. If $g$ is differentiable at $c$ and $f$ differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ; the statement applies to real and imaginary parts separately (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 derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

[F2]

One-dimensional change of variables. If $φ$ is $C^{1}$ and injective on a neighbourhood of $[a, b]$ with $φ^{'} \neq 0$ there, and $f$ is continuous on an interval containing $φ ([a, b])$ , then $\int_{\min φ ([a, b])}^{\max φ ([a, b])} f (y) d y = \int_{a}^{b} f (φ (ξ)) ∣ φ^{'} (ξ) ∣ d ξ$ (In one dimension the compact-Jordan formula is substitution over the unoriented image interval with the absolute derivative).

Proof

technique · direct; differentiate the affine substitution twice by its chain rule and substitute the definition of $h$, then integrate by the one-dimensional change of variables in each strict-sign case

Given: the data of the statement and [F1]-[F2].

1.1F1

[Second derivatives under the substitution] Since $ξ \mapsto ℓ ξ$ is $C^{1}$ with derivative $ℓ$ and inverse $x \mapsto x / ℓ$ , the map $ψ = u \circ (\cdot / ℓ)$ is $C^{2}$ exactly when $u$ is, and by [F1] applied twice, $ψ^{'} (x) = \frac{u^{'} (x / ℓ)}{ℓ}, ψ^{''} (x) = \frac{u^{''} (x / ℓ)}{ℓ^{2}} (x \in ℓ I) .$

1.2givenalgebra

[The scale identity] From the definition of $h$ and $W$ , $E_{⋆} > 0$ , $h^{2} = \frac{ℏ^{2}}{2 m ℓ^{2} E_{⋆}}, hence \frac{1}{h^{2} ℓ^{2}} = \frac{2 m E_{⋆}}{ℏ^{2}} .$

1.3F2givenalgebra

[Forbidden-region exponent identity (b)(i)] On $[a, b]$ the function $x \mapsto ℓ x$ is $C^{1}$ and strictly increasing with derivative $ℓ > 0$ , and the integrand $f_{+} (x) : = \sqrt{2 m (E_{⋆} W (x / ℓ) - E_{⋆} λ)}$ is continuous on $[ℓ a, ℓ b]$ because $W - λ > 0$ . By [F2] applied to $φ (ξ) = ℓ ξ$ , $\int_{ℓ a}^{ℓ b} f_{+} (x) d x = ℓ \sqrt{2 m E_{⋆}} \int_{a}^{b} \sqrt{W (ξ) - λ} d ξ .$ Dividing by $ℏ$ and using $ℓ \sqrt{2 m E_{⋆}} / ℏ = 1 / h$ gives (b)(i).

2.1step 1.1step 1.2algebra

[Forward implication of (a)] Suppose $u$ is $C^{2}$ with $u^{''} = (W - λ) u / h^{2}$ on $I$ . By step 1.1, $ψ$ is $C^{2}$ on $ℓ I$ and $ψ^{''} (x) = \frac{u^{''} (x / ℓ)}{ℓ^{2}} = \frac{1}{ℓ^{2}} \cdot \frac{W (x / ℓ) - λ}{h^{2}} u (x / ℓ) = \frac{2 m E_{⋆}}{ℏ^{2}} (W (x / ℓ) - λ) ψ (x),$ by step 1.2. Multiplying by $- ℏ^{2} / (2 m)$ and bringing $ψ$ terms to the left gives $- (ℏ^{2} / 2 m) ψ^{''} + E_{⋆} W (x / ℓ) ψ = E_{⋆} λ ψ$ on $ℓ I$ .

2.2step 1.1step 1.2algebra

[Converse implication of (a)] Suppose conversely that $ψ$ is $C^{2}$ with $- \frac{ℏ^{2}}{2 m} ψ^{''} + E_{⋆} W (x / ℓ) ψ = E_{⋆} λ ψ$ on $ℓ I$ . By step 1.1, $u (ξ) = ψ (ℓ ξ)$ is $C^{2}$ on $I$ with $u^{''} (ξ) = ℓ^{2} ψ^{''} (ℓ ξ)$ ; substituting the assumed equation at $x = ℓ ξ$ gives $u^{''} (ξ) = ℓ^{2} \cdot \frac{2 m}{ℏ^{2}} (E_{⋆} W (ξ) - E_{⋆} λ) ψ (ℓ ξ) = \frac{2 m ℓ^{2} E_{⋆}}{ℏ^{2}} (W (ξ) - λ) u (ξ) = \frac{W (ξ) - λ}{h^{2}} u (ξ),$ the last equality by step 1.2.

3.1F2givenalgebra∎

[Allowed-region phase identity (b)(ii)] If instead $λ - W > 0$ on $[a, b]$ , then $f_{-} (x) : = \sqrt{2 m (E_{⋆} λ - E_{⋆} W (x / ℓ))}$ is continuous and real on $[ℓ a, ℓ b]$ . The same change of variables gives $\int_{ℓ a}^{ℓ b} f_{-} (x) d x = ℓ \sqrt{2 m E_{⋆}} \int_{a}^{b} \sqrt{λ - W (ξ)} d ξ .$ Division by $ℏ$ and the same scale identity prove (b)(ii), with the nonnegative real square roots justified by the strict sign hypothesis.

Remarks

Role of the lemma. The lemma is the exact bookkeeping that lets the dimensionless equation $u^{''} = (W - λ) u / h^{2}$ , in which the semiclassical parameter $h$ is explicit, be read as the physical line-model equation with potential $E_{⋆} W (\cdot / ℓ)$ at energy $E_{⋆} λ$ . Both the equation and the phase integral transfer exactly; no approximation is involved.
Small $h$ . The regime $h ≪ 1$ is the regime $ℏ ≪ ℓ \sqrt{2 m E_{⋆}}$ ; the lemma itself makes no smallness assumption, and the error theorems that use smallness state it separately.

Nondimensionalisation of the one-dimensional stationary equation and of the WKB exponent

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources