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

Relative versus total bound state

Example

Assume the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The Axiom of Choice). Let $m_{1}, m_{2}, μ, M, κ, ℏ$ be as in Two-body reduced mass, let $C_{μ}$ and $T_{R}$ be the relative and centre-of-mass kinetic operators there, let $u_{1} \in L^{2} (R_{r}^{3})$ be any nonzero relative ground vector with $C_{μ} u_{1} = E_{1} u_{1}$ , where $E_{1} = - \frac{μ κ^{2}}{2 ℏ^{2}}$ , and let $φ \in C_{c}^{\infty} (R_{R}^{3}; C)$ be a nonzero centre-of-mass test function. Consider the product vector $Ψ : = φ \otimes u_{1} \in L^{2} (R_{R}^{3}) \hat{\otimes} L^{2} (R_{r}^{3}),$ viewed as an element of $L^{2} (R^{6})$ through the identification of Euclidean L² product unitary: L²(R^a)⊗̂L²(R^b) ≅ L²(R^{a+b}). This example verifies that:

(a) $(T_{R} \otimes I + I \otimes C_{μ}) Ψ = E_{1} Ψ + (T_{R} φ) \otimes u_{1}$ , and $T_{R} φ \neq 0$ , so $Ψ$ is not an eigenvector of the two-body operator;

(b) $⟨ (T_{R} \otimes I + I \otimes C_{μ}) Ψ, Ψ ⟩ = ∥ u_{1} ∥^{2} (E_{1} ∥ φ ∥^{2} + ⟨ T_{R} φ, φ ⟩) > E_{1} ∥ Ψ ∥^{2}$ : the product vector has energy strictly above the bottom $E_{1}$ of the two-body spectrum, and the bottom is not attained. When $∥ u_{1} ∥ = 1$ , the identity reduces to $E_{1} ∥ φ ∥^{2} + ⟨ T_{R} φ, φ ⟩$ ;

(c) the relative bound state $u_{1}$ is an eigenvector of the relative operator $C_{μ}$ , but the two-body operator has no eigenvalues at all (Two-body reduced mass (d)); the relative bound energy is a threshold of the continuous spectrum of the total operator, so "relative bound state" and "bound state of the two-body problem" are distinct notions.

Verification

Given: the constants and operators $T_{R}, C_{μ}, M, μ, κ, ℏ$ ; the relative ground state $u_{1}$ ; the test function $φ$ ; the product vector $Ψ$ .

Proof technique: direct computation with the tensor decomposition and the positivity of $T_{R}$ .

[F1] $C_{μ} u_{1} = E_{1} u_{1}$ with $E_{1} = - \frac{μ κ^{2}}{2 ℏ^{2}}$ and $0 < ∥ u_{1} ∥ < \infty$ , and $C_{μ} \geq E_{1}$ on its form domain (Laguerre bound energy exhaustion, Transported radial endpoint realization).

[F2] Tensor identities: $(A \otimes I) (u \otimes φ) = (A u) \otimes φ$ and $(I \otimes B) (u \otimes φ) = u \otimes (B φ)$ on the appropriate domains, and $⟨ u \otimes φ, u^{'} \otimes φ^{'} ⟩ = ⟨ u, u^{'} ⟩ ⟨ φ, φ^{'} ⟩$ (Euclidean L² product unitary: L²(R^a)⊗̂L²(R^b) ≅ L²(R^{a+b}), Hilbert space).

[F3] $T_{R} \geq 0$ , $T_{R} φ \neq 0$ for every nonzero $φ \in C_{c}^{\infty} (R_{R}^{3})$ : if $T_{R} φ = 0$ , then the Fourier transform satisfies $\frac{4 π^{2} ℏ^{2}}{2 M} ∣ ξ ∣^{2} \hat{φ} (ξ) = 0$ a.e., hence $\hat{φ} = 0$ a.e. off $∣ ξ ∣ = 0$ , and since ${0}$ is null, $φ = 0$ (Real multiplication operators and free plus bounded-potential Schrödinger operators, Plancherel theorem, Distributional derivatives are polynomial Fourier multipliers).

[F4] Cauchy-Schwarz and sesquilinearity of the inner product for the displayed computations (Cauchy-Schwarz inequality for $L^{2}$ , The space $L^{p} (μ)$ as the quotient by null functions, Complex Lp classes and Euclidean test-function conventions).

1.1F1F2F3algebra

[The product vector is not an eigenvector] By [F2], $(T_{R} \otimes I) Ψ = (T_{R} φ) \otimes u_{1}$ and $(I \otimes C_{μ}) Ψ = φ \otimes (C_{μ} u_{1}) = φ \otimes E_{1} u_{1} = E_{1} Ψ$ by [F1]; hence $(T_{R} \otimes I + I \otimes C_{μ}) Ψ = E_{1} Ψ + (T_{R} φ) \otimes u_{1}$ , and the difference from $E_{1} Ψ$ is $(T_{R} φ) \otimes u_{1}$ . By [F3] $T_{R} φ \neq 0$ and $u_{1} \neq 0$ , so this difference is nonzero: $Ψ$ is not an eigenvector at $E_{1}$ . The full no-eigenvalue result Two-body reduced mass (d) also rules out every other energy, so $Ψ$ is not an eigenvector at any energy. This is (a).

2.1step 1.1F1F2F3F4algebra

[Energy strictly above the threshold] Taking pairings with $Ψ$ and using [F2] and [F1], $⟨ (T_{R} \otimes I + I \otimes C_{μ}) Ψ, Ψ ⟩ = ∥ u_{1} ∥^{2} ⟨ T_{R} φ, φ ⟩ + ∥ u_{1} ∥^{2} E_{1} ∥ φ ∥^{2} = ∥ u_{1} ∥^{2} (E_{1} ∥ φ ∥^{2} + ⟨ T_{R} φ, φ ⟩)$ , and $⟨ T_{R} φ, φ ⟩ = \frac{4 π^{2} ℏ^{2}}{2 M} \int ∣ ξ ∣^{2} ∣ \hat{φ} (ξ) ∣^{2} d ξ > 0$ by [F3] applied to the nonzero function $φ$ (the integrand is nonnegative and not a.e. zero). Hence the energy of $Ψ$ is strictly larger than $E_{1} ∥ Ψ ∥^{2}$ , and since $∥ Ψ ∥^{2} = ∥ φ ∥^{2} ∥ u_{1} ∥^{2}$ , $Ψ / ∥ Ψ ∥$ is a unit vector with energy $E_{1} + ⟨ T_{R} φ, φ ⟩ / ∥ φ ∥^{2} > E_{1}$ , this vector lies strictly above the bottom $E_{1}$ of the spectrum; by the no-eigenvalue theorem of Two-body reduced mass (d) no nonzero vector at all attains $E_{1}$ . This is (b).

3.1step 2.1F1algebra

[Relative eigenvalue versus total spectrum] The relative vector $u_{1}$ is an eigenvector of $C_{μ}$ at $E_{1}$ by [F1]; but by the actual no-eigenvalue theorem of Two-body reduced mass (d), no nonzero vector at all satisfies the two-body eigenvalue equation, and $E_{1}$ is the bottom of the continuous spectrum of the total operator. This is (c).

4.1step 1.1step 2.1step 3.1∎

[Conclusion] Parts (a), (b), (c) are steps 1.1, 2.1 and 3.1.

Remarks

If $u_{1}$ is twice a unit ground vector, the unnormalized product energy is four times the unit-ground-vector expression. The factor $∥ u_{1} ∥^{2}$ retains all nonzero relative ground vectors and cancels in the normalized product energy.

Relative versus total bound state

Example

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources