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.

Parameter-shift derivative for a Pauli generator

Statement

Suppose one parameter occurs in exactly one gate $U_{j} (θ) = e^{- i θ P / 2}$ with $P = P^{*}$ and $P^{2} = I$ , while all other circuit factors, the input state, and the Hermitian observable are independent of $θ$ . Then for each linear expectation term $C (θ)$ , $\partial_{θ} C (θ) = \frac{1}{2} (C (θ + π / 2) - C (θ - π / 2)) .$ The identity is exact. Finite-shot estimates of the two shifted terms have separate sampling and measurement costs.

Facts & Assumptions

Given: $P^{2} = I$ , finite-dimensional unitary factors, a fixed density operator, and a Hermitian observable.

[F1]

Denotational semantics of a finite layered circuit: circuit composition denotes the corresponding finite product of operators.

[F2]

Dirac Notation Conversion: Dirac expectations agree with the root-space matrix coefficient convention.

[F3]

Finite Hermitian matrix dynamics and The spectral functional calculus f(T) for a normal endomorphism define $e^{- i t P}$ by the finite spectral functional calculus.

[F4]

Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely diagonalizes Hermitian $P$ ; since $P^{2} = I$ , each eigenvalue is $+ 1$ or $- 1$ .

[F5]

Euler's formula: $\exp (i θ) = \cos θ + i \sin θ$ for every real $θ$ : $\exp (i x) = \cos x + i \sin x$ for real $x$ .

[F6]

Parity and the Pythagorean identity for sine and cosine: cosine is even and sine is odd.

[F7]

The addition formulas for sine and cosine gives the double-angle identities.

[F8]

The derivatives of sine and cosine are cosine and minus sine gives $(\sin x)^{'} = \cos x$ and $(\cos x)^{'} = - \sin x$ .

[F9]

Quarter-turn values and shifts by pi/2 and pi gives the shifts by $\pm π / 2$ used in the centered difference.

Proof

technique · direct

1.1givenF1F2F3F4F5F6F7algebra

By [F3]–[F4], write the spectral projections of $P$ as $Π_{+}, Π_{-}$ (either may be zero), so $e^{- i θ P / 2} = \exp (- i θ / 2) Π_{+} + \exp (i θ / 2) Π_{-}$ . Euler's formula [F5] and parity [F6] give $e^{- i θ P / 2} = \cos (θ / 2) I - i \sin (θ / 2) P$ . Absorb all other fixed circuit factors into fixed vectors/operators and expand the expectation bilinearly. Products of the two trigonometric factors reduce by [F7] to $C (θ) = a + b \cos θ + c \sin θ$ for constants independent of $θ$ .

2.1givenF8F9step 1.1algebra∎

By [F8], differentiation gives $C^{'} (θ) = - b \sin θ + c \cos θ$ . The shift formulas [F9] give $C (θ + π / 2) - C (θ - π / 2) = 2 (- b \sin θ + c \cos θ)$ , proving the formula. For a finite sum of such expectation terms, differentiation and the shifted difference both distribute linearly.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 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)