Distance-Three exRec Correctness and Truncated Witness Reduction

Choose a complete stabilizer syndrome decoder $U:H_P\to H_L\otimes H_S$, using the stipulated Pauli recovery representative for each syndrome. The stabilizer eigenspaces are mutually orthogonal copies of the code, so this map is unitary. Write $\mathcal{U}={\mathrm{Ad}}_U$ and $D={\mathrm{Tr}}_S\mathcal{U}$. Recursively, $U_j$ first applies $U_{j-1}$ to each subblock and then $U$ to the resulting logical coordinates, retaining every syndrome register. Thus $H_{P,j}=H_L\otimes H_{S,j}$ after applying $U_j$. A weight-filter sector becomes $H_L\otimes S_0$ or $H_L\otimes S_1$, where $S_s$ is the span of syndrome basis vectors of errors of weight at most $s$. For a degenerate code, errors with the same syndrome give the same copy of the logical space, so this assertion remains true. All tensor products below include the external reference unchanged.

Here are the actual circuit boundaries used below. An ordinary gadget core is its recursive replacement circuit, before adjoining leading ECs of its opening child roots. Give every child slot its schedule address and every shared EC one physical address. To expand an exRec, adjoin those opening leading EC cores, then their opening leading EC cores at the next lower scale, and continue downwards. An added leading $j$-EC is the output $j$-EC of the previous $j$-rectangle on precisely that wire; it does not include the previous gate. Thus after a later bad root claims its expanded support, its earlier neighbors lose only output ECs at the outer scale and at successively lower scales. Each affected lower rectangle still has the full input and output registers of its own gate. Its missing EC wires are connected directly from the last retained operation to the first operation owned by the later root. Register identity along that connection does not assert equality of their states after any recovery. This is a boundary in the actual retained directed circuit, not a factor of a remotely placed final decoder. Gates on other wires may lie between its endpoints in a linear schedule; none lies on that wire between these endpoints, by the definition of the preceding rectangle.

At scale one let $s_i$ count faults in the leading ECs, $f$ those in the gate, and $t_a$ those in the output ECs which are present. If their total is at most one, the leading ECs put the input in ${⨂}_i{P}_{s_i}$. The gate takes this entire sector into $P_{s+f}$ on each output, where $s={\sum }_i{s}_i$, and has decoded logical action $g$. Every present output EC preserves that action because $s+f+t_a\le 1$. If an output EC is absent, the decoded gate identity already gives precisely the same conclusion on that output; no EC is inserted. This proves, simultaneously for every subset $J$ of output ECs retained, $D_{\mathrm{o}\mathrm{u}\mathrm{t}}{E}_J{G}_f{\mathrm{\mid }}_{{⨂}_i{P}_{s_i}}=g{D}_{\mathrm{i}\mathrm{n}}{\mathrm{\mid }}_{{⨂}_i{P}_{s_i}}$. The corresponding preparation and destructive-measurement identities are exactly those in [A1]. This establishes the base assertion for complete and truncated rectangles together.

First remove transparent classical bypasses from the EC ownership graph. A retained logical classical record on which $D$ acts as identity cannot have a last incident location inside an elementary EC: replacing that location by its ideal operation followed by resetting that outgoing bit to zero is an allowed one-location CPTP fault. No later EC location could restore it. On an encoded quantum input with that logical bit equal to one, this would violate $D{E}_1{P}_0=D{P}_0$, including its classical port. The same argument excludes a newly prepared retained logical bit. Thus these external record wires pass untouched through the EC; route their fan-out directly from their original incoming source, outside the EC owner. Recursive refinement preserves these bypasses because it replaces locations, and there is no EC location on such a wire to replace. Records obtained by decoding an encoded block instead belong to that block bundle until its declared measurement. Now contract ordinary recursively replaced cores. By the port discipline this recovers the parent circuit DAG, with the transparent wires bypassed: all internal ancillas close within their invocation, and every remaining external quantum or classical wire is a parent edge. Moving a shared EC from an earlier rectangle to a following selected bad exRec transfers an output-terminal subcircuit forward along that edge. No output of the moved piece returns to a retained operation of the earlier owner. To check the last assertion at nested boundaries, take the first lower EC core adjoined across the boundary: it is the trailing EC immediately before the first opening child in the already transferred piece. A retained gate on that wire between it and that child would contradict their being consecutive. Any other non-bypass output of that EC is an internal ancilla, closed within the same EC, or another output in that same block bundle. Repeat at smaller scales. Thus every collar piece transferred forward is terminal on all its non-bypass external output wires in the retained earlier owner. All such outputs of the transferred EC feed the claiming successor: syndrome-processing records are internal, transparent classical fan-out has already been bypassed, and the quantum output is precisely that successor's input bundle. Thus each new quotient edge into the successor replaces an old forward path through the preceding owner and that EC; there is no new outgoing edge to a third owner. Such a transfer cannot create a quotient cycle, since replacing every new edge by its old forward path would give a cycle in the previous DAG. Repeating these finite transfers, in the prescribed reverse root order and descending collar scale, gives disjoint owners and a causal quotient DAG. The owner's interface can be staggered in elementary time; at a stagger use its complete child block bundles, descending until each bundle is exposed. Every primitive multi-register operation belongs to one owner and is never split. This also proves that the quotient's root labels and the addresses erased at its boundaries are exactly those in the stated scan.

We will retain the syndromes in that identity. If a CPTP map $M$ on $H_L\otimes K$ has logical marginal $g{\mathrm{Tr}}_K$ for every input, its conjugation by $g^{-1}$ has identity logical marginal. Its Choi matrix has marginal supported on the one-dimensional maximally entangled logical subspace. Positivity forces the entire Choi matrix to have support in that subspace tensored with the remaining registers; hence it factors as the identity-channel Choi matrix times the Choi matrix of a CPTP map on $K$. Consequently $M={\mathrm{Ad}}_g\otimes T$. Apply this to the entire filter sector in step 2.1, which by step 1.1 is the full logical space tensored with an allowed syndrome subspace. It gives an exact syndrome-retaining identity on that sector, including all input correlations. Extend $T$ to the remaining syndrome space by first projecting onto this sector and its orthogonal complement and using any fixed channel on the complement. Only the restriction is used on reachable states. For a prescribed pure preparation, its pure logical marginal forces its joint logical/syndrome output to be that state tensored with a syndrome state; this follows by the same positivity-support argument. For a good destructive measurement there is no syndrome output: its full quantum-to-classical channel on the admitted sector is exactly the ideal measurement following ${\mathrm{Tr}}_S$, with all other-block syndromes included in the unchanged external reference. Retain its classical output as a logical wire. No tensor-factor theorem for a general instrument is being assumed.

Fix the elementary pattern. Its replacement maps are fixed local CPTP maps by [F1]; they have no unlisted persistent memory port. Contract each actual physical owner in the DAG of step 2.2, before introducing any syndrome coordinates. It is a channel $B$ on its declared block bundles and classical ports; other live blocks are references. Now change coordinates at its actual input and output bundles: $\widehat{B}={\mathcal{U}}_{\mathrm{o}\mathrm{u}\mathrm{t}}B{\mathcal{U}}_{\mathrm{i}\mathrm{n}}^{-1}$, so ${\mathcal{U}}_{\mathrm{o}\mathrm{u}\mathrm{t}}B=\widehat{B}{\mathcal{U}}_{\mathrm{i}\mathrm{n}}$ exactly. Insert ${\mathcal{U}}^{-1}\mathcal{U}$ on each internal block edge of that DAG; the adjacent pairs cancel. At a staggered interface use the lower bundles of step 2.2 and keep the upper decoder on their logical outputs. No decoder crosses an intervening retained gate. In this construction a syndrome register is the coordinate of its particular physical block edge, not a new global bath: a multi-block operation can process syndromes only on its declared block ports, and a destructive measurement has no outgoing quantum or syndrome port. Thus the coordinate change introduces no extra cross-owner memory edge or cycle. In particular, for a bad owner $\widehat{B}$ is the conjugation of the ORIGINAL retained physical channel, with its original incoming syndromes. Its logical support is only its declared blocks and classical ports, and its elementary support has not enlarged. Neither a physical ideal recovery nor the false identity $U_j{\mathcal{E}}_j=U_j$ has been inserted.

To compare this exact network to the scan, distinguish a restored address from its original physical address: the former is a virtual ideal copy at the same template slot; the original, if claimed by a later bad owner, stays with that owner. Restore the erased cores and collars from the smallest scale upwards. We prove by address induction that every opening EC address of a virtual child is also virtual. Within its restored core this is immediate; at the input boundary the address is one of the leading ECs adjoined by the expanded-support rule of step 1.2, hence was claimed and erased together with that core, and is restored as a fresh ideal copy. Repeat down to elementary addresses. Therefore every wholly added child's entire expanded support is ideal, not merely its gate core. It is good at scale zero and, inductively, at every scale, so it makes no claim on a retained physical address. A retained child's new output EC pieces have just this property; its original physical faults and original leading addresses are unchanged. Induct on its scale: the added child roots are good and make no erasure, and the original child roots have unchanged bad flags and unchanged claims on original addresses. Hence the selected bad children and their template labels agree with the scan in which those output EC pieces are absent. This proves the needed scan mapping without replacing any retained real context by an ideal channel.

