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.

Variational ground gap overlap

Statement

Assume the Axiom of Choice and the Axiom of Countable Choice (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a self-adjoint operator on a nonzero complex Hilbert space $H$ (Symmetric, self-adjoint and essentially self-adjoint operators, Hilbert space) which is bounded below, let $E_{0} : = \inf σ (H) \in R$ , let $E$ be the projection-valued measure of $H$ (Spectral theorem for unbounded self-adjoint operators (PVM form), Projection valued measure), put $P : = E ({E_{0}})$ , and assume that $g > 0$ is a spectral gap: $σ (H) \cap (E_{0}, E_{0} + g) = \emptyset .$ For $u \in D (∣ H ∣^{1 / 2})$ write $E_{u} (B) : = ⟨ E (B) u, u ⟩$ for Borel sets $B \subseteq R$ (Scalar and complex measures from a pvm) and put $q_{H} [u] : = \int_{R} λ d E_{u} (λ)$ ; by Density operators and scalar spectral probability (c) this integral exists for $u \in D (∣ H ∣^{1 / 2})$ , and for $u \in D (H)$ it equals $⟨ H u, u ⟩$ . Then for every $u \in D (∣ H ∣^{1 / 2})$ with $∥ u ∥ = 1$ :

(a) $q_{H} [u] - E_{0} = \int_{R} (λ - E_{0}) d E_{u} (λ) \geq g ∥ (I - P) u ∥^{2}$ ;

(b) if $q_{H} [u] \leq E_{0} + ε$ for some $ε \geq 0$ , then $∥ (I - P) u ∥^{2} \leq ε / g$ ; in particular, if $ε < g$ then $P u \neq 0$ .

No claim is made about the existence of a ground eigenvector, about $E_{0}$ being an eigenvalue, or about any physical interpretation of the trial vector.

Facts & Assumptions

Given: the self-adjoint operator $H$ bounded below with bottom $E_{0} = \inf σ (H)$ , its projection-valued measure $E$ , the ground projection $P = E ({E_{0}})$ , a gap $g > 0$ , and a vector $u \in D (∣ H ∣^{1 / 2})$ with $∥ u ∥ = 1$ .

[F1]

For a self-adjoint $H$ and unit $u \in D (∣ H ∣^{1 / 2})$ , the scalar measure $E_{u} (B) = ⟨ E (B) u, u ⟩$ is a probability measure and $\int ∣ λ ∣ d E_{u} < \infty$ , so its signed first moment $\int λ d E_{u}$ is finite; if $u \in D (H)$ , that moment equals $⟨ H u, u ⟩$ (Density operators and scalar spectral probability (c), Scalar and complex measures from a pvm, Spectral theorem for unbounded self-adjoint operators (PVM form)). No square-root expectation of $H$ is asserted when $H$ may have negative spectrum.

[F2]

$E ({E_{0}}) = P$ is an orthogonal projection; for every Borel set $B$ , $E_{u} (B) = ∥ E (B) u ∥^{2}$ , and $E (B) = 0$ implies $E_{u} (B) = 0$ (Projection valued measure).

[F3]

$E_{0} = \inf σ (H)$ means $σ (H) \subseteq [E_{0}, \infty)$ , so $E ((- \infty, E_{0})) = 0$ ; the gap hypothesis means $E ((E_{0}, E_{0} + g)) = 0$ (Spectral theorem for unbounded self-adjoint operators (PVM form), Projection valued measure, Symmetric, self-adjoint and essentially self-adjoint operators).

Proof

1.1F1F2F3algebra

[Support of the scalar measure] By [F2] and [F3], $E_{u} ((- \infty, E_{0})) = ∥ E ((- \infty, E_{0})) u ∥^{2} = 0$ and $E_{u} ((E_{0}, E_{0} + g)) = ∥ E ((E_{0}, E_{0} + g)) u ∥^{2} = 0$ ; hence $E_{u}$ is concentrated on ${E_{0}} \cup [E_{0} + g, \infty)$ and, since $E_{u}$ is a probability measure ([F1]), $E_{u} (R) = ∥ u ∥^{2} = 1$ , $E_{u} ({E_{0}}) = ∥ P u ∥^{2}$ and $E_{u} ([E_{0} + g, \infty)) = ∥ (I - P) u ∥^{2}$ .

2.1F1step 1.1algebra

[The first-moment inequality] Write $(λ - E_{0})^{+} : = (λ - E_{0}) 1_{[E_{0}, \infty)} (λ)$ , a nonnegative Borel function equal to $λ - E_{0}$ on the support of $E_{u}$ by step 1.1. Since $\int ∣ λ ∣ d E_{u} < \infty$ by [F1] and $E_{u} (R) = 1$ , $\int (λ - E_{0}) d E_{u} = \int λ d E_{u} - E_{0} = q_{H} [u] - E_{0}$ . On the support, $(λ - E_{0})^{+} \geq g 1_{[E_{0} + g, \infty)} (λ)$ , so $q_{H} [u] - E_{0} \geq g E_{u} ([E_{0} + g, \infty)) = g ∥ (I - P) u ∥^{2}$ , which is (a); if in addition $q_{H} [u] \leq E_{0} + ε$ , then $g ∥ (I - P) u ∥^{2} \leq ε$ .

3.1step 2.1algebra∎

[Failure of the ground component] If $ε < g$ , then $∥ (I - P) u ∥^{2} \leq ε / g < 1 = ∥ u ∥^{2}$ , so $∥ P u ∥^{2} = ∥ u ∥^{2} - ∥ (I - P) u ∥^{2} > 0$ and $P u \neq 0$ ; this completes the proof of (b) and of the statement.

Variational ground gap overlap

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources