Theorem: Conditional operational assembly

Fix one circuit instance as in Definition def:instance, one target channel, one output-ownership specification, and one resource library.

Assume:

1. an independent mathematical certificate proves $d_{\diamond }({\mathcal{C}}_f,\mathcal{U})\le s$, or an operational certificate proves such a bound with its stated statistical coverage;

2. implementation comparisons satisfy the common-interface and memory assumptions of Section sec:errors;

3. a transport interpretation is claimed only when Specification spec:transport is supplied;

4. all returned residual and classical factors are included in any complete-output claim;

5. empirical statements use a predeclared complete-record statistical and calibration contract.

Then:

1. the implemented logical error satisfies (eq:totalbudget), with arbitrary untouched references;

2. any supplied geometric endpoint and arrival estimates combine with that logical bound exactly as in Theorem thm:transport;

3. the declared finite gate, call, storage, table, communication, and test ledgers are preserved under the stated compositions;

4. a test threshold has certified, excluded, or inconclusive outcomes according to its rigorous channel interval.

The theorem does not require or prove the universal assertion (eq:documentary).

Proof. Lemma lem:semantics supplies the complete channel. Lemma lem:telescoping, or Lemmas lem:clean-telescope and lem:isometry when their hypotheses apply, gives the implementation comparison. The independent logical certificate adds by the triangle inequality.

The endpoint and arrival conclusion is Theorem thm:transport. Resource counts are those of the actual finite instruction sequence; branchwise peaks retain all supplier holdings declared by the resource model.

For an empirical interval $[L,U]$ and threshold $\tau$, certify when $U\le \tau$, exclude when $L>\tau$, and otherwise return inconclusive. The coverage statement follows from the simultaneous event on which the interval contains the true channel error. No catalogue result enters these arguments.