DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge 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.

Dirac Notation Conversion

Definition

All complex inner products in this track use the root convention: they are linear in the first argument and conjugate-linear in the second (Real and complex inner-product spaces and their induced length). For vectors $x, y$ in the same space, define the Dirac pairing by

$⟨ x ∣ y ⟩_{D} : = ⟨ y, x ⟩_{r o o t} .$

The ket $∣ x ⟩$ denotes the vector $x$ . The bra $⟨ x ∣$ denotes the linear functional $z \mapsto ⟨ z, x ⟩_{r o o t}$ .

For finite-dimensional complex inner-product spaces $H, K$ , vectors $y \in H$ and $x \in K$ , define the rank-one linear map

$∣ x ⟩ ⟨ y ∣ : H \to K, z \mapsto ⟨ z, y ⟩_{H, r o o t} x .$

Given ordered orthonormal bases of $H$ and $K$ , its coordinate matrix is $[x] [y]^{†}$ , where $[x]$ and $[y]$ are the corresponding coordinate columns and $M^{†} : = {\overline{M}}^{T}$ is the conjugate transpose. The coordinate assertion is established in Dirac Notation Coordinate Identity ↗.

Depends on

Used by

Amplitude amplification with a fixed integer iteration count Algorithm
Amplitude amplification with independently chosen phase rotations Algorithm
Amplitude-estimation expectation estimator Algorithm
BBHT search when the marked count is unknown Algorithm
Bounded-error evaluation from a dual adversary certificate Algorithm
Complete-graph continuous-time search Algorithm
Controlled input-consistency reflection from a bit query Algorithm
Costed coherent evaluation of cyclic group powers Algorithm
Finite CKS sparse QLSP with variable-time inverse estimation Algorithm
Finite cyclic discrete logarithm by Fourier sampling Algorithm
Five-local history-state adiabatic path Algorithm
HHL finite sine-window phase-estimation algorithm Algorithm
Hypercube continuous-time state transfer Algorithm
Known-count Grover search by exact integer maximization Algorithm
LCU block encoding Algorithm
LCU block-encoding construction Algorithm
Modular order finding with rational reconstruction Algorithm
One finite abelian hidden-subgroup Fourier sample Algorithm
One Grover iterate in the standard bit-query model Algorithm
One-query Bernstein–Vazirani algorithm Algorithm
One-query Deutsch algorithm Algorithm
One-query Deutsch–Jozsa algorithm Algorithm
Product block encoding with separate ancillas Algorithm
QSVT implementation of a bounded matrix function Algorithm
QSVT regularized pseudoinverse transformation Algorithm
Quantum phase estimation Algorithm
Quantum phase-estimation spectral sampler Algorithm
Quantum singular-value transformation circuit Algorithm
Reversible binary dot-product query Algorithm
Reversible modular multiplication by a unit Algorithm
Szegedy-walk marked-set detection Algorithm
Unknown-amplitude randomized search Algorithm
Variance-aware quantum Monte Carlo Algorithm
A preserved unknown state cannot program its own reflection Counterexample
One uniform phase query gives small trace-distance advantage Counterexample
Parity violation makes singular-value action basis dependent Counterexample
Amplitude estimation and counting input/output contract Definition
Binary phase-query convention Definition
Block-encoded QLSP input and singular-gap promise Definition
Boolean oracle query model for search lower bounds Definition

…and 149 more results.

Dependency tree · two levels

17 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

John Watrous, The Theory of Quantum Information (2018 author-hosted draft), Chapters 1–2 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (2026-08-27), Appendices A.3 and A.10 (standard reference, not scraped)