Oai272-A Finite Certificates for Secret-Bit Obstructions and PPT-Composition Counterexample Interfaces A source-qualified proof, audit, and separation manuscript

We develop a self-contained certificate framework for the external Family 272 claims while keeping the explicit dimension-ten geometric construction outside the verified release. For a precisely specified local-instrument model, we prove the common-factor form of Eve's complete-transcript output. A four-effect inequality then yields a uniform unhalved trace-norm distance of at least $1/5$ from every ideal secret bit for states represented by two completely positive, completely copositive local maps. The final numerical implication has an exact rational certificate, independent of copy number, communication length, and local processing cost.

We separately prove the Choi transfer identity, the product-free range criterion, and the conversion of a PPT pair into a trace-preserving PPT channel in dimension $2d+1$. We give a terminating, promise-dependent finite procedure producing an entanglement witness from an exact rational product-free support, and derive a complete-record statistical certificate for a specified witness measurement. These are conditional construction and verification interfaces, not an execution of the external dimension-ten arithmetic.

Several corrections are essential. Restricting an already excluded protocol class preserves the obstruction. Product-free range is sufficient for entanglement, not necessary for the zero-key argument. A Bell-overlap recovery test cannot detect PPT entanglement. The full channel Choi matrix need not have product-free range even when its compressed corner does. The inspected Comparator targets contain sorry; their statements are not machine-checked proofs, and neither target formalizes the secret-key theorem. The supplementary integer checks concern a separate combinatorial construction, not every argument in the paper.

The completed release is the local certificate and reduction package. It does not independently establish the external matrices' required geometric properties, minimal dimensions, or a gravitational interpretation. No Page curve, island, gravity-generated-entanglement test, or exclusion of classical gravity is constructed.

The supplied plan has stages $0$–$6$. Its mathematical completion must distinguish:

1. a locally proved implication;

2. an explicit finite certificate for that implication;

3. verification that particular external matrices satisfy its hypotheses;

4. an experimental or computational execution.

None of these categories substitutes for another.

The principal locally proved results are Theorems thm:bit-gap, thm:rational-gap, thm:completion, thm:witness-algorithm, and thm:assembly. The dimension-ten construction is retained as a documentary application target. Consequently, this manuscript is not a purported independent proof of every result in the external Family 272 paper.

The source paper is attributed to OpenAI and dated 27 September 2026 OpenAI272. The companion identification page distinguishes that source from Cheung's programme Companion272. This development uses the requested identifier Oai272-A. It does not assert authorship, registration, approval, or endorsement of this development by N. Cheung.

The external paper asserts an explicit entangled density operator

whose range contains no nonzero product vector. For its admitted completed local-instrument protocols on every ${\rho }^{\otimes n}$, Eve retains a purification and the entire public transcript. The asserted distance from every ideal secret bit is at least $1/5$ in unhalved trace norm, equivalently at least $1/10$ in trace distance. Its stated distillable key is zero.

The protocols allow joint processing of all copies and authenticated two-way public communication without a uniform communication bound. The input is the only shared private resource. This is not a statement about every entangled state or every operational enlargement of that protocol model OpenAI272.

The source specifies PPT maps

without requiring trace preservation, and asserts that

Its state is $\rho =Z/\mathrm{Tr}Z$, not generally $Z/10$. The pair therefore supplies a counterexample to the unrestricted two-map PPT-composition assertion, provided its advertised positivity and range properties hold OpenAI272.

A different construction in the source gives a trace-preserving PPT channel

whose square is asserted not to be entanglement breaking. The source does not claim that dimensions $10$ or $21$ are minimal. Failure at the second iterate does not assert failure of eventual entanglement breaking OpenAI272.

These three records are not premises of the local theorems below. In particular, the notation $\rho ,{\Phi }_1,{\Phi }_2,\Theta$ in a record does not assert that their external construction has been checked here.

The following distinctions were checked against the publicly accessible source files on 14 October 2026.

scope versus proof. The scope note lists a dimension-ten pair target and a dimension-twenty-one channel target, and expressly excludes the zero-key theorem LeanScope. More strongly, the inspected files end the relevant theorem bodies with by sorry:

LeanPair,LeanChannel. They specify targets; those bodies are not completed proofs. No Lean execution or independent checking of other repository files is asserted.

arithmetic roles. The dimension-ten argument uses its own algebraic and arithmetic certificate. The supplementary integer programs described in the paper concern the separate projection/combinatorial construction. Their scope does not include all geometric, operational, or nonseparability arguments, and they do not instantiate that construction's large global matrices Supplementary272.

sizes. A Choi matrix for a map $M_{10}(\mathbb{C})\to M_{10}(\mathbb{C})$ is $100\times 100$. For $M_{21}(\mathbb{C})\to M_{21}(\mathbb{C})$, it is $441\times 441$. The phrase “enormous global matrices” in the supplementary-check discussion must not be silently transferred to identify the dimension-ten Choi matrix with the separate large combinatorial objects.

entanglement breaking. Park's preprint, first submitted on 13 August 2026, states eventual entanglement breaking for every finite-dimensional PPT endomap, with a map-dependent iterate Park. We do not independently verify that preprint. Nevertheless, a proposal that a PPT channel never becomes entanglement breaking would need to confront that stated theorem; it is not a consequence of a second-iterate counterexample. Earlier results established important eventual-breaking cases HansonRouzeFranca.

All finite matrix spaces are complex and have fixed orthonormal bases. Transpose $T_d(X)=X^{\mathsf{T}}$ is complex-linear. A map $F:M_a(\mathbb{C})\to M_b(\mathbb{C})$ is PPT if $F$ and $T_{b}F$ are completely positive. No trace condition is included.

We use the unnormalized Choi convention

A channel has $\mathrm{Tr}J(F)=a$, and its normalized Choi state is $j(F)=J(F)/a$. A nonzero CP map without trace preservation instead has normalized Choi state $J(F)/\mathrm{Tr}J(F)$.

For states and compatible channels,

The diamond norm includes an independent reference Watrous. Natural logarithms are used unless a base is displayed; key lengths are measured in bits.

A positive bipartite matrix is separable if it is a finite sum ${\sum }_r{A}_r\otimes B_r$ with $A_r,B_r⪰0$. A CP map is entanglement breaking at the CP-cone level if every positive referenced input has separable output. This definition also applies to maps that are not trace preserving.

A density operator $R$ on $A\otimes B$ belongs to $\mathcal{C}$ if

where $\chi$ is a finite bipartite vector and

are CP, for the respective input dimensions $r,s$. Only $R$ is normalized. Neither representing map is required to preserve trace, and $\chi$ need not have unit norm.

This is a mathematical representation, not a supplied physical implementation of $L$ and $M$.

For a CP map $F:M_a(\mathbb{C})\to M_b(\mathbb{C})$, its adjoint and $T_{b}F{T}_a$ are CP. Moreover,

Adjoints and transpose-adjoints of PPT maps are PPT. Every state in $\mathcal{C}$ is PPT, and $\mathcal{C}$ is closed under finite tensor products after grouping the parties.

Proof. If $F(X)={\sum }_{\alpha }{K}_{\alpha }X{K_{\alpha }}^{†}$, then

These formulas prove the CP assertions and the equivalence. Taking adjoints proves the transpose-adjoint statements.

For (eq:C),

Tensor the representing maps and vectors. In product bases, the transpose on a tensor product is the tensor product of the transposes. The required CP conditions therefore persist.

PPT is only a consequence of the representation. It is not a substitute for the representing maps in the four-effect proof below. Positive key from some PPT bound-entangled states is established in the literature HHHO2005,HHHO2009.

The following operational requirements make explicit the model used in the local proof. They preserve the source's relevant resource and complete-history distinctions OpenAI272,CLMOW.

An admitted protocol has finite-dimensional bipartite input $A\otimes B$, local quantum memories and local CP instruments, and classical public communication. It satisfies:

1. An initial standard Borel public variable $C_0$ is recorded and independent of the input and every untouched reference. Conditional on $C_0$, the private auxiliary resources of the two laboratories are independent of each other and of the input. Their preparation kernels are fixed when the input is changed. There is no other shared resource or preshared secret key.

2. Each instrument has a standard Borel outcome space, measurable conditional laws and updates, and trace-preserving total. Its choice depends only on its laboratory's earlier private history and the preceding public record.

3. After any explicitly supplied local aggregation, the genuine classical history has finitely or countably many coordinates in fixed standard Borel spaces. Aggregations retain all subsequently used private records and memories and are valid on arbitrary inputs with untouched finite references.

4. Every public message is generated by its sender from its own history and the preceding public record. An independent public-source draw uses a fixed kernel depending only on that record and acts trivially on quantum systems. Public controls, speaker choices, stopping decisions, and public randomness are included in the complete transcript $T$.

5. Unnormalized finite-prefix laws are one reference-compatible instrument family on arbitrary positive inputs. Tracing current memories and summing the next outcomes recovers the preceding reference matrix measure.

6. A terminal classical output is a measurable function of local history and $T$. If a terminal quantum readout is used after a complete infinite history, both its incoming local CP process and the readout instrument are supplied. They are local, reference-compatible, and jointly refine the complete-history matrix measure. Summing the terminal outcomes removes those refinements. An unspecified infinite quantum evolution is not declared to be a terminal instrument.

7. Each local output has a specified finite alphabet and a missing symbol $\perp$. A completed protocol produces its prescribed output at both laboratories almost surely on the actual input, with normalized total output. Completion on auxiliary inputs is not required.

Eve retains the original purification and the complete public transcript, not private instrument labels merely used inside a laboratory.

There is no uniform upper bound on communication, local memory, copy number, or finite-prefix length in this specification. It does not silently identify all topological closures of LOCC with a protocol possessing the required terminal process CLMOW.

For a standard Borel transcript and a finite quantum register, a positive state is a positive matrix-valued measure of total trace one. If a Hermitian difference has density $H(t)$ with respect to a common finite dominating measure,

This norm is independent of the dominating measure.

If

then

Proof. Write the block matrix as ${\sum }_{\alpha }\left(\genfrac{}{}{0ex}{}{u_{\alpha }}{v_{\alpha }}\right){\left(\genfrac{}{}{0ex}{}{u_{\alpha }}{v_{\alpha }}\right)}^{†}$. Then

Let $R\in \mathcal{C}$, and let $X_0,X_1,Y_0,Y_1⪰0$. Put

Then

No POVM normalization of the four local matrices is required.

Proof. Choose (eq:C), and write

First make the $A_i$ commute by a change of representation. For $H=A_0+A_1$, let $S$ equal $H^{-1/2}$ on $\mathrm{ran}H$ and the identity on $\ker H$. Replace

The output is unchanged. The new pullbacks sum to the support projection of $H$, so they commute. The PPT condition persists because

Suppress the new notation, set $C=L\otimes M$, and define

Applying Lemma lem:block to $C$, and then to the CP map $C(T_r\otimes T_s)$, gives

For the second estimate use the input vectors $\overline{v},\overline{u}$; transposition exchanges the two diagonal inputs and leaves the desired off-diagonal output.

Let $P$ be the common spectral projection where $A_0\ge A_1$, and split

The pullback cross terms vanish, and

Equation (eq:two-block) bounds the four terms in the expansion of $C(|\chi ⟩⟨\chi |)$, respectively, by

The triangle inequality proves (eq:four). No inverse of an output state or effect was used.

The source identifies (eq:four) as its four-effect step. The argument above states the complete finite algebraic hypotheses rather than importing a result from a recovery manuscript OpenAI272.

Fix a density $R$ on $A\otimes B$, and use the canonical purification

For a completed bit-output protocol satisfying Specification spec:protocol, there are a finite positive measure $\mu$ on the complete transcript space and measurable positive matrices $X_i(t),Y_j(t)$ such that Eve's unnormalized bit-branch densities are

outside a single null set. The same two local pairs work in all four branches, and

Proof. For a finite protocol, fixing the public transcript fixes all public choices. The compatible private histories sum separately in the two laboratories. Thus the final branch map is a product of two local CP maps. Pulling back the identity gives $X_i,Y_j$, and tracing the laboratory outputs in (eq:canonical) gives (eq:transcript).

We give the complete-history argument because finite-prefix factorization alone does not justify every infinite terminal readout.

Let $a=\dim A$, $b=\dim B$, and run the same protocol on

The references $A_0,B_0$ are untouched. On this auxiliary input replace a missing local bit by zero, without replacing a bit already produced by the other party.

Choose finite informationally complete POVMs on the references. They can be measured at the beginning because they commute with all laboratory operations. Conditional on $C_0$, the tested experiment has independent local sampling tapes $U,V$. Measurable sampling of standard Borel probability kernels and regular conditional laws are available in this setting Kallenberg.

Write ${\mathcal{F}}_m$ for the public prefix sigma field. Induction gives conditional independence of $U,V$ given ${\mathcal{F}}_m$. For example, after Alice's next message, ${\mathcal{F}}_{m+1}\subseteq \sigma (U)\vee {\mathcal{F}}_m$, and

Conditioning once more and multiplying by bounded functions of $U$ proves the product identity at $m+1$. The Bob step is symmetric. At a public-source step the new kernel depends only on the public prefix and does not change either conditional private marginal.

For bounded $u,v$, martingale convergence of conditional expectations in $L^2$, followed by Cauchy–Schwarz for the products, therefore gives

Countable generating algebras on the standard Borel tape spaces make this a conditional product-law identity outside one null set. In particular it applies to the defaulted local bits and the local reference-test outcomes. The supplied local terminal processes in (P6) are included in these genuine tested laws.

Next retain the reference systems instead of measuring them. By (P5), the finite-prefix reference matrix measures are consistent. Their scalar positive tests extend to the countable history space; polarization recovers the matrix entries. Positivity follows by testing a countable dense family of reference vectors and then continuity. The terminal refinements in (P6) give positive bit-conditioned reference measures $W_{ij}$ on that same complete history.

Push these measures to $T$ and dominate them by

Entrywise Radon–Nikodym derivatives yield positive densities $W_{ij}(t)$. Set

The conditional product law of the informationally complete tests gives

Since $E_r\otimes G_s$ span the Hermitian matrices,

simultaneously for all branches.

Finally apply the algebraic reference filter

Acting on the auxiliary product probes, it prepares exactly (eq:canonical). It commutes with every laboratory operation and public scalar kernel. Reference compatibility and uniqueness of the complete-history measures consequently give filtered branch laws $K{W}_{ij}{K}^{†}$.

On the actual input the event of a missing bit has probability zero. Its filtered positive matrix is therefore zero, as is the filtered matrix of every subevent. Auxiliary defaults thus make no contribution to the actual output. Taking

gives (eq:transcript). Normalization follows from completion. The filter need not be a physical operation and no inverse of $R$ is required.

This proof retains private histories privately. It does not announce private Kraus labels to Eve, condition on a positive-probability singleton of a continuous transcript, or assume convergence of unused quantum memories.

For positive matrices define root fidelity by

This is not squared fidelity.

For square matrices $A,B$,

For positive $H,K$,

Also $f(H^{\mathsf{T}},K^{\mathsf{T}})=f(H,K)$.

Proof. Extend the polar partial isometries to unitaries for the first identity. Transpose invariance follows from functional calculus and invariance of singular values under transpose and adjoint.

For (eq:fidelity-lower), put $A=\sqrt{H}$, $B=\sqrt{K}$, $D=A-B$. Since $H-K=AD+DB$, trace-norm duality gives

On a unit eigenvector of $D$ with eigenvalue $d$, positivity gives $⟨A+B⟩\ge |d|$. Thus

The normalized version is a standard trace-distance/fidelity comparison FuchsVanDeGraaf; the displayed proof fixes the unnormalized convention needed here.

A normalized bit output has a transcript-coherence certificate if, with respect to a finite transcript measure, its positive Eve densities ${\tau }_{ij}(t)$ satisfy

and

This is a finite collection of scalar inequalities after the analytic transcript and coherence statements have been proved. It is not a claim that observing a few finite protocols proves a universal quantifier over all protocols.

For $R\in \mathcal{C}$, every completed bit protocol of Specification spec:protocol, with Eve's canonical purification, satisfies Definition def:TC.

Proof. Use Theorem thm:transcript. The fidelity identities give

Apply Lemma lem:four pointwise and scalar Cauchy–Schwarz to each integral.

For a normalized Eve law ${\sigma }_{ET}$, define

For a bit output $\tau$, write

A secure fixed-length key-distillation sequence has lengths ${\ell }_n\ge 0$ and comparison laws ${\sigma }_n$ such that

Its lower asymptotic rate is ${\mathrm{liminf}}_n{\ell }_n/n$. The corresponding $K_D$ is the supremum over admitted secure sequences, including the empty-key sequence.

This is the purification-and-public-transcript security task, not quantum recovery from a classical record HHHO2009,CheungI,CheungHawk04B.

Every normalized output with a transcript-coherence certificate obeys

for every normalized comparison law $\sigma$.

Consequently, if $R\in \mathcal{C}$, the same bound holds for every $n\ge 1$ and every completed protocol on $R^{\otimes n}$ satisfying Specification spec:protocol. It holds for every initial purification retained by Eve, and $K_D(R)=0$ for this model.

Proof. Use a common dominating measure for the actual transcript law and the ideal comparison law. This retains their singular parts. Homogeneity preserves (eq:TC).

Set

The classical bit blocks give

The total trace deficit in the two matching blocks is $e$; hence $a_0+a_1\ge e$, so

Lemma lem:fidelity also gives

or

Cauchy–Schwarz and the arithmetic–geometric mean inequality simplify (eq:TC) to

If $e\ge 1/10$, (eq:eta2e) proves (eq:gap). If $0\le e\le 1/10$, then

Equation (eq:etaf) again proves (eq:gap).

For $R^{\otimes n}$, tensor closure and Lemma lem:Ccertificate supply the same certificate. For an arbitrary purification, an Eve-side channel recovers the canonical purification from it: invert its purifying isometry on its range and complete the map by fixed-state preparation on the orthogonal complement. This channel fixes the bits and public transcript, maps ideal keys to ideal keys, and contracts trace norm.

Finally, retaining the first bit locally from any nonempty ideal uniform key gives an ideal bit and cannot increase distance. A secure sequence therefore cannot have ${\ell }_n\ge 1$ for infinitely many $n$. Its lengths are eventually zero, and its rate is zero. The empty key attains zero rate.

This proves the operational engine for the explicitly defined class and protocol model. It does not prove that a particular external entangled matrix belongs to that class until the matrix construction and its certificates are supplied.

The scalar constraints

imply $\eta \ge 1/5$.

The numerical proof requires only the rational identity

on $0\le e\le 1/10$, together with a split at $e=1/10$.

The constant $1/5$ is optimal for this scalar relaxation:

satisfies all four scalar constraints. This does not assert attainability by a physical state or protocol.

Proof. For $e\ge 1/10$, use $\eta \ge 2e$. Otherwise the two factors on the right of (eq:rational-certificate) are nonnegative. Thus $f\le 3/10+1/10=2/5$, and $\eta \ge 1-2f\ge 1/5$. The displayed equality tuple proves the relaxation statement.

This is an exact finite mathematical certificate, not a simulation, tomography result, or universal proof obtained by enumerating protocols. The universal content lies in Theorem thm:transcript, Lemma lem:four, and tensor closure; the constant itself needs no enormous matrix.

If the same normalized output instead satisfies

then

Proof. The case $e\ge 1/10$ gives $\eta \ge 1/5$. For $e\le 1/10$, the upper bound is $\mathfrak{f}\le 2/5+\kappa$, while $\eta \ge 1-2\mathfrak{f}$.

The allowance $\kappa$ must be derived uniformly in the intended inputs and protocols. A statistical radius for one experiment does not automatically provide such a universal defect.

For the outputs in Theorem thm:bit-gap:

1. Conditioning on a measurable public-transcript event with probability $r>0$ preserves the $1/5$ gap for the normalized accepted output.

2. If a completed output includes local abort symbols with joint abort probability $a<1$, and ${\eta }_{\mathrm{ok}}$ is its normalized non-aborting distance from an ideal bit on a common Eve interface, then

   $$(1-a){\eta }_{\mathrm{ok}}+2a\ge \frac{1}{5}.$$

   In particular, vanishing abort probability cannot coexist with vanishing non-aborting key error.

Proof. For (1), restrict the transcript measure to the public event and divide every branch density by $r$. In (eq:transcript), absorb $1/r$ into both Alice effects. The four-effect inequality is homogeneous, so the normalized accepted output has the same certificate.

For (2), replace each party's own abort symbol by zero. This is a local completed bit protocol. Its distance from the chosen ideal bit is at most $(1-a){\eta }_{\mathrm{ok}}+2a$, since the distance between normalized states in unhalved trace norm is at most two. Apply Theorem thm:bit-gap.

Suppose a certified ideal output has gap $1/5-2\kappa$, and an implemented output on the same bit–Eve interface satisfies

Then its distance from every ideal bit obeys

Compatible stepwise half-diamond allowances $b_1,\dots ,b_m$ give the valid choice $b\le \min \{1,{\sum }_j{b}_j\}$.

Proof. Use the triangle inequality and telescope compatible channel compositions. Pre- and postcomposition by channels contract diamond distance.

The comparison interface must retain Eve's purification and all public information. A comparison only on Alice's selected bit is not sufficient.

Let

Discarding $T$ gives a perfect uniform correlated bit. With $T$ retained, however,

Indeed, dephase $\sigma$ in the transcript basis. For either transcript value, the sum of the two classical absolute differences is $1/2$, independently of that transcript's comparison probability. Summing gives one, and the uniform comparison law attains it.

A uniform obstruction proved for a protocol class also holds for every subclass. In particular, the zero-key conclusion of Theorem thm:bit-gap implies zero one-way key and zero key under any fixed communication budget within that model.

Proof. The same lower bound applies to each member of the smaller class. Equivalently, optimizing a rate over fewer protocols cannot increase it.

Thus the plan's “drop two-way discussion” and “drop unlimited communication” entries require correction. A positive-rate comparison or a sharp one-way/two-way formula could be new work; the inherited zero upper bound is immediate. An entangled-game repetition theorem is not needed for that logical restriction.

A CP map $F$ is entanglement breaking if and only if $J(F)$ is separable. This equivalence does not require trace preservation.

Proof. If $J(F)$ is separable, refine its positive factors spectrally:

Comparison of matrix-unit blocks gives

On a positive referenced input this is a sum of positive product operators. Conversely, apply the defining entanglement-breaking property to $|{\Omega }_a⟩⟨{\Omega }_a|$.

This is the standard measure-and-prepare characterization HSR2003; the CP and matrix-unit conventions are fixed by the Choi correspondence Choi1975,Watrous.

Every nonzero separable positive matrix has a nonzero product vector in its range. Hence a nonzero positive matrix with product-free range is entangled.

Proof. Write a separable positive matrix as $Z={\sum }_{\alpha }|u_{\alpha }\otimes v_{\alpha }⟩⟨u_{\alpha }\otimes v_{\alpha }|$. Its kernel is the intersection of the orthogonal complements of these product vectors, so every summand vector lies in $(\ker Z{)}^{\perp }=\mathrm{ran}Z$. At least one is nonzero.

Only this sufficient failure of a necessary separability condition is used. It is not an equivalence HorodeckiRange.

For CP maps $F:M_a(\mathbb{C})\to M_b(\mathbb{C})$ and $G:M_b(\mathbb{C})\to M_c(\mathbb{C})$, define

Then

If both maps are PPT and $Z=J(GF)\ne 0$, then

Proof. For Kraus matrices $A_r$ of $F$ and $B_s$ of $G$, the Kraus matrices of $F^{♯}$ are ${A_r}^{\mathsf{T}}$, and

Sum their rank-one projectors to prove (eq:transfer). Lemma lem:stability supplies the four CP conditions. Finally $\mathrm{Tr}Z>0$ because $Z$ is positive and nonzero.

The identity is also part of the established PPT-composition framework CMHW2019. The normalization is by the actual Choi trace, with no additional factor $b$.

If PPT maps $F,G$ have nonzero $Z=J(GF)$ with product-free range, then $Z/\mathrm{Tr}Z$ is an entangled PPT state with zero distillable key for Specification spec:protocol, and every completed bit protocol has the $1/5$ gap.

Proof. Apply Lemmas lem:range and lem:transfer, then Theorem thm:bit-gap.

The external dimension-ten arithmetic must establish the hypotheses of this corollary. The corollary does not establish those hypotheses by referring to the catalogue.

Let $F,G:M_d(\mathbb{C})\to M_d(\mathbb{C})$ be PPT. There are explicit $s,t>0$ and a trace-preserving PPT channel $\Theta :M_{2d+1}(\mathbb{C})\to M_{2d+1}(\mathbb{C})$ whose squared Choi matrix has a coordinate-local corner equal to $stJ(GF)$. If $J(GF)$ is entangled, ${\Theta }^2$ is not entanglement breaking.

Proof. Set

Since $A,B⪰0$,

Use the real coordinate inclusions $V_0,V_1$ in

Write $X_{jj}={V_j}^{†}X{V}_j$. Define

The moving terms are CP. Each flag term is a positive-effect measurement followed by a fixed preparation, hence CP. The identities $sA+D=tB+E=I$ prove trace preservation.

Output transpose replaces $F,G$ by $T_{d}F,T_{d}G$ in the moving branches and fixes $P_{\star }$. All branches remain CP, so $\Theta$ is PPT. This uses ordinary complex-linear transpose; it does not conjugate the scalar flag coefficient.

The flag is absorbing. For every $Y\in M_d(\mathbb{C})$,

Expanding in input matrix units gives

Local compression preserves separability. Therefore a separable $J({\Theta }^2)$ would force separability of its entangled corner, a contradiction.

This switch-and-flag mechanism has precedents in PPT-composition and trace-decreasing-map completion CMHW2019,Filippov2021. It is proved here for the stated interface rather than inferred from a channel-synthesis template.

For general complex input and output isometries $W,V$,

The real coordinate inclusions in (eq:corner) remove this otherwise important distinction.

The full $J({\Theta }^2)$ has the product direct summand $P_{\star }\otimes P_{\star }$. Its range is therefore not product-free. The proof of nonseparability uses the entangled corner, not a false product-free claim for the full channel Choi matrix.

Assume a PPT pair $F,G:M_d(\mathbb{C})\to M_d(\mathbb{C})$ has entangled $J(GF)$. There is a trace-preserving PPT channel $\Xi :M_{3d+1}(\mathbb{C})\to M_{3d+1}(\mathbb{C})$ such that

Proof. Replace the two-block cycle in (eq:completion) by the acyclic transitions

Send the missing trace from each transition to the absorbing flag, and discard input off-diagonal blocks. The same branchwise proof gives a PPT channel. The input-block-$0$, output-block-$2$ corner of its square is $stJ(GF)$. After three steps every input block has reached the flag. Trace preservation identifies the remaining scalar with $\mathrm{Tr}X$.

This is a conditional construction from any qualifying pair. It is not a new assertion that the external channel in dimension $21$ has a particular third iterate.

Let $\dim Q=d\ge 2$. If the only input-dependent accessible output is a classical measurement record, then every quantum decoder implements an entanglement-breaking channel $\Lambda$, and

Basis measurement followed by basis-state preparation attains the bound.

Proof. The decoded channel has the form

Its Bell-input output is separable. For normalized product states,

Convexity and the Bell-projector test give the lower bound. Computational dephasing is the average of $d$ phase-unitary conjugations; the triangle inequality gives the matching upper bound $1-1/d$.

This is the finite distinction emphasized in Cheung's Landmark I, VIII-B, and Hawk04-B CheungI,CheungVIIIB,CheungHawk04B. It does not apply when an authorized input-dependent quantum memory is also retained.

The channel

has a constant selected record and exact recovery from the retained memory. Replacing it by a record-only interface changes the task.

A classical record can support classical secret key while failing to recover an unknown quantum state. Conversely, recovery failure alone does not prove a zero secret-key rate. The purification and public-transcript security conditions are indispensable HHHO2009.

For a finite instrument $\{{\mathcal{A}}_x{\}}_x$, let $r_x=\mathrm{rank}J({\mathcal{A}}_x)$ after zero maps are removed, and $R_0={\sum }_x{r}_x$. A pure-environment isometric implementation with orthogonal outcome blocks has minimum environment dimension $R_0$. Its full-readout environment register needs

qubits. A prescribed rectangular outcome/index split needs

Proof. The minimum Kraus number of a CP map is its Choi rank: spectral decomposition supplies that many Kraus vectors, while any Kraus decomposition is a positive sum of rank-one Choi matrices and cannot use fewer. Orthogonal outcome blocks add their dimensions. The displayed encodings attain the bounds.

This is the declared one-shot model in En02-A CheungEn02A ({thm:Dprime}). It is not a lower bound on every adaptive peak memory and does not replace (eq:four).

The detailed supplied statements support the first three and the En01-C/Em03 comparisons CheungHawk04B,CheungEn02A,CheungEn02B,CheungEn02C, CheungEn01C,CheungEm03F,CheungEm03G. Other named sheets are retained as the plan's comparison nominations where a full theorem statement was not supplied; no missing theorem number or model identification is invented ComparisonDossier.

For an entangled corner, the appropriate successor object is a separating entanglement witness. A separable decomposition of that same corner cannot be the desired output.

Let $0\ne Z⪰0$ on ${\mathbb{C}}^a\otimes {\mathbb{C}}^b$, and let $P$ be its range projection and $Q=I-P$. If $\mathrm{ran}Z$ is product-free, then

For every $0<ϵ\le {\delta }_{\ast }$,

is nonnegative on every positive separable matrix and satisfies

Proof. The product of the two unit spheres is compact. A zero minimum would give a unit product vector in $\ker Q=\mathrm{ran}Z$. Thus the minimum is positive. The defining lower bound proves block positivity of $W$, which extends to the separable cone. Since $QZ=0$, the negative expectation follows.

Suppose $Z\ne 0$ is a positive matrix with entries in $\mathbb{Q}+i\mathbb{Q}$, and its range is product-free. There is an exact-arithmetic procedure which terminates and outputs rational $ϵ>0$ and

as in Proposition prop:support-witness. It supplies a finite rational certificate for global product nonnegativity. No polynomial running-time bound is asserted.

Proof. Gaussian elimination selects a full-column-rank rational matrix $V$ spanning $\mathrm{ran}Z$. Therefore

have rational complex entries.

For integers $M\ge 2(a+b)$, use all nonzero complex grid vectors whose real and imaginary coordinates are integer multiples of $1/M$ in $[-1,1]$, and normalize them. They form unit-sphere nets ${\mathcal{N}}_a(M)$, ${\mathcal{N}}_b(M)$. Rounding and then normalizing gives covering radii at most $2a/M$, $2b/M$, respectively.

For unit vectors, $0⪯Q⪯I$ gives

where $q(x,y)=⟨x\otimes y,Q(x\otimes y)⟩$. Consequently, with

every unit product vector has $Q$-expectation at least ${ϵ}_M$.

Each grid expectation is rational. If $x=g/\Vert g\Vert$ and $y=h/\Vert h\Vert$, its value is

with rational numerator and denominator. Thus all comparisons are exact. Try successively doubled $M$ until ${ϵ}_M>0$. Because $m_M\ge {\delta }_{\ast }>0$, termination follows.

For a fixed $M$, at most

pairs are tested. Their rational values and the Lipschitz allowance certify the global lower bound. The potentially very small unknown ${\delta }_{\ast }$ prevents a claimed efficient complexity bound.

This is a genuine finite construction theorem under its exact input and support promises. It does not construct the external $Z$, prove its promise, or execute the search. Algebraic rather than rational input requires a declared exact algebraic-number representation and comparison procedure.

Under Theorem thm:completion, suppose $Z=J(GF)\ne 0$ has a witness $W=Q-ϵI$ from Proposition prop:support-witness. For $D=2d+1$, set

Then $\hat{W}$ is nonnegative on the full separable cone and

Proof. Compression of a product vector is a product vector, possibly zero. This proves block positivity of $\hat{W}$. Equation (eq:corner) gives the expectation and the factor $1/D$ from normalized Choi convention.

An algorithmic or execution theorem must specify:

1. the input matrices or generating formulas and their exact arithmetic representation;

2. every needed positivity, rank, support, or geometric promise;

3. output format, bit precision, and normalization;

4. computational cost and termination conditions;

5. whether the task is generating a matrix, verifying a certificate, measuring a witness, or classifying an arbitrary input.

A finite formula can specify a large object without any program in the release having instantiated it.

Family 283's target-dependent oracle, Family 281's energy approximation, En02-B's decoder, and Landmark I's readout do not supply those missing objects. The representability/production split in Oai265-A is an appropriate comparison, not an algorithmic premise CheungOai265A,ComparisonDossier.

Assume $0<ϵ\le 1$ and let $\hat{W}$ be as above. Its spectrum is contained in $[-ϵ,1-ϵ]$, with zero on the unused corner complement. Thus

is an effect. Every normalized separable state obeys

whereas the target normalized Choi state obeys

A finite test specifies:

1. a preparation of the identified normalized Choi state;

2. the effect $H$, its implementation, and a complete outcome alphabet retaining failures;

3. independent attempted runs and a predeclared bounded score in $[0,1]$;

4. preparation and measurement allowances on the same complete comparison interface.

No success-only postselection, unpriced apparatus memory, or access to an unprepared Eve system is assumed.

Under Specification spec:experiment, let $\hat{p}$ be the mean of $N$ independent scores. If the actual expectation differs from the intended $\mathrm{Tr}(H\omega )$ by at most $b$, then, with probability at least $1-\alpha$,

If this upper endpoint is below $ϵ$, the intended $\omega$ is entangled.

More generally, if the actual separable-null mean is at least $ϵ-b_0$, and a named target-family mean is at most $ϵ-g+b_1$, put

For $g_{\ast }>0$, the midpoint test has each error at most

Thus

is sufficient for each error to be at most $\alpha$.

Proof. Hoeffding's inequality for independent observations in $[0,1]$ gives the confidence radius Hoeffding. The separable expectation bound proves the certification rule. For the two-family comparison, the midpoint is separated from either allowed mean by at least $g_{\ast }/2$. The one-sided Hoeffding bound is $e^{-2N(g_{\ast }/2{)}^2}$.

This is the bounded-statistic architecture used in En01-C and related Cheung certificates, on a different declared observable CheungEn01C,CheungEn01B. It is not an asserted laboratory calibration or a rerun of an external script.

For a normalized PPT state $\sigma$ on ${\mathbb{C}}^d\otimes {\mathbb{C}}^d$,

Proof. If $S$ is the swap operator, then

Since ${\sigma }^{T_B}⪰0$, $\mathrm{Tr}{\sigma }^{T_B}=1$, and $S⪯I$,