Circuit Syntax, Denotational Semantics, and Measurement

Since $h,k,e\ge 1$, the registers $A=Q_{ke}$ and $B=Q_h$ are nonzero. By [F1] and [F3], $\dim (H\otimes A)=hke=\dim (K\otimes E\otimes B)$.

Choose an orthonormal basis $(u_i{)}_{i<h}$ of $H$ using [F5]. By [F2], $(u_i\otimes a_0{)}_{i<h}$ is orthonormal in $H\otimes A$. The complex polarization identity for the first-linear inner-product convention, $⟨x,y⟩=\frac{1}{4}(\mathrm{\parallel }x+y{\mathrm{\parallel }}^2-\mathrm{\parallel }x-y{\mathrm{\parallel }}^2+i\mathrm{\parallel }x+iy{\mathrm{\parallel }}^2-i\mathrm{\parallel }x-iy{\mathrm{\parallel }}^2),$ and the linearity and norm preservation of $V$ from [F6] give $⟨V{u}_i,V{u}_j⟩=⟨u_i,u_j⟩={\delta }_{ij}$. Since $b_0$ has norm one by [F1], the product inner product [F2] makes $(V{u}_i\otimes b_0{)}_{i<h}$ orthonormal in $K\otimes E\otimes B$. The linear map sending $u_i\otimes a_0$ to $V{u}_i\otimes b_0$ is therefore an isometry between the two $h$-dimensional subspaces they span.

Let $S$ and $T$ be those two spans. By [F4], each ambient space is the orthogonal direct sum of its span and orthogonal complement. Choose orthonormal bases of $S^{\perp }$ and $T^{\perp }$ by [F5], of lengths $p$ and $q$. Concatenate each with the corresponding $h$-vector orthonormal list from step 1.2. Each concatenated list spans its ambient space by the direct-sum decomposition. It is linearly independent: a zero linear combination splits as $s+z=0$ with $s$ in the span and $z$ in its orthogonal complement, so directness gives $s=z=0$, and independence within each list makes every coefficient zero. Thus the concatenated lists are bases; by the definition of dimension, their lengths give $hke=h+p$ and $hke=h+q$ using step 1.1. Hence $p=q$, establishing equal complement dimensions and giving completed orthonormal bases of the full input and output spaces.

Map the completed input basis bijectively to the completed output basis, using the prescribed map on $(u_i\otimes a_0)$. Its linear extension is surjective and preserves inner products because it sends one orthonormal basis to another. It is the required $W$ by [F6]. Linearity gives $W(x\otimes a_0)=Vx\otimes b_0$ for all $x$. The argument uses only finite basis choices, not a choice axiom.

List the complement wires as $c_0<\cdots <c_{n-r-1}$. The rule $\mathrm{\mid }{x}_0,\dots ,x_{n-1}⟩\mapsto \mathrm{\mid }{x}_{w_0},\dots ,x_{w_{r-1}}⟩\otimes \mathrm{\mid }{x}_{c_0},\dots ,x_{c_{n-r-1}}⟩$ is a bijection from the computational basis of ${\mathcal{Q}}_n$ to the product basis of ${\mathcal{Q}}_r\otimes {\mathcal{Q}}_{n-r}$: the output lists each original coordinate once and records which coordinate occupies each position. Its linear extension $P_w$ sends one orthonormal basis bijectively to another, hence is unitary by [F2].

Put $T=U\otimes I_{{\mathcal{Q}}_{n-r}}$. By [F3]–[F5], $T^{†}T=(U^{†}U)\otimes I=I$ and $T{T}^{†}=(U{U}^{†})\otimes I=I$. Thus $T^{†}$ is a two-sided inverse, and [F6] gives $\mathrm{\parallel }Tz{\mathrm{\parallel }}^2=⟨Tz,Tz⟩=⟨z,T^{†}Tz⟩=\mathrm{\parallel }z{\mathrm{\parallel }}^2$ for every $z$. Hence $T$ is unitary. Since $P_w$ is a surjective isometry by step 1.1, its inverse also preserves norms: for $y=P_{w}x$, $\mathrm{\parallel }{P}_w^{-1}y\mathrm{\parallel }=\mathrm{\parallel }x\mathrm{\parallel }=\mathrm{\parallel }{P}_{w}x\mathrm{\parallel }=\mathrm{\parallel }y\mathrm{\parallel }$. Therefore the composite ${\tilde{U}}_w=P_w^{-1}(U\otimes I_{{\mathcal{Q}}_{n-r}})P_w$ is invertible and norm-preserving, hence unitary by [F5]. Its action, by the definition of $P_w$, applies $U$ to the selected factors in tuple order and leaves the complement factors fixed, as required.

The computational basis spans ${\mathcal{Q}}_n$. Any linear map with the specified action on its basis vectors is unique, so the embedding in step 2.1 is the unique one.

Fix a computational basis vector $\mathrm{\mid }x⟩$. For an ordered wire tuple $w$, write $x_w$ for its ordered bit subtuple and $x^{w\leftarrow u}$ for the full bitstring obtained by replacing those positions by $u$. By [F1], the embedding of the first gate with matrix coefficients $U_{u,x_S}$ acts as $\mathrm{\mid }x⟩\mapsto {\sum }_u{U}_{u,x_S}\mathrm{\mid }{x}^{S\leftarrow u}⟩\mathrm{.}$ Applying the second gate on the disjoint tuple $T$ gives ${\sum }_{u,v}{U}_{u,x_S}{V}_{v,x_T}\mathrm{\mid }{x}^{S\leftarrow u,T\leftarrow v}⟩\mathrm{.}$ In the reverse order the result is the same sum with scalar factors $V_{v,x_T}{U}_{u,x_S}$, which agree because complex scalars commute; the replacement bitstrings are identical because $S\cap T=\mathrm{\varnothing }$. Thus both composites agree on this basis vector.

The computation in step 1.1 holds for every computational basis vector, which spans ${\mathcal{Q}}_n$. Therefore the two global linear maps agree on a basis and are equal, so the embedded gates commute.

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

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.

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

Put $h=\dim H$. By [F2] and $H\mathrm{\ne }0$, $h\ge 1$; choose an ordered basis of length $h$. The coordinate columns of the identity map give the matrix $I_h$ by [F3], so ${\mathrm{tr}}_H(I_H)=\mathrm{tr}(I_h)=h>0$.

Suppose $\dim K=0$. Then [F2] gives $K=\{0\}$, so every output endomorphism ${\mathcal{I}}_a(I_H)$ is the zero operator and has trace $0$. Applying [F1] to $I_H$ would give $0={\mathrm{tr}}_H(I_H)$, contradicting step 1.1. Hence $\dim K>0$ and $K\mathrm{\ne }0$.

Put $S={\sum }_{a,j}{M}_{a,j}^{†}{M}_{a,j}\in \mathcal{L}(H)$. For every $X\in \mathcal{L}(H)$, [F1]–[F3] give ${\mathrm{tr}}_H(X)={\sum }_a{\mathrm{tr}}_K({\mathcal{I}}_a(X))={\sum }_{a,j}{\mathrm{tr}}_K(M_{a,j}X{M}_{a,j}^{†})={\sum }_{a,j}{\mathrm{tr}}_H(X{M}_{a,j}^{†}{M}_{a,j})={\mathrm{tr}}_H(XS)$.

Cyclicity in [F3] gives ${\mathrm{tr}}_H((S-I_H)X)={\mathrm{tr}}_H(X(S-I_H))=0$ for every $X$. Apply [F4] to $D=S-I_H$ to obtain $S-I_H=0$, which is the stated normalization. This proof uses the exact trace-pairing lemma The trace pairing on a finite endomorphism space is nondegenerate and does not use a channel characterization.

By [F12], $K$ is nonzero. For each $a\in \mathrm{\Omega }$, complete positivity in [F1] and [F2] supplies a finite Kraus family for ${\mathcal{I}}_a$ as in [F3]. Let $r$ be the maximum of their finitely many lengths and $1$; append zero operators to shorter lists until every list has length $r$. These finitely many choices are made successively over $\mathrm{\Omega }$, so no choice axiom is used.

Define $P_a{e}_b=e_b$ if $b=a$ and $0$ otherwise on $Q_m$, and put ${\mathrm{\Pi }}_a=P_a\otimes I_{Q_r}$. The basis definitions show $P_a$ is self-adjoint and idempotent, the $P_a$ are pairwise orthogonal and sum to $I_{Q_m}$, so [F7] makes them a projective measurement. By [F8], ${\mathrm{\Pi }}_a(e_b\otimes f_j)$ equals $e_b\otimes f_j$ if $b=a$ and $0$ otherwise; since these basis vectors are orthonormal and span $E$, ${\mathrm{\Pi }}_a$ is the orthogonal projection onto the subspace with observed label $a$.

The branch families in step 1.1 are the instrument's finite branch Kraus families, so [F4] gives ${\sum }_{a,j<r}{M}_{a,j}^{†}{M}_{a,j}=I_H$. Since $m,r\ge 1$, the registers in [F5] exist.

For $x,y\in H$, orthogonality of the product record basis [F6] and the adjoint identity [F10] give $⟨Vx,Vy⟩={\sum }_{a,j}⟨M_{a,j}x,M_{a,j}y⟩={\sum }_{a,j}⟨x,M_{a,j}^{†}{M}_{a,j}y⟩=⟨x,y⟩$ by step 2.1. Thus the finite sum defines a linear isometry.

The adjoint $V^{†}$ in the claimed operator identity exists by [F11]. Expanding the isometry gives $VX{V}^{†}={\sum }_{b,c\in \mathrm{\Omega }}{\sum }_{j,k<r}{M}_{b,j}X{M}_{c,k}^{†}\otimes \mathrm{\mid }{e}_b\otimes f_j⟩⟨e_c\otimes f_k\mathrm{\mid }\mathrm{.}$ Applying $I_K\otimes {\mathrm{\Pi }}_a$ on both sides kills terms unless $b=c=a$. The partial-trace formula [F9] then keeps only the diagonal hidden entries $j=k$, leaving ${\sum }_{j<r}{M}_{a,j}X{M}_{a,j}^{†}={\mathcal{I}}_a(X)$ by [F3]. The rank-one record operators have the action specified by [F13]. Thus only $a$ is recorded as the outcome; $j$ is traced out.

For each $a\in \mathrm{\Omega }$, [F1] makes ${\mathcal{I}}_a$ completely positive, so [F2] supplies a finite family $(M_{a,j}{)}_j$ representing it as in [F3]. If the supplied family is empty, append one zero operator; this preserves the formula and makes each index list nonempty. Since $\mathrm{\Omega }$ is finite, the lists can be selected one at a time by finite induction; no arbitrary-index choice is used.

Define $\mathrm{\Phi }={\sum }_{a\in \mathrm{\Omega }}{\mathcal{I}}_a$. Concatenating the finite lists in step 1.1 gives a Kraus representation of $\mathrm{\Phi }$. These are exactly the finite branch Kraus families of the instrument in [F1], so [F4] gives ${\sum }_{a,j}{M}_{a,j}^{†}{M}_{a,j}=I_H$.

For each outcome define $E_a={\sum }_j{M}_{a,j}^{†}{M}_{a,j}$. By [F5], each summand is self-adjoint and $⟨M_{a,j}^{†}{M}_{a,j}x,x⟩=⟨M_{a,j}x,M_{a,j}x⟩\ge 0$. Thus each $E_a$ is non-negative by [F6]. Step 2.1 gives ${\sum }_a{E}_a=I_H$, so $(E_a)$ is a finite POVM by [F7].

For every $X\in \mathcal{L}(H)$, the Kraus formula [F3], trace linearity, and rectangular cyclicity [F8] give ${\mathrm{tr}}_K({\mathcal{I}}_a(X))={\sum }_j{\mathrm{tr}}_K(M_{a,j}X{M}_{a,j}^{†})={\sum }_j{\mathrm{tr}}_H(X{M}_{a,j}^{†}{M}_{a,j})={\mathrm{tr}}_H(X{E}_a)$. This proves the displayed outcome-law identity for every density operator as well.

If another family $E_a^{\mathrm{\prime }}$ has the same identity for every $X$, then ${\mathrm{tr}}_H(X(E_a-E_a^{\mathrm{\prime }}))=0$ for all $X$. By [F8], this equals ${\mathrm{tr}}_H((E_a-E_a^{\mathrm{\prime }})X)$; [F9] implies $E_a-E_a^{\mathrm{\prime }}=0$. This holds for each $a$, so the induced POVM is unique.

Put $m=\mathrm{\mid }\mathrm{\Omega }\mathrm{\mid }\ge 1$ and write an arbitrary vector of $Q_m\otimes K$ uniquely as ${\sum }_{a\in \mathrm{\Omega }}{e}_a\otimes x_a$. The block formula sends it to ${\sum }_a{e}_a\otimes S_a{x}_a$; orthogonality of the $e_a$ makes distinct label blocks orthogonal.

By [F1]–[F3], the observed law is the instrument branch law, equals the induced POVM law, and the conditional state is assigned only on a positive-weight branch. The $\mathrm{\perp }$ convention applies on every zero-probability branch; the history tree records only its observed edge labels.

For vectors ${\sum }_a{e}_a\otimes x_a$ and ${\sum }_a{e}_a\otimes y_a$, the product inner product gives $⟨Bx,By⟩={\sum }_a⟨S_a{x}_a,S_a{y}_a⟩={\sum }_a⟨x_a,y_a⟩=⟨x,y⟩$. The block map with $S_a^{†}$ in each block is its two-sided inverse, so $B$ is a surjective isometry.

Step 2.1 establishes the mathematical block unitary. Its inclusion as a circuit operation still requires the explicit access or construction promised by the model, as required by [F5]; the definition grants no additional oracle or gate capability.

Flattening the layer lists gives a finite list containing each gate occurrence exactly once by the circuit syntax. Its length is ${\sum }_t\mathrm{\mid }{L}_t\mathrm{\mid }$, so the size definition counts exactly the occurrences in the circuit.

Reordering gates within a disjoint layer changes neither that layer's finite cardinality nor the sum of the layer cardinalities. Thus the declared size is unchanged by within-layer ordering; the separately declared depth remains the number of layers.

The access coordinates are assigned only to calls named by the operation model. By [F2]–[F3], controlled and inverse calls require their own explicit declarations, so no query or gate cost is inferred from a matrix description alone.

The branch output is the unnormalized operator ${\tau }_a={\mathcal{I}}_a(\rho )$, and its trace is the branch weight $p_a$, by [F1].

The weights form a finite probability law by [F2], and the same law is $\mathrm{tr}(\rho E_a)$ by [F3] and [F4]. This establishes consistency of the instrument and POVM descriptions.

If $p_a>0$, the conditional output is defined by division by that positive scalar; if $p_a=0$, [F1] assigns $\mathrm{\perp }$ and no division is made. The finite Kraus index remains internal to ${\mathcal{I}}_a$ and is not part of $\mathrm{\Omega }$.

Enumerate one layer as $L_t=(g_1,\dots ,g_s)$. By [F1] its denotation is ${\tilde{U}}_{g_s}\cdots {\tilde{U}}_{g_1}$, so [F4] gives its adjoint ${\tilde{U}}_{g_1}^{†}\cdots {\tilde{U}}_{g_s}^{†}$.

For each occurrence, its global embedding $T={\tilde{U}}_{g_j}$ is unitary by [F1]. The inverse $T^{-1}=T^{†}$ acts on each ordered product basis vector by applying $U_{g_j}^{-1}=U_{g_j}^{†}$ to the selected factors and leaving every complement factor fixed: applying $T$ to that result returns the original vector. The legal local-adjoint embedding has the same action, so uniqueness in [F5] identifies it with $T^{†}$. The assumed legal inverse occurrence and [F2] provide this call. There is one inverse occurrence per original gate, so the size is unchanged by [F3].

By [F1], the whole circuit is $U_{L_d}\cdots U_{L_1}$. Repeated use of [F4] yields $U_C^{†}=U_{L_1}^{†}\cdots U_{L_d}^{†}$, which acts by executing the inverse of $L_d$ first and the inverse of $L_1$ last. Since each layer is unitary, $U_C^{†}{U}_C=U_C{U}_C^{†}=I$, so $U_C^{†}=U_C^{-1}$ and it is the denotation of the reversed circuit.

If $d=0$, both circuits are empty and denote the identity; the occurrence count is zero on both sides by [F3].