ExampleConstruction: Literature-sourcedVerification: 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.

One-gate history Hamiltonian energy check

Example

Take one work qubit in $∣ 0 ⟩$ , one gate $U_{1} = H$ , and declare outcome $∣ 1 ⟩$ accepting. Then the history is $∣ η ⟩ = \frac{1}{\sqrt{2}} (∣ 0 ⟩ ∣ c_{0} ⟩ + ∣ + ⟩ ∣ c_{1} ⟩), ∣ + ⟩ = (∣ 0 ⟩ + ∣ 1 ⟩) / \sqrt{2} .$ Verify that propagation energy is zero and that the scaled output penalty has energy $1 / 2$ , equal to the verifier's rejection probability.

Facts & Assumptions

Given: The $T = 1$ history Hamiltonian and the stated one-qubit circuit.

[F1]

Feynman–Kitaev history Hamiltonian: at $T = 1$ , propagation is the half-weight edge penalty and output penalty coefficient is $T + 1 = 2$ .

[F2]

Propagation kernel and path-Laplacian gap: the edge penalty vanishes exactly when the second computation component is $U_{1}$ applied to the first.

[F3]

Input and output penalties on history states: the scaled output penalty equals the terminal rejection probability.

Proof

1.1F1F2givenalgebra

The propagation quadratic form on an arbitrary vector $∣ u ⟩ ∣ c_{0} ⟩ + ∣ v ⟩ ∣ c_{1} ⟩$ is $\frac{1}{2} ∥ v - H u ∥^{2}$ . Here $v = H ∣ 0 ⟩ = ∣ + ⟩$ , so the norm is zero and propagation energy vanishes.

2.1F1F3step 1.1algebra∎

The terminal state is $∣ + ⟩$ , whose probability of rejecting the accept-on- $∣ 1 ⟩$ predicate is $∣ ⟨ 0 ∣ + ⟩ ∣^{2} = 1 / 2$ . Directly, the clock- $c_{1}$ history component has squared norm $1 / 2$ , its reject projection has probability $1 / 2$ within that component, and the coefficient 2 cancels the clock factor $1 / 2$ ; the total output energy is $1 / 2$ . This matches [F3].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

Dorit Aharonov and Tomer Naveh, Quantum NP: A Survey (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes (standard reference, not scraped)