Theorem: Hawk04-D conditional extrapolation certificate

Under the applicable parts of Definition def:acceptance:

1. Compatible stepwise complete comparisons give actual-to-proxy complete-channel distance at most $b_{\mathrm{tot}}$.

2. A proxy residual Choi discrepancy $e$ gives

   $${\delta }_{\mathrm{full}}(\mathcal{E})\le \min \{1,de+b_{\mathrm{tot}}\},{\epsilon }_{\mathrm{rec}}(\mathcal{N})\le \min \{a_d,\sqrt{2de}+b_{\mathrm{tot}}\}.$$

   A specified decoder gives error at most $\min \{1,d{r}_{\mathrm{dec}}+b_{\mathrm{tot}}\}$.

3. An independently proved accessible replacement comparison gives the lower bound $\max \{0,a_d-\eta \}$.

4. A matched inverse-square luminosity with relative power error $\rho <1$ gives the cutoff-lifetime bracket (eq:lifetime-bracket). It does not determine below-cutoff behavior.

5. The endpoint package gives the fixed-decoder bounds of Theorem thm:endpoint.

6. Any prescribed subsequent detector channel inherits the decoded channel allowance by CPTP contraction.

7. Residual Enter followed by Drop leaves the already supplied accessible channel unchanged and adds no final-burst conclusion.

The channel, mass, and endpoint conclusions follow from separate hypotheses. None supplies a missing hypothesis of another.

Proof. Telescoping matched CPTP compositions and contraction prove (i). Theorem thm:certificate proves (ii); Proposition prop:featureless proves (iii). Theorems thm:lifetime and thm:mass-stability prove (iv). Theorem thm:endpoint proves (v). Postprocessing contraction proves (vi), and Proposition prop:drop proves (vii). The hypotheses are explicitly partitioned by their mathematical objects, so the final scope assertion makes no additional physical identification.