DefinitionDefinition: Literature-sourcedProof: AI-adaptedPipeline-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.

Denotational semantics of a finite layered circuit

Definition

For a gate occurrence $g = (γ, w)$ in a circuit on $Q_{n}$ , let ${\tilde{U}}_{g}$ be the global embedding from A local gate has a unique global wire embedding. For a layer $L_{t} = (g_{1}, \dots, g_{s})$ , define $U_{L_{t}} : = {\tilde{U}}_{g_{s}} \dots {\tilde{U}}_{g_{1}} .$ For a circuit with chronological layers $L_{1}, \dots, L_{d}$ , define $U_{C} : = U_{L_{d}} \dots U_{L_{1}} .$ The empty circuit and every empty layer denote the identity on $Q_{n}$ .

Facts & Assumptions

Given: A finite layered circuit on the ordered register $Q_{n}$ .

[F1]

Finite circuit syntax and ordered wire labels: layers are finite ordered lists of gates with pairwise disjoint supports, and $L_{1}$ is applied first.

[F2]

A local gate has a unique global wire embedding: each gate occurrence has a unique unitary action on the full register.

[F3]

Gates on disjoint wires commute: the embeddings of gates in the same layer commute.

[F4]

Orthogonal and unitary operators form groups, and their determinants have modulus one: finite products and inverses of unitary operators are unitary.

Proof

1.1givenF2F4algebra

Every factor ${\tilde{U}}_{g_{j}}$ in a layer product is unitary by [F2]; the empty product is identity. The layer map $U_{L_{t}}$ is therefore unitary by [F4].

1.2givenF1F3algebra

Since every pair of gates in a layer has disjoint support, [F3] shows the factors commute pairwise. Any two enumerations of a finite list are related by finitely many adjacent swaps, so the layer product is independent of the enumeration.

2.1givenF1F4algebra∎

The chronological application of $L_{1}, \dots, L_{d}$ composes the last-applied map on the left, hence is $U_{L_{d}} \dots U_{L_{1}}$ . It is unitary as a finite product of unitary maps; when $d = 0$ this is the identity.

Depends on

Used by

Controlled T using a clean ancilla Algorithm
Costed coherent evaluation of cyclic group powers Algorithm
Dense-coding procedure Algorithm
Exact binary QFT circuit Algorithm
Exact single-qubit Clifford+T synthesis Algorithm
Finite higher-order Suzuki product formula Algorithm
First-order term-list simulator Algorithm
Gray-Path Synthesis of a Two-Level Gate Algorithm
LCU block-encoding construction Algorithm
One finite abelian hidden-subgroup Fourier sample Algorithm
Power-of-two dihedral hidden-subgroup sieve Algorithm
QC24 State Preparation Algorithm
Quantum phase estimation Algorithm
Quantum singular-value transformation circuit Algorithm
Qubit teleportation procedure Algorithm
Reversible embedding of a Boolean circuit Algorithm
Reversible modular multiplication by a unit Algorithm
Stabilizer encoder by symplectic elimination Algorithm
Truncated binary QFT Algorithm
Ancilla-free Rz approximation problem and T-count Definition
Circuit Optimization Task Definition
Circuit-family and computation cost model Definition
Coherent variable-time algorithm model Definition
Eigenphase estimation access model Definition
End-to-end channel and output error contract Definition
Fault-Tolerant Gadget and Proper-Code Contract Definition
Finite adaptive Pauli-measurement circuit tree Definition
Finite block encoding Definition
Finite open-graph adaptive measurement pattern Definition
Finite quantum promise-computation model Definition
Full-list uniform quantum circuit family Definition
Normalized output law for finite quantum query branches Definition
Normalized transport schedule for a J/CZ circuit Definition
Parameterized variational quantum objective Definition
QAOA circuit and expected combinatorial objective Definition
QC24 Clean Ancilla Output Projection Definition
QSP signal matrix and ordered phase sequence Definition
Quantum query algorithm Definition
SDP maximally entangled reference-state access Definition
Uniform verifier interface with a quantum witness Definition

…and 65 more results.

Dependency tree · two levels

29 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 Preskill, Quantum Computation, Chapter 5: Classical and Quantum Circuits (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)