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.

Smooth local continuity equation and its integrated forms

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Fix $ℏ > 0$ , $m > 0$ , let $Ω \subseteq R^{3}$ and $I \subseteq R$ be nonempty open sets, let $V : Ω \to R$ be continuous and let $ψ : Ω \times I \to C$ be such that $ψ$ , $\partial_{t} ψ$ and all spatial partial derivatives $\partial_{j} ψ$ , $\partial_{k} \partial_{j} ψ$ ( $j, k \in {1, 2, 3}$ ) exist and are continuous on $Ω \times I$ , and $i ℏ \partial_{t} ψ (x, t) = - \frac{ℏ^{2}}{2 m} Δ ψ (x, t) + V (x) ψ (x, t) for every (x, t) \in Ω \times I,$ where $\nabla ψ : = (\partial_{1} ψ, \partial_{2} ψ, \partial_{3} ψ)$ is the spatial gradient and $Δ ψ : = \sum_{j = 1}^{3} \partial_{j} \partial_{j} ψ$ is the classical Laplacian on $R^{3}$ (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ). Define the current $j (x, t) : = \frac{ℏ}{m} Im (\overline{ψ (x, t)} \nabla ψ (x, t)) \in R^{3} .$ Then:

(a) pointwise continuity equation. For every $(x, t) \in Ω \times I$ , $\partial_{t} ∣ ψ ∣^{2} (x, t) + div j (x, t) = 0,$ where the divergence is the classical one of the $C^{1}$ field $x \mapsto j (x, t)$ (Divergence and curl are linear and satisfy the scalar product rules);

(b) integrated balance. If $D \subseteq Ω$ is a bounded open set with $C^{1}$ boundary and $\overline{D} \subseteq Ω$ (Divergence on a bounded C1 Euclidean domain), then $t \mapsto \int_{D} ∣ ψ (x, t) ∣^{2} d x$ is differentiable on $I$ with $\frac{d}{d t} \int_{D} ∣ ψ (x, t) ∣^{2} d x = - \int_{\partial D} j (x, t) \cdot n (x) d S,$ $n$ the outward unit normal;

(c) global conservation under domination. If $Ω = R^{3}$ , if there is $g \in L^{1} (R^{3})$ with $∣ ψ (x, t) ∣^{2} \leq g (x)$ for almost every $x$ and every $t \in I$ , and if $\lim_{R \to \infty} \sup_{t \in I} \int_{{∣ x ∣ = R}} ∣ j (x, t) ∣ d S = 0,$ then, for all $s, t \in I$ such that the closed interval joining $s$ and $t$ is contained in $I$ , $∥ ψ (\cdot, s) ∥_{L^{2} (R^{3})}^{2} = ∥ ψ (\cdot, t) ∥_{L^{2} (R^{3})}^{2};$

(d) norm conservation from unitary dynamics. Assume additionally the Axiom of Choice (The Axiom of Choice). If $K$ is a self-adjoint operator on a complex Hilbert space $H$ and $ψ (t) : = e^{- i t K / ℏ} ψ_{0}$ for some $ψ_{0} \in H$ , then $∥ ψ (t) ∥ = ∥ ψ_{0} ∥$ for every $t \in R$ (A self-adjoint operator generates a strongly continuous unitary group, Integral of a measurable function against a projection-valued measure).

Assertion (d) is independent of the smooth local model of (a)-(c); no interpretation of $∣ ψ ∣^{2}$ as a measured counting rate is asserted.

Facts & Assumptions

Given: $ℏ, m > 0$ , open $Ω \subseteq R^{3}$ , nonempty open time set $I$ , continuous real $V$ , a $C^{2}$ solution $ψ$ of the displayed equation with continuous $\partial_{t} ψ$ , and the current $j$ .

[F1]

The real one-variable product and sum rules are supplied by 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$ . Writing $ψ = u + i v$ with real $u, v$ and restricting to a time or spatial coordinate line gives $\partial_{t} ∣ ψ ∣^{2} = \partial_{t} (u^{2} + v^{2}) = 2 u \partial_{t} u + 2 v \partial_{t} v = 2 Re (\overline{ψ} \partial_{t} ψ)$ and likewise for $\partial_{j} ∣ ψ ∣^{2}$ . Also $j = \frac{ℏ}{m} (u \nabla v - v \nabla u)$ ; the real scalar-vector product rule of Divergence and curl are linear and satisfy the scalar product rules gives $div j = \frac{ℏ}{m} (u Δ v - v Δ u) = \frac{ℏ}{m} Im (\overline{ψ} Δ ψ)$ , since the two gradient inner products cancel.

[F2]

The conjugated equation: $\partial_{t} ψ = \frac{i}{ℏ} (\frac{ℏ^{2}}{2 m} Δ ψ - V ψ)$ , since $V$ is real-valued.

[F3]

Divergence theorem: for a bounded $C^{1}$ domain $D$ and $F \in C^{1} (\overline{D}; R^{3})$ , $\int_{D} div F d x = \int_{\partial D} F \cdot n d S$ (Divergence on a bounded C1 Euclidean domain).

[F4]

Differentiation under the integral sign on an open interval $J \subseteq R$ : if $f : D \times J \to C$ has integrable spatial sections, differentiable time sections outside one measurable null set, measurable spatial sections of its time derivative, and $∣ \partial_{t} f (x, t) ∣ \leq G (x)$ outside one measurable null set for every $t \in J$ , with one nonnegative $G \in L^{1} (D)$ , then $t \mapsto \int_{D} f (x, t) d x$ is differentiable on $J$ with derivative $\int_{D} \partial_{t} f (x, t) d x$ (Differentiation under the integral sign).

