Manuscript Oai290-A@1 · Oai290-A.tex · theorem · 7c6e104a

Theorem: Typed recovery decision

The corrected assembly and decision theorem · lines 1972–2043 · proof included or linked

Oai290-A@1#thm:assembly

Back to manuscript

Fix the three-ledger finite contract, a named effect or bounded Hermitian , a specified decoder, and threshold . Suppose a jointly valid event supplies the inputs of Theorem thm:certificate and any separately announced lower witnesses.

Then the following decisions are justified on that event:

  1. Specified quantum recovery certified. If , every input and reference has returned quantum error at most . Named effect and bounded-observable errors follow from Theorem thm:effect.

  2. Specified decoder excluded at the threshold. If , that implemented target channel has error larger than . This does not exclude a different decoder.

  3. All deterministic decoders excluded. If a lower bound from (eq:accesslower), (eq:complementlower), or Proposition prop:dimension exceeds , every decoder on that same access interface has error larger than .

  4. Effect-only reconstruction certified or excluded. A proved upper bound on certifies the measurement task at that bound. A lower bound from (eq:effectlower) applies to every boundary effect. Neither conclusion is automatically a full-code verdict.

  5. Exact correctability decided. A constant complete complement gives exact recovery and (eq:rankcapacity). A nonconstant complete complement excludes exact full-code recovery, but not every positive-error target.

  6. Otherwise inconclusive. If no applicable upper or lower bound separates the target, the result is inconclusive. Unverified contract inputs do not become certified by observing favorable data.

If the separate scalar-centralizer modular contract is also supplied, Theorem thm:bounded and Corollaries cor:boundeddefect–cor:intertwining give their bounded-witness conclusions. This conjunction does not identify the modular witnesses with the finite reconstructed observables.

A geometric conclusion requires Definition def:geometry. An endpoint conclusion requires Definition def:endpoint.

Proof. Items 1 and 2 are Theorem thm:certificate. Item 3 uses the lower bounds that are uniform over all decoders. Item 4 is Theorem thm:effect and Proposition prop:effectlower. Item 5 is Theorem thm:exact and Corollary cor:nonconstant. Item 6 follows because none of those theorems supplies a converse to an unsuccessful sufficient certificate.

The modular conclusions have their own printed hypotheses and proofs. No connecting map is among the assembly inputs. The geometric and endpoint definitions supply additional objects, so they cannot be inferred by omitting those inputs.

Nearby in this section