Pipeline-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.

Circuit Syntax, Denotational Semantics, and Measurement — Examples

1 · Prerequisites

2 · Summary

This example compares a one-bit classical feed-forward circuit with its coherent deferred-measurement version. It computes each branch and the final joint distribution in the declared ordered basis, using explicit gate matrices and an explicitly granted controlled block.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

One-bit feed-forward and deferred measurement

Statement

Start two qubits in $∣ 00 ⟩$ , apply $H$ to the first, measure the first qubit in the computational basis, and apply $X$ to the second qubit if and only if the observed bit is $1$ . The final joint computational-basis law is $\Pr (00) = \Pr (11) = 1 / 2$ , with the other two outcomes having probability $0$ . Replacing the intermediate measurement and classical control by the explicitly granted block gate $C (X)$ and measuring both qubits at the end gives the same law.

Facts & Assumptions

Given: The ordered two-qubit register with initial vector $∣ 00 ⟩$ . The operation model for this example explicitly grants $H$ and $X$ as ordinary one-qubit gate calls and $C (X)$ as a separate control-first two-qubit gate call. Set $H = \frac{1}{\sqrt{2}} (\begin{array}{cc} 1 & 1 \\ 1 & - 1 \end{array}), X = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array}), C (X) = (\begin{array}{cc} I_{2} & 0 \\ 0 & X \end{array}) .$ Direct multiplication gives $H^{†} H = H H^{†} = I_{2}$ and $X^{†} X = X X^{†} = I_{2}$ . Hence $C (X)^{†} C (X) = C (X) C (X)^{†} = diag (I_{2}, I_{2}) = I_{4}$ , so all three displayed operations are unitary gate data.

[F1]

Controlled Unitary Access: a controlled operation is the control-first block matrix $C (U) = diag (I, U)$ when that access is explicitly granted.

[F2]

Finite projective measurements: a projective measurement is a finite family of self-adjoint idempotents, pairwise orthogonal, whose sum is identity.

[F3]

Projective measurement outcome weights are probabilities: for a density operator $ρ$ and projectors $(P_{a})$ , the outcome weights are $tr (ρ P_{a})$ .

[F4]

Conditional state for a projective measurement: when $p_{a} > 0$ , the conditional density is $P_{a} ρ P_{a} / p_{a}$ .

[F5]

Pure state and ray and Dirac Notation Conversion: a unit vector $u$ represents the ray with projector $P_{u} = ∣ u ⟩ ⟨ u ∣$ , acting by $z \mapsto ⟨ z, u ⟩_{r o o t} u$ .

[F6]

Ray-to-projector is well-defined and bijective: $P_{u}$ is non-negative with trace one, hence is a density operator by Density operator.

[F7]

Denotational semantics of a finite layered circuit: a chronological gate list is interpreted by its ordered product on the stated register.

[F8]

Finite registers and their ordered computational bases and Ordered tensor registers, their inner product, and wire permutations: the ordered two-qubit basis is $∣ 00 ⟩, ∣ 01 ⟩, ∣ 10 ⟩, ∣ 11 ⟩$ .

Example

Let $P_{0} = diag (1, 1, 0, 0)$ and $P_{1} = diag (0, 0, 1, 1)$ in that ordered basis. The measured circuit uses this projective measurement and the classical rule $a \mapsto X^{a}$ on the target. The coherent replacement uses the explicitly declared $C (X)$ from Given. The finite operation model grants $H$ and $X$ as ordinary calls and $C (X)$ as a separate block-gate call; no controlled access is inferred from the matrix $X$ alone.

Proof

1.1givenF2F8algebra

Direct multiplication gives $P_{0}^{*} = P_{0} = P_{0}^{2}$ , $P_{1}^{*} = P_{1} = P_{1}^{2}$ , $P_{0} P_{1} = P_{1} P_{0} = 0$ , and $P_{0} + P_{1} = I_{4}$ . Thus $(P_{0}, P_{1})$ is a projective measurement by [F2].

1.2givenF5F6F7F8algebra

By the matrix $H$ in Given and the circuit semantics [F7], applying $H$ to the first qubit sends the initial vector to $u = (∣ 00 ⟩ + ∣ 10 ⟩) / \sqrt{2}$ . The basis in [F8] is orthonormal, so $∥ u ∥ = 1$ ; [F5]–[F6] therefore give the input density $ρ = ∣ u ⟩ ⟨ u ∣$ .

2.1step 1.1step 1.2F3F8algebra

The matrix of $ρ$ in [F8] has diagonal $(1 / 2, 0, 1 / 2, 0)$ and nonzero off-diagonal entries only in positions $(00, 10)$ and $(10, 00)$ , each $1 / 2$ . Multiplication by the diagonal projectors gives $tr (ρ P_{0}) = 1 / 2$ and $tr (ρ P_{1}) = 1 / 2$ ; the outcomes have these probabilities by [F3].

2.2step 1.2F3F5F6F8algebra

The explicitly granted block matrix in Given sends $∣ 00 ⟩$ to $∣ 00 ⟩$ and $∣ 10 ⟩$ to $∣ 11 ⟩$ . It therefore sends the premeasurement vector $u$ from step 1.2 to $u^{'} = (∣ 00 ⟩ + ∣ 11 ⟩) / \sqrt{2}$ . The ordered basis in [F8] makes $u^{'}$ a unit vector, so [F5]–[F6] give the density operator $∣ u^{'} ⟩ ⟨ u^{'} ∣$ . Applying the diagonal projectors gives terminal weights $1 / 2$ on $00, 11$ and zero on $01, 10$ by [F3]. Thus the coherent circuit has the same joint law.

3.1step 1.1step 1.2step 2.1F4algebra

By [F4], the normalized conditional states are $P_{0} ρ P_{0} / (1 / 2) = ∣ 00 ⟩ ⟨ 00 ∣$ and $P_{1} ρ P_{1} / (1 / 2) = ∣ 10 ⟩ ⟨ 10 ∣$ . On the outcome- $0$ branch the target is unchanged; on the outcome- $1$ branch the matrix $X$ in Given sends $∣ 10 ⟩$ to $∣ 11 ⟩$ . The measured-and-controlled circuit therefore has the joint law stated.

4.1step 3.1step 2.2F1construct∎

The displayed branches are the one-instrument, one-bit case of the coherent equivalence in [thm-qc-deferred-measurement]. The measurement label stays the first wire and the target update depends on that label.