[F5]

Dominated convergence, and the fact that an integral over $B_{R}$ of an $L^{1}$ class converges to the integral over $R^{3}$ as $R \to \infty$ (Dominated convergence).

[F6]

A self-adjoint $K$ with spectral PVM $E$ has $e^{- i t K / ℏ} = \int e^{- i t λ / ℏ} d E (λ)$ , a strongly continuous unitary group: each $e^{- i t K / ℏ}$ is unitary, hence norm preserving (A self-adjoint operator generates a strongly continuous unitary group, Integral of a measurable function against a projection-valued measure).

[F7]

If a real function $F$ is continuous on $[s, t]$ , differentiable on $(s, t)$ , and $∣ F^{'} (τ) ∣ \leq M$ there, the mean value theorem gives $∣ F (t) - F (s) ∣ \leq M (t - s)$ (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

Proof

1.1givenF1F2algebra

[The pointwise identity] At a point $(x, t) \in Ω \times I$ , [F2] gives $\partial_{t} ψ = \frac{i}{ℏ} (\frac{ℏ^{2}}{2 m} Δ ψ - V ψ)$ and hence, by [F1], $\partial_{t} ∣ ψ ∣^{2} = 2 Re (\overline{ψ} \partial_{t} ψ) = 2 Re [\frac{i}{ℏ} (\frac{ℏ^{2}}{2 m} \overline{ψ} Δ ψ - V ∣ ψ ∣^{2})] = \frac{ℏ}{m} Re (i \overline{ψ} Δ ψ) = - \frac{ℏ}{m} Im (\overline{ψ} Δ ψ)$ , because the term $- \frac{i}{ℏ} V ∣ ψ ∣^{2}$ is purely imaginary and $V$ is real. Comparing with [F1]'s expression for $div j$ gives $\partial_{t} ∣ ψ ∣^{2} + div j = 0$ , which is (a).

2.1givenstep 1.1F3F4algebra

[The integrated balance] Let $D$ be as in (b). If $D = \emptyset$ , then $\partial D = \emptyset$ , both integrals are zero and (b) holds. Suppose $D \neq \emptyset$ and fix $t_{0} \in I$ . Openness of $I$ gives $ε > 0$ with $[t_{0} - ε, t_{0} + ε] \subseteq I$ ; put $J : = (t_{0} - ε, t_{0} + ε)$ . By step 1.1, $\partial_{t} ∣ ψ ∣^{2} = - div j$ , continuous on the nonempty compact set $\overline{D} \times [t_{0} - ε, t_{0} + ε]$ , so $M : = \max_{\overline{D} \times [t_{0} - ε, t_{0} + ε]} ∣ div j ∣ < \infty$ . Each section $∣ ψ (\cdot, t) ∣^{2}$ is bounded on $\overline{D}$ and integrable on the bounded set $D$ ; its time derivative exists everywhere and has continuous, hence measurable, spatial sections. The fixed majorant $G (x) : = M$ on $D$ is integrable and bounds the derivative for every $t \in J$ , with no exceptional set. Thus [F4] applies to $D \times J$ , giving differentiability at $t_{0}$ and derivative $- \int_{D} div j (\cdot, t_{0})$ . By [F3] applied to the $C^{1}$ field $j (\cdot, t_{0})$ , this equals $- \int_{\partial D} j (\cdot, t_{0}) \cdot n d S$ . Since $t_{0}$ was arbitrary, (b) holds on the possibly disconnected open set $I$ .

3.1givenstep 2.1F5F7algebra

[Global conservation] Assume (c), and let $s, t \in I$ with $s < t$ and $[s, t] \subseteq I$ . For $R > 0$ with $K_{R} : = {x : ∣ x ∣ < R}$ we have by step 2.1 applied to $D = K_{R}$ (for $R$ so large that $\overline{K_{R}} \subseteq R^{3}$ , which always holds) $\frac{d}{d τ} \int_{K_{R}} ∣ ψ ∣^{2} = - \int_{\partial K_{R}} j \cdot n d S$ , so [F7] gives $∣ \int_{K_{R}} ∣ ψ (x, t) ∣^{2} d x - \int_{K_{R}} ∣ ψ (x, s) ∣^{2} d x ∣ \leq (t - s) \sup_{τ \in [s, t]} \int_{\partial K_{R}} ∣ j ∣ d S$ , and the right side tends to $0$ as $R \to \infty$ by the hypothesis on the flux. By [F5], $\int_{K_{R}} ∣ ψ (\cdot, τ) ∣^{2} \to ∥ ψ (\cdot, τ) ∥^{2}$ for $τ = t$ and $τ = s$ , using $∣ ψ ∣^{2} \leq g \in L^{1}$ . Letting $R \to \infty$ in the inequality gives $∣ ∥ ψ (\cdot, t) ∥^{2} - ∥ ψ (\cdot, s) ∥^{2} ∣ = 0$ . Thus the norms agree for every pair with the closed interval between them contained in $I$ , proving (c).

4.1givenF6algebra∎

[Unitary dynamics] By [F6], $ψ (t) = e^{- i t K / ℏ} ψ_{0}$ with $e^{- i t K / ℏ}$ unitary, so $∥ ψ (t) ∥ = ∥ ψ_{0} ∥$ for every $t$ . This is (d) and completes the proof.

Smooth local continuity equation and its integrated forms

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources