Theorem: Oai272-A conditional assembly

Suppose exact finite PPT maps $F,G:M_d(\mathbb{C})\to M_d(\mathbb{C})$ are supplied with certified nonzero product-free $Z=J(GF)$. Then the locally proved package establishes:

1. $Z/\mathrm{Tr}Z$ is an entangled PPT state in $\mathcal{C}$;

2. every admitted completed bit protocol on every tensor power has unhalved error at least $1/5$, and its model-specific distillable key is zero;

3. $GF$ is not entanglement breaking;

4. the explicit channel (eq:completion) is trace preserving and PPT on dimension $2d+1$, with non-entanglement-breaking square;

5. a certified product-support lower bound produces a separating witness for the square's normalized Choi state;

6. an independently implemented witness experiment has the finite-confidence conclusions of Theorem thm:statistics.

The theorem does not supply its own external maps, their geometric certificate, or an experimental implementation.

Proof. Items 1–2 are Lemma lem:transfer, Lemma lem:range, and Theorem thm:bit-gap. Item 3 is Lemma lem:choiEB. Item 4 is Theorem thm:completion. Item 5 is Proposition prop:support-witness and Corollary cor:channel-witness, with Theorem thm:witness-algorithm available on its rational input promise. Item 6 follows only after the additional experimental contract is satisfied.