TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

VQE Rayleigh–Ritz upper bound and equality case

Statement

For every ansatz parameter $θ$ , $E (θ) \geq E_{0}$ , with equality exactly when $∣ ψ (θ) ⟩$ lies in the ground eigenspace of $H$ . Thus a VQE evaluation gives an upper bound on the ground energy, but an ansatz family or classical optimizer need not reach $E_{0}$ .

Facts & Assumptions

Given: A finite-dimensional Hermitian $H$ and a normalized ansatz state.

[F1]

Variational eigenvalue objective: $E (θ) = ⟨ ψ ∣ H ∣ ψ ⟩_{D}$ and $E_{0} = \min σ (H)$ .

[F2]

Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely: $H$ has an orthonormal eigenbasis and real eigenvalues.

[F3]

Dirac Notation Conversion: the Dirac expectation is the root-convention matrix coefficient.

Proof

technique · direct

1.1givenF1F2F3algebra

Let $e_{j}$ be an orthonormal eigenbasis with eigenvalues $λ_{j} \geq E_{0}$ , and write $ψ = \sum_{j} c_{j} e_{j}$ . By [F1]–[F3], $E (θ) - E_{0} = \sum_{j} (λ_{j} - E_{0}) ∣ c_{j} ∣^{2} \geq 0.$ The coefficients have squared magnitudes summing to one.

2.1givenstep 1.1algebra∎

Every summand in step 1.1 is nonnegative. The sum is zero exactly when $c_{j} = 0$ for each $λ_{j} > E_{0}$ , which is exactly the condition that $ψ$ belongs to the eigenspace for $E_{0}$ , allowing any degeneracy there.

Depends on

Used by

A variational circuit family may miss the optimum Counterexample
VQE and MaxCut-QAOA objective calculation Example

Dependency tree · two levels

16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

https://arxiv.org/pdf/2012.09265v2 (standard reference, not scraped)