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.

No full discrete eigenbasis

Example

Assume the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The Axiom of Choice). Let $γ > 0$ , let $C = - Δ - γ / ∣ \cdot ∣$ on $H^{2} (R^{3}; C)$ be as above, and fix $g \in C_{c}^{\infty} ((0, \infty); C)$ with $\int_{0}^{\infty} φ_{0} (1, r) g (r) d r = 1,$ where $φ_{0} (1, \cdot)$ is the regular solution of Coulomb Jost Volterra solution at $k = 1$ , $l = 0$ . Such a $g$ exists because $φ_{0} (1, \cdot)$ is nonzero and locally square-integrable. Put $ψ (x) : = \frac{g (r)}{r} Y_{00} (Ω) (x = r Ω) .$ This example verifies concretely that:

(a) $ψ \in L^{2} (R^{3}; C)$ and the coefficients of $ψ$ in the polar decomposition of Angular radial unitary reduction vanish except in the $(0, 0)$ -block, where they equal $g$ ;

(b) $⟨ E_{C} ((0, \infty)) ψ, ψ ⟩ = \int_{0}^{\infty} ρ_{0} (E) ∣ \int_{0}^{\infty} φ_{0} (\sqrt{E}, r) g (r) d r ∣^{2} d E > 0$ ;

(c) consequently the closed span of the bound states $(ψ_{n l m})$ of Negative-subspace completeness and degeneracy is a proper subspace of $L^{2} (R^{3}; C)$ : the bound states alone are not a complete eigenbasis, and the nonnegative continuous spectral projection is indispensable.

Verification

Given: $γ > 0$ , the source $g$ with the displayed normalization, the function $ψ$ , and the operators $C, A_{0}$ with their spectral measures.

Proof technique: explicit computation with the unitary polar decomposition and the spectral density; positivity of a continuous nonzero integrand.

[F1] The polar unitary $U$ of Angular radial unitary reduction maps the block function $r^{- 1} g (r) Y_{00} (Ω)$ to the vector with $(0, 0)$ -entry $g$ and all other entries $0$ , and $∥ r^{- 1} g Y_{00} ∥_{2} = ∥ g ∥_{2}$ ; $C_{c}^{\infty} ((0, \infty)) \subseteq L^{2} (0, \infty)$ is dense and $φ_{0} (1, \cdot) \neq 0$ (Coulomb Jost Volterra solution, The space $L^{p} (μ)$ as the quotient by null functions, Complex Lp classes and Euclidean test-function conventions).

[F2] Spectral density of $A_{0}$ for compactly supported sources: for every $0 < a < b$ , $⟨ E_{A_{0}} ((a, b)) g, g ⟩ = \int_{a}^{b} ρ_{0} (E) ∣ \int_{0}^{\infty} φ_{0} (\sqrt{E}, r) g (r) d r ∣^{2} d E$ with $ρ_{0} (E) > 0$ ; the identity of measures extends to all Borel sets in $(0, \infty)$ (Coulomb continuum spectral density).

[F3] The block identity $U C U^{*} = ⨁_{(l, m)} A_{l}$ ; the negative spectral subspace of $C$ is the closed span of the bound states, which is $U^{- 1}$ of the corresponding direct sum of negative eigenspaces of the $A_{l}$ (Transported radial endpoint realization, Negative-subspace completeness and degeneracy, Coulomb essential spectrum).

[F4] Complex conjugation and continuity: $E \mapsto \int_{0}^{\infty} φ_{0} (\sqrt{E}, r) g (r) d r$ is continuous on $(0, \infty)$ (it is a pairing against a smooth family of solutions, Coulomb Jost Volterra solution, Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point), and Cauchy-Schwarz bounds the expression (Cauchy-Schwarz inequality for $L^{2}$ , Hilbert space).

1.1F1givenalgebra

[The vector and its coefficients] Since $g$ is compactly supported in $(0, \infty)$ and $Y_{00}$ is bounded, $ψ$ is a finite-block element in $L^{2}$ ; by [F1] its polar transform is supported in the $(0, 0)$ -block with entry $g$ , so $∥ ψ ∥_{2} = ∥ g ∥_{2} < \infty$ and $ψ \neq 0$ . This is (a).

2.1step 1.1F2F3F4algebra

[Positive continuous-spectrum component] The function $h (E) : = \int_{0}^{\infty} φ_{0} (\sqrt{E}, r) g (r) d r$ is continuous by [F4] and satisfies $h (1) = 1$ by the choice of $g$ ; hence there is $δ > 0$ with $∣ h (E) ∣ \geq 1 / 2$ on $(1 - δ, 1 + δ)$ . By [F2] and the block identity [F3], $⟨ E_{C} ((0, \infty)) ψ, ψ ⟩ = ⟨ E_{A_{0}} ((0, \infty)) g, g ⟩ = \int_{0}^{\infty} ρ_{0} (E) ∣ h (E) ∣^{2} d E \geq \int_{1 - δ}^{1 + δ} ρ_{0} (E) ∣ h (E) ∣^{2} d E \geq \frac{1}{4} \int_{1 - δ}^{1 + δ} ρ_{0} (E) d E > 0$ , because $ρ_{0} > 0$ and the interval has positive length. This is (b).

3.1step 2.1F3algebra

[The bound states do not span $L^{2}$ ] The negative spectral subspace $E_{C} ((- \infty, 0)) L^{2}$ is exactly the closed span of the bound states by [F3]; since $(0, \infty)$ and $(- \infty, 0)$ are disjoint Borel sets, the spectral projections are orthogonal, so the component $E_{C} ((0, \infty)) ψ \neq 0$ of step 2.1 is orthogonal to the whole negative spectral subspace. Hence $ψ$ is not in the closed span of the bound states, which is therefore a proper subspace of $L^{2} (R^{3}; C)$ . This is (c).

No full discrete eigenbasis

Example

Verification

Depends on

Dependency tree · 2 levels

Sources