Specify the induction domain at one actual INPUT boundary, rather than intersecting constraints at different circuit times. Fix the fault pattern, root and truncation. At every exposed opening lower block port record the filter required by that opening component's leading EC; impose no filter at an opening bad component. Also record the outer one-scale filter $P_{s_i}$ on the decoded subblock coordinates of each parent input block, where $s_i$ counts the effective faults in its leading EC. These are all conditions on the same input registers. Under the recursive decoder each lower-port filter constrains the syndrome register of its decoder-tree node; the outer filter constrains the outer syndrome register. Each acts as identity on the final logical coordinates by step 1.1. Thus their joint allowed space is $U_{j,\mathrm{i}\mathrm{n}}^{-1}(H_{L,\mathrm{i}\mathrm{n}}\otimes K_{\mathrm{\partial }})$ for a syndrome subspace $K_{\mathrm{\partial }}$ (use a direct sum of allowed syndrome tuples if several boundary cases are allowed). No filter at a later intermediate time is included in this definition. We prove simultaneously at scale $j$: a good retained rectangle has ideal logical action on EVERY state in this full input space, with arbitrary reference; its syndrome-retaining form is the factor in step 3.1; a bad owner is its original exact conjugation; and a leading-EC subnetwork with $f\le 1$ effective child faults puts its decoded subblock coordinates in $P_f$, preserving their decoded logical state on $P_s$ when $s+f\le 1$. The EC assertion is on those decoded coordinates, not a claim of weight-at-most-one elementary error at every concatenation level. At scale one these assertions are exactly [A1] and step 2.1 and step 3.1.

Suppose the assertion holds at every scale at most $j$. Decompose a retained level-$(j+1)$ exRec using the actual level-$j$ block interfaces of step 2.2, descending through staggered collars. All components used here have scale at most $j$. Start with an arbitrary state in the full input sector of step 4.1, and process this DAG in topological order. For each next good component its leading EC is either at the initial boundary, where the required filter is part of $K_{\mathrm{\partial }}$, or is already in the processed prefix, where the lower-scale EC assertion forces that filter on EVERY incoming state. A bad component needs no input filter. This forward support induction proves eligibility of each lower-scale identity for every state in the parent input sector; it does not infer eligibility merely from one particular image of the parent leading EC. Contract their original channels and change coordinates as in step 3.2. The induction hypothesis replaces a good unitary component by its ideal logical gate and a syndrome-only channel; a good preparation by its prescribed pure logical state and a syndrome state; and a good destructive measurement by its ideal quantum-to-classical channel, discarding that measured block's syndrome. Classical outcomes remain explicit logical wires. On other blocks all syndrome registers remain references. The tensor syndrome channels on the surviving block edges commute with ideal logical gates on those edges, and with a measurement on its logical coordinate before its syndrome is discarded. If the parent is good there is at most one bad component by step 3.3. Keep each syndrome-edge channel in causal order. Its causal past supplies an arbitrary finite syndrome-memory input to that one fault; its causal future has no further access to logical data through a fault. After tracing the final syndromes, those future trace-preserving memory channels have no effect on the logical instrument and can be removed, even when conditioned on retained classical outcomes. With no bad component the whole syndrome network is of this harmless kind. Thus only the memory already arriving at the bad component is included in its effective fault map; no future outcome is pulled backwards and no other logical block is accessed. Classical controls are handled on each retained classical history, keeping the corresponding instrument branch and summing those branches at the end. This is the primitive one-scale template with at most one effective faulty location, the same classical ports, some output ECs omitted, and arbitrary finite memory only at that fault. It has not contracted multiple bad owners into a common channel or reordered memory interactions between them.

Apply [A1] to the resulting one-scale network. If $s_i$ effective faults are in leading EC $i$, the EC condition puts its coarse output coordinates in $P_{s_i}$ for every coarse input, with the smaller syndrome registers retained as reference or allowed fault memory. On a coarse $P_s$ input it also gives the asserted decoded preservation whenever $s+s_i\le 1$. This proves the auxiliary EC assertion at the new scale. The gate filter condition similarly propagates the coarse input filters, and its decoded identity, followed by any present output ECs, gives step 2.1 for the parent. Its absent output ECs remain absent. Since step 5.1 established every lower component's eligibility for ALL states in the input sector defined in step 4.1, this is a channel identity on that full sector, not just on the image of a preceding channel. Step 3.1 now supplies the parent's syndrome-retaining factor, pure preparation factor, or destructive measurement identity, as applicable. It remains to verify the ENTIRE boundary sector for the actual parent leading-EC output. Use the following cover of the actual exposed ports. A retained good opening level-$a$ component $p$ has its immediately preceding level-$a$ EC $e$ and the descending input collar of $e$ available as physical context, possibly owned by an earlier rectangle. Here availability is relative to the network under consideration: if $p$ is inside a larger claimed owner, that owner contains this context. If a different later owner had erased $e$ from this context, its only external quantum outlet would lead to $p$. By step 1.2 and step 2.2 the claim must then include that immediately following opening region; it cannot pass through or jump across a retained gate. Thus $p$ would have been removed into that owner, or would itself be the selected bad claimant, which imposes no boundary filter. Private EC records give no alternative outlet. This excludes precisely the case of a retained good $p$ whose necessary EC has disappeared; it does not assert that an EC owned elsewhere is absent from the physical circuit. For each such good $p$, its scan contains at most one bad child in total, hence at most one in $e$. To apply the EC assertion to $e$, first cover the opening ports of $e$ and its retained collar in the same manner at scales STRICTLY BELOW $a$. At scale zero there is no decoder input filter to supply. Ascending this finite cover tree, the already proved lower-scale EC assertion therefore forces each required filter for every incoming state, including an arbitrary output of a preceding bad owner. A bad opening component requires no filter, and virtual opening components have entirely ideal collars by step 3.3. For a parent of scale $j+1$, the largest $a$ used in this cover is $j$, so no same-level EC assertion is invoked to establish its own input domain. The cover establishes all lower exposed-port constraints of $K_{\mathrm{\partial }}$ independently; applying the elementary EC condition to the reduced actual parent leading EC then supplies its outer $P_f$ constraint. Their joint range is exactly the input-boundary sector defined in step 4.1. In particular no outer $P_f$ condition is used to infer a lower syndrome condition. A bad parent is still its original conjugated channel. This closes the simultaneous induction using only strictly smaller-scale identities in step 5.1 and in the cover descent, and elementary identities at the new scale. Encoded inputs or the prescribed pure preparations close the initial circuit boundary, and final destructive instruments give the ideal output law when all selected top roots are good.

A selected bad level-$r$ root, $r\ge 1$, contains at least two selected bad child roots in its retained scan. Choose the first two in the fixed order, and repeat inside each of them down to scale zero. The result is a full binary tree of depth $r$. A later selected bad child claimed every location of its retained exRec before the earlier child was processed. Hence the two child supports are disjoint. This remains true at every nested boundary because [A2] erases all overlapping elementary locations, not just the nominal outer EC. Induction down the tree gives $2^r$ distinct faulty elementary leaves. The same argument gives disjoint leaves for trees from jointly selected roots. Ideal completions create no faulty leaves.

Count the trees before considering probabilities. At each internal vertex its two child roots have labels in its fixed complete exRec template, with at most $b$ possibilities; hence their unordered pair has at most $A=\left(\genfrac{}{}{0px}{}{b}{2}\right)$ possibilities. Order that pair by the fixed template order. A full depth-$r$ binary tree has $2^r-1$ internal vertices, so it has at most $A^{2^r-1}$ labelings. A label sequence fixes every elementary leaf's physical location in the original schedule, regardless of which ECs the scan erased: truncation deletes locations and never changes a root's template address. Thus no extra count of truncation patterns is needed. Some labelings cannot survive a scan or repeat a leaf; discard them. Every actual witness is among the remaining predetermined labelings, by step 7.1.

For $k$ specified selected bad roots, choose one of these labelled witness trees for each root. There are at most $A^{k(2^r-1)}$ such tuples. Keep only tuples with $k{2}^r$ distinct elementary leaves. For a fixed retained tuple the probability all its leaves fault is ${\eta }^{k{2}^r}$ by [F1]; no restriction on other locations, erasure decisions, or additional faults is imposed. Step 7.1 makes the event of interest a subset of the union of these fixed leaf-fault events. Applying [F2] proves $\mathbb{P}(\text{all specified roots selected bad})\le A^{k(2^r-1)}{\eta }^{k{2}^r}$. This proof uses independence only for fixed elementary locations and therefore remains valid for fault-dependent truncations.