Allocate local error budgets through a pipeline

Inputs: a finite list of $L$ stage compilers $C_1,\dots ,C_L$, each accepting a rational local precision and, when it uses randomized verification, a rational local failure budget; rational targets $0<\epsilon ,\delta <1$; and declared stage input/output interfaces $T_0,\dots ,T_L$, including encodings or register spaces. Stage $j$ must accept $T_{j-1}$ and return $T_j$ at every admissible budget, so adjacent interfaces match. For a channel pipeline these are the matching spaces and channel interfaces of End-to-end channel and output error contract. Each compiler is assumed to terminate with an implemented stage, its output type, and its actual cost record under Classical output, quantum-state output, and access costs. The sequential pipeline is run under the same declared cost-accounting model.

Output: a pipeline from $T_0$ to $T_L$, together with the budget lists and cost records below. If $L=0$, a single interface $T_0$ is supplied; return its identity procedure, empty budget lists, no stage records, and an auxiliary record charging any identity-interface and allocator work. If $L\ge 1$, set ${\epsilon }_j=\epsilon \mathrm{/}L$ and ${\delta }_j=\delta \mathrm{/}L$ for each $j$. For $j=1,\dots ,L$ in order, invoke $C_j({\epsilon }_j,{\delta }_j)$ once when stage $j$ uses randomized verification, and otherwise invoke $C_j({\epsilon }_j)$ once and mark its failure coordinate not applicable. Retain each returned implementation, output type, and actual stage cost record, then compose the stages chronologically. Record shared input/preprocessing, allocation arithmetic, and any interstage wiring, control, postprocessing, or final-output costs in a separate auxiliary record, counting each operation once. Return the composed implementation, local budget lists, per-stage records, and auxiliary record. The correctness theorem gives an additive resource bound from these records under its explicit accounting assumptions; a requested precision alone does not determine an implementation or its cost.

The correctness claim is separate: Allocated local errors meet the global budget proves the global channel and failure bounds and composes the recorded cost coordinates under explicit stage and pipeline accounting assumptions. This algorithm does not create implementations or amplify a compiler's error; each compiler's correctness method and cost remain part of its own guarantee.