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.

Galilean boost covariance of the Schrodinger model with bounded potential

Statement

Assume the Axiom of Choice and the Axiom of Countable Choice (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )). Fix $ℏ > 0$ , $m > 0$ , a real bounded measurable $V : R^{3} \to R$ , and let $K : = \frac{1}{2 m} \sum_{j} P_{j}^{2} + M_{V}$ with domain $W^{2, 2} (R^{3}; C)$ be the free-plus-bounded-potential operator of Real multiplication operators and free plus bounded-potential Schrödinger operators clause (c); write $V_{u} (x, t) : = V (x - u t)$ for $u \in R^{3}$ . For $u \in R^{3}$ and $t \in R$ define the boost operator $(B_{u} (t) ψ) (x) : = e^{i (\frac{m}{ℏ} u \cdot x - \frac{m ∣ u ∣^{2}}{2 ℏ} t)} ψ (x - u t), ψ \in L^{2} (R^{3}; C) .$ Then:

(a) for every $t$ , $B_{u} (t)$ is unitary with $B_{u} (t)^{- 1} = B_{u} (t)^{*}$ , and $B_{u} (t)$ maps $W^{1, 2}$ and $W^{2, 2}$ onto themselves;

(b) for every $u_{0} \in W^{2, 2}$ and every $s \in R$ the curve $v (t) : = B_{u} (t) e^{- i (t - s) K / ℏ} B_{u} (s)^{- 1} u_{0}$ lies in $W^{2, 2}$ , is differentiable into $L^{2}$ on $R$ , and satisfies $v (s) = u_{0}$ and $i ℏ v^{'} (t) = (\frac{1}{2 m} \sum_{j} P_{j}^{2} + M_{V_{u} (\cdot, t)}) v (t) (t \in R),$ where $M_{V_{u} (\cdot, t)}$ is multiplication by $x \mapsto V (x - u t)$ . It is the unique such curve: if $w : R \to W^{2, 2}$ is continuous into $W^{2, 2}$ , differentiable into $L^{2}$ and satisfies the same equation with $w (s) = u_{0}$ , then $w = v$ ;

(c) the two-parameter family $U_{u} (t, s) : = B_{u} (t) e^{- i (t - s) K / ℏ} B_{u} (s)^{- 1}$ consists of unitaries preserving $W^{2, 2}$ , satisfies $U_{u} (t, t) = I$ , $U_{u} (t, r) U_{u} (r, s) = U_{u} (t, s)$ , and $v (t) = U_{u} (t, s) v_{0}$ is the solution of (b) at time $s$ for every $v_{0} \in W^{2, 2}$ ;

(d) free propagator covariance. With $K_{0} : = \frac{1}{2 m} \sum_{j} P_{j}^{2}$ (that is $V = 0$ ) one has $B_{u} (t) e^{- i (t - s) K_{0} / ℏ} = e^{- i (t - s) K_{0} / ℏ} B_{u} (s)$ for all $t, s$ .

All assertions concern the displayed unitary family and the Schrodinger-type equation; no Lorentz structure, no photon limit and no worldline of an unmeasured particle is asserted.

Facts & Assumptions

Given: $ℏ, m > 0$ , $u \in R^{3}$ , a real bounded measurable $V$ , the boost $B_{u} (t) = M_{e^{i φ (\cdot, t)}} T_{u t}$ with phase $φ (x, t) : = \frac{m}{ℏ} u \cdot x - \frac{m ∣ u ∣^{2}}{2 ℏ} t$ , translation $T_{a} f (x) = f (x - a)$ , the operator $K = \frac{1}{2 m} \sum_{j} P_{j}^{2} + M_{V}$ , and $A : = \frac{1}{2 m} \sum_{j} P_{j}^{2} + M_{V_{u} (\cdot, t)}$ .

[F1]

$M_{V}$ is bounded self-adjoint; $K$ is self-adjoint with $D (K) = W^{2, 2}$ , and $e^{- i t K / ℏ}$ is a strongly continuous unitary group with $e^{- i t K / ℏ} D (K) = D (K)$ , commuting with $K$ on $D (K)$ , and derivative $- \frac{i}{ℏ} K x$ exactly on $D (K)$ (Real multiplication operators and free plus bounded-potential Schrödinger operators clause (c), A self-adjoint operator generates a strongly continuous unitary group, Integral of a measurable function against a projection-valued measure).

[F2]

Translations and unimodular multiplications: $T_{a}$ is unitary and preserves $W^{1, 2}$ , $W^{2, 2}$ , with $D_{j} (T_{a} f) = T_{a} (D_{j} f)$ (Self-adjointness, Fourier representation and translation identities of position and momentum clause (c)); the phase family $M_{e^{i φ (\cdot, t)}}$ is unitary, preserves $W^{1, 2}$ and $W^{2, 2}$ , and has $t$ -derivative $i (\partial_{t} φ) M_{e^{i φ (\cdot, t)}} = - \frac{i m ∣ u ∣^{2}}{2 ℏ} M_{e^{i φ (\cdot, t)}}$ on $L^{2}$ (Gauge multiplication preserves H2 and transports the magnetic momentum applied with $(q, ℏ, χ) = (1, 1, φ)$ , whose hypotheses hold because $φ$ is affine in $x$ and $\partial_{t} φ = - \frac{m ∣ u ∣^{2}}{2 ℏ}$ ).

[F3]

For a smooth scalar $f : R^{3} \to C$ , define $\nabla f : = (\partial_{1} f, \partial_{2} f, \partial_{3} f)$ and $Δ f : = \sum_{j = 1}^{3} \partial_{j}^{2} f$ . The complex exponential addition law $\exp (z + w) = \exp z \exp w$ holds ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential). For fixed $t$ , put $α_{j} : = \partial_{j} φ = m u_{j} / ℏ$ ; the gauge-domain theorem F2, clause (b), gives the first derivative identity as an $L^{2}$ class, which is classical for smooth $ψ$ ; differentiating it with the product rule 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$ gives $\partial_{j} (e^{i φ} ψ) = e^{i φ} (\partial_{j} ψ + i α_{j} ψ)$ , and, since $α_{j}$ is constant in $x$ , $\partial_{j}^{2} (e^{i φ} ψ) = e^{i φ} (\partial_{j}^{2} ψ + 2 i α_{j} \partial_{j} ψ - α_{j}^{2} ψ)$ . Summing these coordinate identities yields the gradient and Laplacian formulas used below.

[F4]

Density extends the identities of [F3] to the Sobolev classes. First, for fixed $ψ \in W^{1, 2}$ the translation-difference-quotient identity $\frac{1}{h} (T_{u h} ψ - ψ) \to - u \cdot \nabla ψ$ in $L^{2}$ as $h \to 0$ : for smooth $ψ$ this is the classical chain rule, $\frac{1}{h} (T_{u h} ψ - ψ) (x) = - \frac{1}{h} \int_{0}^{h} (u \cdot \nabla ψ) (x - s u) d s$ , and the bound $∥ \frac{1}{h} (T_{u h} ν - ν) ∥ \leq ∥ u \cdot \nabla ν ∥$ for smooth $ν$ together with the density of $C_{c}^{\infty}$ in $W^{1, 2}$ extends the identity to all $ψ \in W^{1, 2}$ (the translation is isometric by [F2]). Second, for $ρ \in W^{1, 2}$ and $w : = B_{u} ρ$ , one has $B_{u} (\nabla ρ) = \nabla w - i \frac{m}{ℏ} u w$ as $L^{2}$ vector classes; and for $ρ \in W^{2, 2}$ also $B_{u} (Δ ρ) = Δ w - 2 i \frac{m}{ℏ} u \cdot \nabla w - \frac{m^{2} ∣ u ∣^{2}}{ℏ^{2}} w$ as multiplier classes. Both follow from the smooth case in [F3] by density of $C_{c}^{\infty}$ in $W^{1, 2}$ and $W^{2, 2}$ (Integer-order Sobolev spaces and their norms, Compactly supported smooth functions are dense in W^{k,p}(R^n)) and continuity of the maps involved in the relevant norms.

[F5]

$P_{j} = - i ℏ D_{j}$ on its domain, so $u \cdot P ψ = - i ℏ u \cdot \nabla ψ$ for $\nabla ψ \in L^{2}$ ; and $B_{u} (t)^{- 1} = T_{- u t} M_{e^{- i φ (\cdot, t)}}$ with the analogous derivative $i (\partial_{t} φ)$ term (Self-adjointness, Fourier representation and translation identities of position and momentum, Position and momentum operators on Euclidean L2, [F2]).

[F6]

A real function continuous on a closed interval and differentiable in its interior with zero derivative is constant, by 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)$ ; restrictions of a differentiable curve to compact intervals satisfy these continuity hypotheses.

Proof

1.1givenF2

[Unitarity and domain preservation] By [F2], $B_{u} (t)$ is a product of two unitary operators preserving $W^{1, 2}$ and $W^{2, 2}$ , hence unitary on $L^{2}$ and preserving both Sobolev spaces; its inverse is $T_{- u t} M_{e^{- i φ}}$ , so $B_{u} (t)^{- 1} = B_{u} (t)^{*}$ and (a) holds.

1.2givenF2F3F4algebra

[Derivative identities] Put $λ : = \frac{m ∣ u ∣^{2}}{2 ℏ}$ . Direct computation from the definition gives $B_{u} (t + h) = B_{u} (t) e^{- i λ h} T_{u h}$ , so for fixed $ψ \in W^{1, 2}$ the difference quotient is $\frac{1}{h} (B_{u} (t + h) ψ - B_{u} (t) ψ) = B_{u} (t) [e^{- i λ h} \frac{T_{u h} ψ - ψ}{h} + \frac{e^{- i λ h} - 1}{h} ψ]$ . The bracket tends to $- u \cdot \nabla ψ - i λ ψ$ in $L^{2}$ : the first term by the translation-difference-quotient identity of [F4] (classical chain rule [F3] extended by density), the second by [F2] instantiated at the affine phase $φ^{'} (x, t) : = - λ t$ , which gives $\frac{d}{d t} e^{- i λ t} = - \frac{i m ∣ u ∣^{2}}{2 ℏ} e^{- i λ t}$ . Hence $\frac{d}{d t} [B_{u} (t) ψ] = - i λ B_{u} (t) ψ - B_{u} (t) (u \cdot \nabla ψ)$ . By the transported-gradient identity of [F4], $B_{u} (t) (u \cdot \nabla ψ) = u \cdot \nabla (B_{u} (t) ψ) - 2 i λ B_{u} (t) ψ$ , so the identity also reads $\frac{d}{d t} [B_{u} (t) ψ] = i λ B_{u} (t) ψ - u \cdot \nabla (B_{u} (t) ψ)$ ; replacing $u$ by $- u$ , which gives $B_{- u} (t) = B_{u} (t)^{- 1}$ directly from the definition, yields $\frac{d}{d t} [B_{u} (t)^{- 1} η] = i λ B_{u} (t)^{- 1} η + u \cdot \nabla (B_{u} (t)^{- 1} η)$ for fixed $η \in W^{1, 2}$ .

1.3givenF2algebra

[Transported potential] $B_{u} (t) M_{V} B_{u} (t)^{- 1} = M_{V (\cdot - u t)}$ : indeed $T_{u t} M_{V} T_{- u t} = M_{V (\cdot - u t)}$ by the change of variables $y = x - u t$ , and conjugation by a unimodular multiplication fixes multiplication by a real function.

1.4givenF4algebra

[Transported Laplacian] Let $ρ \in W^{2, 2}$ and $w : = B_{u} (t) ρ$ . Applying [F4] twice, $B_{u} (\nabla ρ) = \nabla w - i \frac{m}{ℏ} u w$ and $B_{u} (Δ ρ) = Δ w - 2 i \frac{m}{ℏ} u \cdot \nabla w - \frac{m^{2} ∣ u ∣^{2}}{ℏ^{2}} w$ ; consequently $B_{u} (t) (- \frac{ℏ^{2}}{2 m} Δ ρ) = - \frac{ℏ^{2}}{2 m} Δ w + i ℏ u \cdot \nabla w + \frac{m ∣ u ∣^{2}}{2} w$ .

2.1givenstep 1.2step 1.3step 1.4F1F2F4F5algebra

[Forward equation and initial data] Let $u_{0} \in W^{2, 2}$ and $s \in R$ , put $w_{0} : = B_{u} (s)^{- 1} u_{0}$ , $w (t) : = e^{- i (t - s) K / ℏ} w_{0}$ and $v (t) : = B_{u} (t) w (t)$ . By [F1] the group preserves $D (K)$ , commutes with $K$ there and is strongly continuous both on $L^{2}$ and on $D (K)$ with graph norm: apply strong continuity to $w_{0}$ and $K w_{0}$ . That graph norm is equivalent to the $W^{2, 2}$ norm, since the free operator has this equivalence and the bounded perturbation satisfies $∥ K_{0} f ∥ \leq ∥ K f ∥ + ∥ V ∥_{\infty} ∥ f ∥$ and $∥ K f ∥ \leq ∥ K_{0} f ∥ + ∥ V ∥_{\infty} ∥ f ∥$ . Hence $w$ is continuous into $W^{2, 2}$ and differentiable into $L^{2}$ with $w^{'} = - i K w / ℏ$ . The boosts are strongly continuous on $W^{2, 2}$ : translations are isometries in each weak-derivative norm and are continuous by smooth density, while derivatives of the affine-phase multiplier are constant multiples of that multiplier; its time dependence is a scalar phase. They are locally uniformly bounded on $W^{2, 2}$ . Thus $v$ is continuous into $W^{2, 2}$ . For differentiability, decompose its quotient into $B_{u} (t + h) (w (t + h) - w (t)) / h + (B_{u} (t + h) - B_{u} (t)) w (t) / h$ ; strong continuity on $L^{2}$ , unitarity and step 1.2 give $v^{'} = B_{u} (t) w^{'} + i λ v - u \cdot \nabla v$ , where $λ = m ∣ u ∣^{2} / (2 ℏ)$ . By steps 1.3-1.4, $B_{u} (t) K w = - ℏ^{2} Δ v / (2 m) + i ℏ u \cdot \nabla v + m ∣ u ∣^{2} v / 2 + M_{V_{u} (\cdot, t)} v$ . Therefore $i ℏ v^{'} = - m ∣ u ∣^{2} v / 2 - i ℏ u \cdot \nabla v + B_{u} (t) K w = (- ℏ^{2} Δ / (2 m) + M_{V_{u} (\cdot, t)}) v$ ; both extra terms cancel. At the actual initial time, $v (s) = B_{u} (s) w_{0} = u_{0}$ , with no assumption that $s = 0$ . This proves existence and the initial condition in (b).

3.1givenstep 1.2step 1.3step 1.4step 2.1F1F5algebraF6

[Uniqueness with the transformed initial datum] Let $w$ be another solution in the stated class, and put $ρ (t) : = B_{u} (t)^{- 1} w (t)$ . The continuity argument of step 2.1 applies also to the inverse boost. For its $L^{2}$ derivative, decompose the difference quotient just as in step 2.1, using the inverse derivative from step 1.2; this gives $ρ^{'} = i λ ρ + u \cdot \nabla ρ + B_{u} (t)^{- 1} w^{'}$ . The inverse transported identities of steps 1.3-1.4 give $B_{u} (t)^{- 1} (- ℏ^{2} Δ / (2 m) + M_{V_{u} (\cdot, t)}) B_{u} (t) ρ = K ρ - i ℏ u \cdot \nabla ρ + m ∣ u ∣^{2} ρ / 2$ . Substituting the equation for $w$ cancels the scalar and first-order terms, so $i ℏ ρ^{'} = K ρ$ and $ρ (s) = B_{u} (s)^{- 1} u_{0}$ . Set $G (t) : = e^{i (t - s) K / ℏ}$ and $F (t) : = G (t) ρ (t)$ . The quotient decomposition $G (t + h) (ρ (t + h) - ρ (t)) / h + (G (t + h) - G (t)) ρ (t) / h$ converges in $L^{2}$ : the first term by strong continuity and unitarity, the second by [F1] on the fixed vector $ρ (t) \in D (K)$ . Hence $F^{'} = G (t) (ρ^{'} + i K ρ / ℏ) = 0$ . A differentiable Hilbert-space curve with zero derivative is constant, by applying the real scalar mean-value theorem to every bounded real linear functional. Thus $F (t) = F (s) = B_{u} (s)^{- 1} u_{0}$ , and $ρ (t) = e^{- i (t - s) K / ℏ} B_{u} (s)^{- 1} u_{0}$ . Multiplying by $B_{u} (t)$ proves $w (t) = B_{u} (t) e^{- i (t - s) K / ℏ} B_{u} (s)^{- 1} u_{0} = v (t)$ . This proves the uniqueness part of (b) with its actual initial datum.

4.1givenstep 2.1step 3.1F1algebra

[Propagator properties] Each $U_{u} (t, s)$ is unitary and preserves $W^{2, 2}$ by (a) and [F1]; $U_{u} (t, t) = B_{u} (t) B_{u} (t)^{- 1} = I$ ; and the composition law follows from $B_{u} (r)^{- 1} B_{u} (r) = I$ and the group law of $e^{- i τ K / ℏ}$ : $U_{u} (t, r) U_{u} (r, s) = B_{u} (t) e^{- i (t - r) K / ℏ} e^{- i (r - s) K / ℏ} B_{u} (s)^{- 1} = U_{u} (t, s)$ . By step 2.1, $t \mapsto U_{u} (t, s) v_{0}$ solves the moving-potential equation with initial value $v_{0}$ , and step 3.1 makes it unique. This is (c).

5.1step 3.1step 4.1F1F4algebra∎

[Free covariance] Let $V = 0$ , so $V_{u} = 0$ , $K = K_{0}$ and the equation of (b) is the free equation. By step 4.1 with $V = 0$ , the propagator for the free equation is $B_{u} (t) e^{- i (t - s) K_{0} / ℏ} B_{u} (s)^{- 1}$ , and it equals $e^{- i (t - s) K_{0} / ℏ}$ because the free equation has at most one $W^{2, 2}$ -valued solution for each initial datum (step 3.1 with $V = 0$ ). Multiplying the identity $B_{u} (t) e^{- i (t - s) K_{0} / ℏ} B_{u} (s)^{- 1} = e^{- i (t - s) K_{0} / ℏ}$ on the right by $B_{u} (s)$ gives (d). This equality first holds on $W^{2, 2}$ and extends to all $L^{2}$ because both sides are bounded unitaries and $C_{c}^{\infty} \subset W^{2, 2}$ is dense in $L^{2}$ by [F4].

Galilean boost covariance of the Schrodinger model with bounded potential

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources