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.

Conditional Stern-Gerlach force for a spin-coupled bounded field model

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$ , $γ_{s} \in R$ and a real function $B_{z} \in C^{1} (R)$ with $B_{z}$ and $B_{z}^{'}$ bounded. Let $H : = L^{2} (R^{3}; C) \oplus L^{2} (R^{3}; C), ⟨ (u_{+}, u_{-}), (v_{+}, v_{-}) ⟩ : = ⟨ u_{+}, v_{+} ⟩ + ⟨ u_{-}, v_{-} ⟩,$ let $P_{j}, Q_{j}$ act componentwise (Position and momentum operators on Euclidean L2, Self-adjointness, Fourier representation and translation identities of position and momentum), write $B_{z} (Q_{x})$ for componentwise multiplication by $x \mapsto B_{z} (x_{1})$ and $S_{z} (u_{+}, u_{-}) : = (\frac{ℏ}{2} u_{+}, - \frac{ℏ}{2} u_{-}), K (u_{+}, u_{-}) : = (\frac{1}{2 m} \sum_{j} P_{j}^{2} u_{+} - \frac{γ_{s} ℏ}{2} B_{z} (Q_{x}) u_{+}, \frac{1}{2 m} \sum_{j} P_{j}^{2} u_{-} + \frac{γ_{s} ℏ}{2} B_{z} (Q_{x}) u_{-}),$ with $D (K) : = {(u_{+}, u_{-}) : u_{+}, u_{-} \in W^{2, 2} (R^{3}; C)}$ , so that formally $K = \frac{1}{2 m} \sum_{j} P_{j}^{2} - γ_{s} S_{z} B_{z} (Q_{x})$ . Identify the spin factor with $V_{1 / 2} = C^{2}$ of Finite spin matrices by the basis $(e_{1 / 2}, e_{- 1 / 2})$ , so that on that factor $S_{z} = ℏ J_{z}$ with $J_{z} e_{m} = m e_{m}$ and eigenvalues $\pm ℏ / 2$ . Then:

(a) $K$ is self-adjoint with domain $D (K)$ , and $S_{z} K = K S_{z}$ on $D (K)$ ; consequently, for $u (t) : = e^{- i t K / ℏ} u_{0}$ and the sector projections $p_{\pm} : = \frac{1}{2} (I \pm \frac{2}{ℏ} S_{z})$ , $∥ p_{\pm} u (t) ∥^{2} = ∥ p_{\pm} u_{0} ∥^{2}, ⟨ S_{z} u (t), u (t) ⟩ = ⟨ S_{z} u_{0}, u_{0} ⟩ (t \in R, u_{0} \in H);$

(b) for every $u_{0} \in D (K^{2}) : = {u \in D (K) : K u \in D (K)}$ the function $t \mapsto ⟨ P_{x} u (t), u (t) ⟩$ is $C^{1}$ and $\frac{d}{d t} ⟨ P_{x} u (t), u (t) ⟩ = γ_{s} ⟨ S_{z} B_{z}^{'} (Q_{x}) u (t), u (t) ⟩,$ where $B_{z}^{'} (Q_{x})$ is componentwise multiplication by $x \mapsto B_{z}^{'} (x_{1})$ and $S_{z} B_{z}^{'} (Q_{x}) (u_{+}, u_{-}) = (\frac{ℏ}{2} B_{z}^{'} (Q_{x}) u_{+}, - \frac{ℏ}{2} B_{z}^{'} (Q_{x}) u_{-})$ ;

(c) if in addition $∥ u_{0} ∥ = 1$ , $p_{+} u_{0} = u_{0}$ , and $B_{z}^{'} (s) = G$ for every $s$ in a Borel set $N \subseteq R$ with $\int_{R ∖ N} η_{+} (x_{1}) d x_{1} = 0$ , where $η_{+} (x_{1}) : = \int_{R^{2}} ∣ u_{0}^{+} (x_{1}, x_{2}, x_{3}) ∣^{2} d x_{2} d x_{3}$ is the first-coordinate marginal density, then $\frac{d}{d t} ∣_{t = 0} ⟨ P_{x} u (t), u (t) ⟩ = \frac{γ_{s} ℏ}{2} G,$ an identity at the preparation time $t = 0$ ; for $t \neq 0$ the general formula of (b) applies and may differ;

(d) for the model field $B (x) : = (0, 0, B_{z} (x_{1}))$ one has $div B = 0$ and $curl B = (0, - B_{z}^{'} (x_{1}), 0)$ at every point.

The statements are conditional identities for the displayed model; no apparatus, measured trajectory, source-free Maxwell realisation of $B$ or inference about an individual particle is asserted.

Facts & Assumptions

Given: $ℏ, m > 0$ , $γ_{s} \in R$ , bounded $B_{z} \in C^{1} (R)$ with bounded $B_{z}^{'}$ ; the direct-sum Hilbert space $H$ ; the operators $S_{z}$ , $B_{z} (Q_{x})$ , $K$ on $H$ ; the componentwise operators $P_{j}, Q_{j}$ .

[F1]

On each component, $K_{\pm} : = \frac{1}{2 m} \sum_{j} P_{j}^{2} \mp \frac{γ_{s} ℏ}{2} M_{B_{z}}$ is self-adjoint with domain $W^{2, 2} (R^{3}; C)$ : this is Real multiplication operators and free plus bounded-potential Schrödinger operators clause (c) with the real bounded potential $\mp \frac{γ_{s} ℏ}{2} B_{z}$ ; $M_{B_{z}}$ is bounded self-adjoint (Real multiplication operators and free plus bounded-potential Schrödinger operators clause (a)).

[F2]

A direct sum $T = T_{+} \oplus T_{-}$ of self-adjoint operators is self-adjoint on $D (T_{+}) \oplus D (T_{-})$ : symmetry is componentwise, and surjectivity of $T \pm i$ follows from surjectivity of the components (Symmetric, self-adjoint and essentially self-adjoint operators).

[F3]

$T_{u (t), u (t)}$ denotes the rank-one operator $x \mapsto ⟨ x, u (t) ⟩ u (t)$ ; the PVM of the bounded self-adjoint $S_{z}$ is $F ({ℏ / 2}) = p_{+}$ , $F ({- ℏ / 2}) = p_{-}$ , $F (R ∖ {\pm ℏ / 2}) = 0$ , and $F (S) U (t) = U (t) F (S)$ whenever $S_{z} K \subseteq K S_{z}$ , by Conserved spectral probability laws for commuting observables and stationary eigenrays clauses (a') and (b)(iii). Also $p_{\pm} = \frac{1}{2} (I \pm \frac{2}{ℏ} S_{z})$ .

[F4]

Graph-domain Ehrenfest identities and the conditional timescale bound clause (a), one-sided form: if $ψ : I \to H$ is $C^{1}$ into $D (A)$ with the graph norm, $ψ^{'} (t) = - \frac{i}{ℏ} K ψ (t)$ and $K ψ (t) \in D (A)$ for all $t$ , then $t \mapsto ⟨ A ψ (t), ψ (t) ⟩$ is $C^{1}$ with derivative $- \frac{2}{ℏ} Im ⟨ A ψ (t), K ψ (t) ⟩$ .

[F5]

Plancherel and Fourier calculus: $F_{2}$ is unitary and $∥ g ∥_{2} = ∥ F_{2} g ∥_{2}$ (Plancherel theorem, Fourier transform on complex L1 classes). For $w \in W^{2, 2} (R^{3}; C)$ the class is bounded with $∣ w (x) ∣ \leq C ∥ w ∥_{W^{2, 2}}$ for a.e. $x$ , because $∣ w (x) ∣ = ∣ \int F_{2} w (ξ) e^{2 π i x \cdot ξ} d ξ ∣ \leq ∥ ⟨ ξ ⟩^{2} F_{2} w ∥_{2} ∥ ⟨ ξ ⟩^{- 2} ∥_{2}$ and $\int (1 + ∣ ξ ∣^{2})^{- 2} d ξ < \infty$ in three dimensions.

[F6]

Products of bounded Sobolev classes: for $w \in W^{2, 2} (R^{3}; C) \subseteq W^{1, 2} \cap L^{\infty}$ and its conjugate $\overline{w} \in W^{1, 2} \cap L^{\infty}$ , the product $∣ w ∣^{2} = w \overline{w}$ lies in $W^{1, 2}$ with $D_{j} ∣ w ∣^{2} = (D_{j} w) \overline{w} + w D_{j} \overline{w} = 2 Re ((D_{j} w) \overline{w})$ (Weak product rule for bounded Sobolev functions).

[F7]

Compactly supported integration by parts: if $u \in W^{1, 2} (R^{3})$ is compactly supported and $v \in W^{1, 2} (R^{3})$ , then $\int u D_{j} v = - \int v D_{j} u$ (Integration by parts for dual-exponent Sobolev functions, case $p = p^{'} = 2$ ). More generally a smooth compactly supported multiplier times a bounded Lipschitz function lies in $W^{1, 2}$ with the Leibniz derivative (Weak Leibniz rule with a smooth factor).

[F8]

Cutoffs and dominated convergence: the functions $χ_{R} (x) = χ (x / R)$ of Explicit compactly supported smooth cutoffs satisfy $0 \leq χ_{R} \leq 1$ , $χ_{R} = 1$ on $[- R, R]^{3}$ , $χ_{R} = 0$ outside $[- 2 R, 2 R]^{3}$ and $∣ D_{j} χ_{R} ∣ \leq C / R$ ; $L^{1}$ dominated convergence applies to integrals against $∣ w ∣^{2}$ and $∣ \partial_{j} ∣ w ∣^{2} ∣$ (Dominated convergence).

[F9]

For self-adjoint $K$ , the spectral unitary group preserves $D (K)$ , commutes with $K$ there and has derivative $- i K / ℏ$ for initial vectors in $D (K)$ . Tonelli on the sigma-finite product $R \times R^{2}$ defines the nonnegative marginal $η_{+}$ and gives $\int η_{+} = ∥ u_{0}^{+} ∥_{2}^{2}$ (A self-adjoint operator generates a strongly continuous unitary group, Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

Proof

1.1givenF1F2

[Self-adjointness and commutation] By [F1] each $K_{\pm}$ is self-adjoint on $W^{2, 2}$ , so [F2] makes $K = K_{+} \oplus K_{-}$ self-adjoint on $D (K) = W^{2, 2} \oplus W^{2, 2}$ . Also $S_{z}$ is bounded self-adjoint with eigenvalues $\pm ℏ / 2$ by the identification with $ℏ J_{z}$ of Finite spin matrices, and for $(u_{+}, u_{-}) \in D (K)$ , $S_{z} K (u_{+}, u_{-}) = (\frac{ℏ}{2} K_{+} u_{+}, - \frac{ℏ}{2} K_{-} u_{-}) = K S_{z} (u_{+}, u_{-})$ componentwise.

1.2givenF5

[The free part is real] For $w \in W^{2, 2} (R^{3}; C)$ put $K_{0} : = \frac{1}{2 m} \sum_{j} P_{j}^{2}$ and $c : = \frac{(2 π ℏ)^{2}}{2 m}$ . By [F5] and the multiplier identity of Self-adjointness, Fourier representation and translation identities of position and momentum, $⟨ P_{x} w, K_{0} w ⟩ = \int_{R^{3}} 2 π ℏ ξ_{1} c ∣ ξ ∣^{2} ∣ F_{2} w (ξ) ∣^{2} d ξ$ , an absolutely convergent integral of a real-valued function, hence a real number (Cauchy–Schwarz bounds it by $∥ P_{x} w ∥_{2} ∥ K_{0} w ∥_{2}$ ; no parity of $∣ F_{2} w ∣^{2}$ is assumed); so $Im ⟨ P_{x} w, K_{0} w ⟩ = 0$ .

1.3givenF6F7F8algebra

[The potential part] Let $w \in W^{2, 2}$ and let $χ_{R}$ be as in [F8]. By [F6], $∣ w ∣^{2} \in W^{1, 2}$ with $D_{x} ∣ w ∣^{2} = 2 Re ((D_{x} w) \overline{w})$ , and by [F7] the compactly supported class $χ_{R} B_{z} (x_{1}) \in W^{1, 2}$ satisfies $\int χ_{R} B_{z} D_{x} ∣ w ∣^{2} = - \int D_{x} (χ_{R} B_{z}) ∣ w ∣^{2} = - \int χ_{R} B_{z}^{'} ∣ w ∣^{2} - \int (D_{x} χ_{R}) B_{z} ∣ w ∣^{2}$ . Letting $R \to \infty$ , [F8] gives $\int B_{z} D_{x} ∣ w ∣^{2} = - \int B_{z}^{'} ∣ w ∣^{2}$ and $∣ \int (D_{x} χ_{R}) B_{z} ∣ w ∣^{2} ∣ \leq C ∥ B_{z} ∥_{\infty} R^{- 1} \int_{∣ x ∣ \geq R} ∣ w ∣^{2} \to 0$ . Since $Im ⟨ P_{x} w, M_{B_{z}} w ⟩ = Im \int (- i ℏ D_{x} w) B_{z} \overline{w} = - ℏ Re \int B_{z} D_{x} w \overline{w} = - \frac{ℏ}{2} \int B_{z} D_{x} ∣ w ∣^{2}$ , this gives $Im ⟨ P_{x} w, M_{B_{z}} w ⟩ = \frac{ℏ}{2} \int B_{z}^{'} ∣ w ∣^{2}$ .

2.1givenstep 1.1F3

[Conserved spin law] By step 1.1 the inclusion $S_{z} K \subseteq K S_{z}$ holds, so [F3] gives $S_{z} U (t) = U (t) S_{z}$ and hence $p_{\pm} U (t) = U (t) p_{\pm}$ because $p_{\pm}$ are polynomials in $S_{z}$ . For $u_{0} \in H$ , $∥ p_{\pm} u (t) ∥ = ∥ U (t) p_{\pm} u_{0} ∥ = ∥ p_{\pm} u_{0} ∥$ , and the mean identity follows from $⟨ S_{z} u, u ⟩ = \frac{ℏ}{2} (∥ p_{+} u ∥^{2} - ∥ p_{-} u ∥^{2})$ applied at times $t$ and $0$ . This is (a).

2.2givenstep 1.1F1F4F5F9algebra

[Graph differentiability for the full stated domain] For $w \in W^{2, 2}$ , the Fourier inequality $ξ_{1}^{2} \leq 1 + ∣ ξ ∣^{4}$ and Plancherel [F5] give $∥ P_{x} w ∥ \leq C (∥ K_{0} w ∥ + ∥ w ∥)$ . Since $K_{\pm} = K_{0} + V_{\pm}$ with bounded $V_{\pm}$ , it follows componentwise that $∥ P_{x} u ∥ \leq C^{'} (∥ K u ∥ + ∥ u ∥)$ on $D (K)$ , so $P_{x}$ is continuous from the $K$ graph norm into $H$ . If $u_{0} \in D (K^{2})$ , [F9] applied both to $u_{0}$ and to $K u_{0} \in D (K)$ makes $u (t) = U (t) u_{0}$ and $K u (t) = U (t) K u_{0}$ continuously differentiable in $H$ , with derivatives $- i K u (t) / ℏ$ and $- i K^{2} u (t) / ℏ$ . Thus $u (t)$ is $C^{1}$ in the $K$ graph norm, and applying the graph-continuous map $P_{x}$ yields $\frac{d}{d t} P_{x} u (t) = - i P_{x} K u (t) / ℏ$ . The domain inclusions $u (t), K u (t) \in D (K) \subseteq D (P_{x})$ therefore meet [F4], which gives $f (t) = ⟨ P_{x} u (t), u (t) ⟩ \in C^{1}$ and $f^{'} (t) = - 2 Im ⟨ P_{x} u (t), K u (t) ⟩ / ℏ$ without weakening $D (K^{2})$ .

3.1givenstep 2.2step 1.2step 1.3algebra

[Assembling the force] Write $u = (u_{+}, u_{-})$ , $K_{\pm} = K_{0} \mp \frac{γ_{s} ℏ}{2} M_{B_{z}}$ and $z (t) = \sum_{\pm} ⟨ P_{x} u_{\pm}, K_{\pm} u_{\pm} ⟩$ . By steps 1.2 and 1.3, $Im z (t) = \sum_{\pm} (\mp \frac{γ_{s} ℏ}{2}) \frac{ℏ}{2} \int B_{z}^{'} ∣ u_{\pm} ∣^{2} = - \frac{γ_{s} ℏ^{2}}{4} \int B_{z}^{'} ∣ u_{+} ∣^{2} + \frac{γ_{s} ℏ^{2}}{4} \int B_{z}^{'} ∣ u_{-} ∣^{2} = - \frac{γ_{s} ℏ}{2} ⟨ S_{z} B_{z}^{'} (Q_{x}) u, u ⟩$ , because $⟨ S_{z} B_{z}^{'} (Q_{x}) u, u ⟩ = \frac{ℏ}{2} \int B_{z}^{'} ∣ u_{+} ∣^{2} - \frac{ℏ}{2} \int B_{z}^{'} ∣ u_{-} ∣^{2}$ . Substituting into step 2.2, $f^{'} = - \frac{2}{ℏ} Im z = γ_{s} ⟨ S_{z} B_{z}^{'} (Q_{x}) u (t), u (t) ⟩$ , which is (b).

4.1givenstep 3.1F9algebra

[Constant-gradient preparation in three dimensions] Under (c), $u_{0} = (u_{0}^{+}, 0)$ and the marginal $η_{+} (x_{1})$ of [F9] satisfies $\int η_{+} = ∥ u_{0} ∥^{2} = 1$ and vanishes in integral off $N$ . Tonelli and boundedness of $B_{z}^{'}$ give $⟨ S_{z} B_{z}^{'} (Q_{x}) u_{0}, u_{0} ⟩ = \frac{ℏ}{2} \int_{R} B_{z}^{'} (x_{1}) η_{+} (x_{1}) d x_{1} = \frac{ℏ}{2} G \int_{N} η_{+} = \frac{ℏ}{2} G$ . By step 3.1 at preparation time $t = 0$ , $f^{'} (0) = γ_{s} ℏ G / 2$ . The general force formula retains the later-time dependence of the marginal and field gradient.

5.1givenalgebra∎

[Field identities] For $B (x) = (0, 0, B_{z} (x_{1}))$ : $div B = D_{1} B_{1} + D_{2} B_{2} + D_{3} B_{3} = 0$ because $B_{1} = B_{2} = 0$ and $B_{3}$ is independent of $x_{3}$ ; and $curl B = (D_{2} B_{3} - D_{3} B_{2}, D_{3} B_{1} - D_{1} B_{3}, D_{1} B_{2} - D_{2} B_{1}) = (0, - B_{z}^{'} (x_{1}), 0)$ (Divergence and curl are linear and satisfy the scalar product rules). This is (d).

Conditional Stern-Gerlach force for a spin-coupled bounded field model

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources