% Oai272-A.tex % Single-file manuscript intended for pdfLaTeX. % No external bibliography, figures, custom class, or shell escape. % % Suggested build commands; not executed in this response: % pdflatex -interaction=nonstopmode -halt-on-error Oai272-A.tex % pdflatex -interaction=nonstopmode -halt-on-error Oai272-A.tex % % RELEASE SCOPE: % The locally proved results are certificate, reduction, and separation % theorems. The dimension-ten geometric/arithmetic construction in the % external Family 272 paper is not independently verified here. % In particular, the manuscript does not present an unverified catalogue % assertion or a Lean statement containing "sorry" as a checked theorem. \documentclass[11pt]{article} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{lmodern} \usepackage[margin=1in]{geometry} \usepackage{amsmath,amssymb,amsthm,mathtools,mathrsfs} \usepackage{array,booktabs,longtable,tabularx} \usepackage{enumitem} \usepackage{microtype} \usepackage{url} \usepackage[hidelinks]{hyperref} \setlength{\emergencystretch}{3em} \setlist[enumerate]{topsep=5pt,itemsep=3pt} \setlist[itemize]{topsep=5pt,itemsep=3pt} \Urlmuskip=0mu plus 1mu \allowdisplaybreaks \numberwithin{equation}{section} \newtheorem{theorem}{Theorem}[section] \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \newtheorem{specification}[theorem]{Specification} \newtheorem{record}[theorem]{Documentary record} \newtheorem{target}[theorem]{Remaining verification target} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newtheorem{example}[theorem]{Example} \newcommand{\C}{\mathbb C} \newcommand{\R}{\mathbb R} \newcommand{\Q}{\mathbb Q} \newcommand{\N}{\mathbb N} \newcommand{\B}{\mathcal B} \newcommand{\Mat}[1]{M_{#1}(\C)} \newcommand{\Tr}{\operatorname{Tr}} \newcommand{\id}{\operatorname{id}} \newcommand{\Ad}{\operatorname{Ad}} \newcommand{\ran}{\operatorname{ran}} \newcommand{\rank}{\operatorname{rank}} \newcommand{\supp}{\operatorname{supp}} \newcommand{\diag}{\operatorname{diag}} \newcommand{\E}{\mathbb E} \newcommand{\Prob}{\mathbb P} \newcommand{\T}{\mathsf T} \newcommand{\ket}[1]{|#1\rangle} \newcommand{\bra}[1]{\langle#1|} \newcommand{\kb}[2]{|#1\rangle\langle#2|} \newcommand{\ddia}{d_{\diamond}} \newcommand{\dtr}{d_{\mathrm{tr}}} \newcommand{\TV}{d_{\mathrm{TV}}} \newcommand{\Sep}{\operatorname{Sep}} \newcommand{\KD}{K_D} \newcommand{\CP}{\mathrm{CP}} \newcommand{\PPT}{\mathrm{PPT}} \newcommand{\EB}{\mathrm{EB}} \newcommand{\NOTCLOSED}{\texttt{NOT\_CLOSED}} \title{\textbf{Oai272-A}\\ Finite Certificates for Secret-Bit Obstructions\\ and PPT-Composition Counterexample Interfaces\\[3pt] \large A source-qualified proof, audit, and separation manuscript} \author{Development manuscript prepared for mathematical review} \date{14 October 2026} \begin{document} \maketitle \begin{abstract} 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 \texttt{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. \end{abstract} \tableofcontents \section{Scope, provenance, and the three distinct claims} \label{sec:scope} \subsection{What this manuscript completes} The supplied plan has stages \(0\)--\(6\). Its mathematical completion must distinguish: \begin{enumerate} \item a locally proved implication; \item an explicit finite certificate for that implication; \item verification that particular external matrices satisfy its hypotheses; \item an experimental or computational execution. \end{enumerate} None of these categories substitutes for another. The principal locally proved results are Theorems~\ref{thm:bit-gap}, \ref{thm:rational-gap}, \ref{thm:completion}, \ref{thm:witness-algorithm}, and \ref{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 \cite{OpenAI272}. The companion identification page distinguishes that source from Cheung's programme \cite{Companion272}. This development uses the requested identifier Oai272-A. It does not assert authorship, registration, approval, or endorsement of this development by N.~Cheung. \subsection{Frozen external records} \begin{record}[The state and secret-key assertion] \label{rec:state} The external paper asserts an explicit entangled density operator \[ \rho\in\Mat{10}\otimes\Mat{10} \] 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 \cite{OpenAI272}. \end{record} \begin{record}[The two-map assertion] \label{rec:pair} The source specifies PPT maps \[ \Phi_1,\Phi_2:\Mat{10}\longrightarrow\Mat{10}, \] without requiring trace preservation, and asserts that \[ Z=J(\Phi_2\Phi_1)\ne0, \qquad \ran Z\text{ contains no nonzero product vector}. \] Its state is \(\rho=Z/\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 \cite{OpenAI272}. \end{record} \begin{record}[The same-channel assertion] \label{rec:channel} A different construction in the source gives a trace-preserving PPT channel \[ \Theta:\Mat{21}\longrightarrow\Mat{21} \] 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 \cite{OpenAI272}. \end{record} 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. \subsection{Corrections established by source inspection} The following distinctions were checked against the publicly accessible source files on 14 October 2026. \paragraph{Comparator 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 \cite{LeanScope}. More strongly, the inspected files end the relevant theorem bodies with \texttt{by sorry}: \[ \texttt{OAI.DimensionTen.main\_pair}, \qquad \texttt{OAI.DimensionTen.exists\_channel\_fin21} \] \cite{LeanPair,LeanChannel}. They specify targets; those bodies are not completed proofs. No Lean execution or independent checking of other repository files is asserted. \paragraph{Two 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 \cite{Supplementary272}. \paragraph{Matrix sizes.} A Choi matrix for a map \(\Mat{10}\to\Mat{10}\) is \(100\times100\). For \(\Mat{21}\to\Mat{21}\), it is \(441\times441\). 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. \paragraph{Eventual 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 \cite{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 \cite{HansonRouzeFranca}. \section{Stage 0: conventions and the operational package} \label{sec:conventions} \subsection{States, maps, and distances} All finite matrix spaces are complex and have fixed orthonormal bases. Transpose \(T_d(X)=X^\T\) is complex-linear. A map \(F:\Mat a\to\Mat b\) is PPT if \(F\) and \(T_bF\) are completely positive. No trace condition is included. We use the unnormalized Choi convention \begin{equation} J(F)=\sum_{i,j=1}^a E_{ij}\otimes F(E_{ij}) =(\id_a\otimes F)(\kb{\Omega_a}{\Omega_a}), \qquad \ket{\Omega_a}=\sum_{i=1}^a\ket{i,i}. \label{eq:choi} \end{equation} A channel has \(\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)/\Tr J(F)\). For states and compatible channels, \[ \dtr(\alpha,\beta)=\frac12\|\alpha-\beta\|_1, \qquad \ddia(F,G)=\frac12\|F-G\|_\diamond. \] The diamond norm includes an independent reference \cite{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\succeq0\). 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. \subsection{The represented class} \begin{definition}[Represented states] \label{def:C} A density operator \(R\) on \(A\otimes B\) belongs to \(\mathscr C\) if \begin{equation} R=(L\otimes M)(\kb{\chi}{\chi}), \label{eq:C} \end{equation} where \(\chi\) is a finite bipartite vector and \[ L,\quad L T_r,\quad M,\quad M T_s \] 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. \end{definition} This is a mathematical representation, not a supplied physical implementation of \(L\) and \(M\). \begin{lemma}[Elementary PPT stability and tensor closure] \label{lem:stability} For a CP map \(F:\Mat a\to\Mat b\), its adjoint and \(T_bFT_a\) are CP. Moreover, \[ FT_a\text{ is CP}\quad\Longleftrightarrow\quad T_bF\text{ is CP}. \] Adjoints and transpose-adjoints of PPT maps are PPT. Every state in \(\mathscr C\) is PPT, and \(\mathscr C\) is closed under finite tensor products after grouping the parties. \end{lemma} \begin{proof} If \(F(X)=\sum_\alpha K_\alpha X K_\alpha^\dagger\), then \[ F^\dagger(Y)=\sum_\alpha K_\alpha^\dagger YK_\alpha, \qquad T_bFT_a(X)=\sum_\alpha\overline K_\alpha X\overline K_\alpha^\dagger . \] These formulas prove the CP assertions and the equivalence. Taking adjoints proves the transpose-adjoint statements. For \eqref{eq:C}, \[ R^{T_A}=((T_A L)\otimes M)(\kb{\chi}{\chi})\succeq0. \] 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. \end{proof} 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 \cite{HHHO2005,HHHO2009}. \subsection{Admitted complete-history protocols} The following operational requirements make explicit the model used in the local proof. They preserve the source's relevant resource and complete-history distinctions \cite{OpenAI272,CLMOW}. \begin{specification}[Local instruments and complete public information] \label{spec:protocol} An admitted protocol has finite-dimensional bipartite input \(A\otimes B\), local quantum memories and local CP instruments, and classical public communication. It satisfies: \begin{enumerate}[label=\textup{(P\arabic*)}] \item 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. \item 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. \item 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. \item 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\). \item 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. \item 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. \item 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. \end{enumerate} Eve retains the original purification and the complete public transcript, not private instrument labels merely used inside a laboratory. \end{specification} 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 \cite{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, \[ \|H\|_1=\int\|H(t)\|_1\,d\mu(t). \] This norm is independent of the dominating measure. \section{Stage 1: the operational certificate} \label{sec:operational} \subsection{A four-effect inequality} \begin{lemma}[Positive block estimate] \label{lem:block} If \[ \begin{pmatrix}H&Z\\Z^\dagger&K\end{pmatrix}\succeq0, \] then \[ \|Z\|_1\le\sqrt{\Tr H\,\Tr K}. \] \end{lemma} \begin{proof} Write the block matrix as \(\sum_\alpha\binom{u_\alpha}{v_\alpha} \binom{u_\alpha}{v_\alpha}^{\dagger}\). Then \[ \|Z\|_1 \le\sum_\alpha\|u_\alpha\|\|v_\alpha\| \le \left(\sum_\alpha\|u_\alpha\|^2\right)^{1/2} \left(\sum_\alpha\|v_\alpha\|^2\right)^{1/2}. \] \end{proof} \begin{lemma}[Four-effect certificate] \label{lem:four} Let \(R\in\mathscr C\), and let \(X_0,X_1,Y_0,Y_1\succeq0\). Put \[ D_{ij}=X_i\otimes Y_j,\qquad p_{ij}=\Tr(D_{ij}R). \] Then \begin{equation} \|\sqrt{D_{00}}R\sqrt{D_{11}}\|_1 \le \sqrt{p_{00}p_{01}} +\sqrt{p_{10}p_{11}} +2\sqrt{p_{01}p_{10}}. \label{eq:four} \end{equation} No POVM normalization of the four local matrices is required. \end{lemma} \begin{proof} Choose \eqref{eq:C}, and write \[ A_i=L^\dagger(X_i),\qquad B_j=M^\dagger(Y_j). \] First make the \(A_i\) commute by a change of representation. For \(H=A_0+A_1\), let \(S\) equal \(H^{-1/2}\) on \(\ran H\) and the identity on \(\ker H\). Replace \[ L\ \longmapsto\ L\Ad_S,\qquad \chi\ \longmapsto\ (S^{-1}\otimes I)\chi . \] The output is unchanged. The new pullbacks sum to the support projection of \(H\), so they commute. The PPT condition persists because \[ \Ad_S T=T\Ad_{\overline S}. \] Suppress the new notation, set \(C=L\otimes M\), and define \[ p_{ij}(u)=\langle u,(A_i\otimes B_j)u\rangle, \qquad Z(u,v)=\sqrt{D_{00}}C(\kb uv)\sqrt{D_{11}}. \] Applying Lemma~\ref{lem:block} to \(C\), and then to the CP map \(C(T_r\otimes T_s)\), gives \begin{equation} \|Z(u,v)\|_1 \le \min\left\{ \sqrt{p_{00}(u)p_{11}(v)}, \sqrt{p_{00}(v)p_{11}(u)} \right\}. \label{eq:two-block} \end{equation} 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 \[ u=(P\otimes I)\chi,\qquad v=((I-P)\otimes I)\chi . \] The pullback cross terms vanish, and \[ p_{ij}=p_{ij}(u)+p_{ij}(v),\qquad p_{11}(u)\le p_{01}(u),\qquad p_{00}(v)\le p_{10}(v). \] Equation~\eqref{eq:two-block} bounds the four terms in the expansion of \(C(\kb{\chi}{\chi})\), respectively, by \[ \sqrt{p_{00}p_{01}},\quad \sqrt{p_{10}p_{01}},\quad \sqrt{p_{10}p_{01}},\quad \sqrt{p_{10}p_{11}}. \] The triangle inequality proves \eqref{eq:four}. No inverse of an output state or effect was used. \end{proof} The source identifies \eqref{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 \cite{OpenAI272}. \subsection{Complete transcripts and common local factors} Fix a density \(R\) on \(A\otimes B\), and use the canonical purification \begin{equation} \ket{\Psi_R} =\sum_h\sqrt R\ket h_{AB}\ket h_E, \qquad E\simeq A\otimes B. \label{eq:canonical} \end{equation} \begin{theorem}[Common factors at the complete public transcript] \label{thm:transcript} For a completed bit-output protocol satisfying Specification~\ref{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 \begin{equation} \tau_{ij}(t) = \bigl(\sqrt R[X_i(t)\otimes Y_j(t)]\sqrt R\bigr)^\T, \qquad i,j\in\{0,1\}, \label{eq:transcript} \end{equation} outside a single null set. The same two local pairs work in all four branches, and \[ \sum_{i,j}\int\Tr\tau_{ij}(t)\,d\mu(t)=1. \] \end{theorem} \begin{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 \eqref{eq:canonical} gives \eqref{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 \[ \ket{\Phi_a}_{AA_0}\otimes\ket{\Phi_b}_{BB_0}, \qquad \ket{\Phi_d}=d^{-1/2}\sum_r\ket{r,r}. \] 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 \cite{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 \[ \E[v(V)\mid\sigma(U)\vee\mathcal F_m] =\E[v(V)\mid\mathcal F_m]. \] 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 \[ \E[u(U)v(V)\mid T] = \E[u(U)\mid T]\E[v(V)\mid T]. \] 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 \[ \mu(S)=\sum_{i,j}\Tr W_{ij}(S). \] Entrywise Radon--Nikodym derivatives yield positive densities \(W_{ij}(t)\). Set \[ U_i(t)=\sum_j\Tr_{B_0}W_{ij}(t),\qquad V_j(t)=\sum_i\Tr_{A_0}W_{ij}(t). \] The conditional product law of the informationally complete tests gives \[ \Tr[(E_r\otimes G_s)W_{ij}(t)] = \Tr(E_rU_i(t))\Tr(G_sV_j(t)). \] Since \(E_r\otimes G_s\) span the Hermitian matrices, \[ W_{ij}(t)=U_i(t)\otimes V_j(t) \] simultaneously for all branches. Finally apply the algebraic reference filter \[ K=\sqrt{ab}\,(\sqrt R)^\T. \] Acting on the auxiliary product probes, it prepares exactly \eqref{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 \(KW_{ij}K^\dagger\). 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 \[ X_i(t)=aU_i(t)^\T,\qquad Y_j(t)=bV_j(t)^\T \] gives \eqref{eq:transcript}. Normalization follows from completion. The filter need not be a physical operation and no inverse of \(R\) is required. \end{proof} 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. \subsection{Fidelity at singular and unnormalized blocks} For positive matrices define root fidelity by \[ f(H,K)=\|\sqrt H\sqrt K\|_1. \] This is not squared fidelity. \begin{lemma}[Finite fidelity identities] \label{lem:fidelity} For square matrices \(A,B\), \[ f(A^\dagger A,B^\dagger B)=\|AB^\dagger\|_1. \] For positive \(H,K\), \begin{equation} f(H,K)\ge \frac{\Tr H+\Tr K-\|H-K\|_1}{2}. \label{eq:fidelity-lower} \end{equation} Also \(f(H^\T,K^\T)=f(H,K)\). \end{lemma} \begin{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 \eqref{eq:fidelity-lower}, put \(A=\sqrt H\), \(B=\sqrt K\), \(D=A-B\). Since \(H-K=AD+DB\), trace-norm duality gives \[ \|H-K\|_1\ge\Tr\bigl(|D|(A+B)\bigr). \] On a unit eigenvector of \(D\) with eigenvalue \(d\), positivity gives \(\langle A+B\rangle\ge|d|\). Thus \[ \|H-K\|_1 \ge\Tr D^2 =\Tr H+\Tr K-2\Tr(AB) \ge\Tr H+\Tr K-2f(H,K). \] \end{proof} The normalized version is a standard trace-distance/fidelity comparison \cite{FuchsVanDeGraaf}; the displayed proof fixes the unnormalized convention needed here. \section{The uniform gap and its exact finite certificate} \label{sec:gap} \subsection{A certificate stated independently of a state construction} \begin{definition}[Transcript-coherence certificate] \label{def:TC} 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 \[ P_{ij}=\int\Tr\tau_{ij}(t)\,d\mu(t),\qquad \sum_{i,j}P_{ij}=1, \] and \begin{equation} \mathfrak f:= \int f(\tau_{00}(t),\tau_{11}(t))\,d\mu(t) \le \sqrt{P_{00}P_{01}} +\sqrt{P_{10}P_{11}} +2\sqrt{P_{01}P_{10}}. \label{eq:TC} \end{equation} \end{definition} 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. \begin{lemma}[Represented inputs supply the certificate] \label{lem:Ccertificate} For \(R\in\mathscr C\), every completed bit protocol of Specification~\ref{spec:protocol}, with Eve's canonical purification, satisfies Definition~\ref{def:TC}. \end{lemma} \begin{proof} Use Theorem~\ref{thm:transcript}. The fidelity identities give \[ f(\tau_{00}(t),\tau_{11}(t)) = \|\sqrt{D_{00}(t)}R\sqrt{D_{11}(t)}\|_1 . \] Apply Lemma~\ref{lem:four} pointwise and scalar Cauchy--Schwarz to each integral. \end{proof} \begin{definition}[Ideal key and distance] \label{def:key} For a normalized Eve law \(\sigma_{ET}\), define \[ \gamma^{(\ell)}_\sigma = 2^{-\ell}\sum_{z\in\{0,1\}^{\ell}} \kb{z,z}{z,z}\otimes\sigma_{ET}. \] For a bit output \(\tau\), write \[ \eta(\tau,\sigma)=\|\tau-\gamma^{(1)}_\sigma\|_1. \] A secure fixed-length key-distillation sequence has lengths \(\ell_n\ge0\) and comparison laws \(\sigma_n\) such that \[ \|\tau_n-\gamma^{(\ell_n)}_{\sigma_n}\|_1\longrightarrow0. \] Its lower asymptotic rate is \(\liminf_n\ell_n/n\). The corresponding \(\KD\) is the supremum over admitted secure sequences, including the empty-key sequence. \end{definition} This is the purification-and-public-transcript security task, not quantum recovery from a classical record \cite{HHHO2009,CheungI,CheungHawk04B}. \begin{theorem}[Uniform secret-bit obstruction] \label{thm:bit-gap} Every normalized output with a transcript-coherence certificate obeys \begin{equation} \|\tau-\gamma^{(1)}_\sigma\|_1\ge\frac15 \label{eq:gap} \end{equation} for every normalized comparison law \(\sigma\). Consequently, if \(R\in\mathscr C\), the same bound holds for every \(n\ge1\) and every completed protocol on \(R^{\otimes n}\) satisfying Specification~\ref{spec:protocol}. It holds for every initial purification retained by Eve, and \(\KD(R)=0\) for this model. \end{theorem} \begin{proof} Use a common dominating measure for the actual transcript law and the ideal comparison law. This retains their singular parts. Homogeneity preserves \eqref{eq:TC}. Set \[ e=P_{01}+P_{10}, \] \[ q=\int\|\tau_{00}(t)-\tau_{11}(t)\|_1\,d\mu(t), \] \[ a_i=\int\|\tau_{ii}(t)-\sigma(t)/2\|_1\,d\mu(t). \] The classical bit blocks give \begin{equation} \eta=e+a_0+a_1,\qquad q\le a_0+a_1=\eta-e. \label{eq:linked} \end{equation} The total trace deficit in the two matching blocks is \(e\); hence \(a_0+a_1\ge e\), so \begin{equation} \eta\ge2e. \label{eq:eta2e} \end{equation} Lemma~\ref{lem:fidelity} also gives \[ \mathfrak f \ge\frac{1-e-q}{2} \ge\frac{1-\eta}{2}, \] or \begin{equation} \eta\ge1-2\mathfrak f. \label{eq:etaf} \end{equation} Cauchy--Schwarz and the arithmetic--geometric mean inequality simplify \eqref{eq:TC} to \begin{equation} \mathfrak f\le \sqrt{e(1-e)}+e. \label{eq:scalar-upper} \end{equation} If \(e\ge1/10\), \eqref{eq:eta2e} proves \eqref{eq:gap}. If \(0\le e\le1/10\), then \[ e(1-e)\le\frac9{100}, \qquad \mathfrak f\le\frac3{10}+\frac1{10}=\frac25. \] Equation~\eqref{eq:etaf} again proves \eqref{eq:gap}. For \(R^{\otimes n}\), tensor closure and Lemma~\ref{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\ge1\) for infinitely many \(n\). Its lengths are eventually zero, and its rate is zero. The empty key attains zero rate. \end{proof} 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. \subsection{The rational terminal certificate} \begin{theorem}[Exact finite certificate for the constant \(1/5\)] \label{thm:rational-gap} The scalar constraints \[ 0\le e\le1,\qquad \eta\ge2e,\qquad \eta\ge1-2f,\qquad f\le\sqrt{e(1-e)}+e \] imply \(\eta\ge1/5\). The numerical proof requires only the rational identity \begin{equation} \frac9{100}-e(1-e) = \left(\frac1{10}-e\right) \left(\frac9{10}-e\right) \label{eq:rational-certificate} \end{equation} on \(0\le e\le1/10\), together with a split at \(e=1/10\). The constant \(1/5\) is optimal for this scalar relaxation: \[ (e,f,\eta)=\left(\frac1{10},\frac25,\frac15\right) \] satisfies all four scalar constraints. This does not assert attainability by a physical state or protocol. \end{theorem} \begin{proof} For \(e\ge1/10\), use \(\eta\ge2e\). Otherwise the two factors on the right of \eqref{eq:rational-certificate} are nonnegative. Thus \(f\le3/10+1/10=2/5\), and \(\eta\ge1-2f\ge1/5\). The displayed equality tuple proves the relaxation statement. \end{proof} 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~\ref{thm:transcript}, Lemma~\ref{lem:four}, and tensor closure; the constant itself needs no enormous matrix. \begin{proposition}[A priced coherence defect] \label{prop:defect} If the same normalized output instead satisfies \[ \mathfrak f\le\sqrt{e(1-e)}+e+\kappa, \qquad \kappa\ge0, \] then \[ \eta\ge\max\{0,1/5-2\kappa\}. \] \end{proposition} \begin{proof} The case \(e\ge1/10\) gives \(\eta\ge1/5\). For \(e\le1/10\), the upper bound is \(\mathfrak f\le2/5+\kappa\), while \(\eta\ge1-2\mathfrak f\). \end{proof} 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. \section{Conditioning, implementation error, and protocol restrictions} \label{sec:extensions} \begin{proposition}[Public conditioning and aborts] \label{prop:conditioning} For the outputs in Theorem~\ref{thm:bit-gap}: \begin{enumerate} \item Conditioning on a measurable public-transcript event with probability \(r>0\) preserves the \(1/5\) gap for the normalized accepted output. \item If a completed output includes local abort symbols with joint abort probability \(a<1\), and \(\eta_{\rm ok}\) is its normalized non-aborting distance from an ideal bit on a common Eve interface, then \[ (1-a)\eta_{\rm ok}+2a\ge\frac15. \] In particular, vanishing abort probability cannot coexist with vanishing non-aborting key error. \end{enumerate} \end{proposition} \begin{proof} For (1), restrict the transcript measure to the public event and divide every branch density by \(r\). In \eqref{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_{\rm ok}+2a\), since the distance between normalized states in unhalved trace norm is at most two. Apply Theorem~\ref{thm:bit-gap}. \end{proof} \begin{proposition}[Complete-interface robustness] \label{prop:robust} Suppose a certified ideal output has gap \(1/5-2\kappa\), and an implemented output on the same bit--Eve interface satisfies \[ \dtr(\widehat\tau,\tau)\le b. \] Then its distance from every ideal bit obeys \[ \dtr(\widehat\tau,\gamma^{(1)}_\sigma) \ge \max\{0,1/10-\kappa-b\}. \] Compatible stepwise half-diamond allowances \(b_1,\ldots,b_m\) give the valid choice \(b\le\min\{1,\sum_jb_j\}\). \end{proposition} \begin{proof} Use the triangle inequality and telescope compatible channel compositions. Pre- and postcomposition by channels contract diamond distance. \end{proof} The comparison interface must retain Eve's purification and all public information. A comparison only on Alice's selected bit is not sufficient. \begin{example}[Dropping the public record manufactures apparent secrecy] Let \[ \tau=\frac12\sum_{i=0}^1 \kb{i,i}{i,i}_{K_AK_B}\otimes\kb ii_T. \] Discarding \(T\) gives a perfect uniform correlated bit. With \(T\) retained, however, \[ \inf_\sigma\|\tau-\gamma^{(1)}_\sigma\|_1=1. \] 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. \end{example} \begin{proposition}[Restriction is not a new impossibility theorem] \label{prop:restrictions} A uniform obstruction proved for a protocol class also holds for every subclass. In particular, the zero-key conclusion of Theorem~\ref{thm:bit-gap} implies zero one-way key and zero key under any fixed communication budget within that model. \end{proposition} \begin{proof} The same lower bound applies to each member of the smaller class. Equivalently, optimizing a rate over fewer protocols cannot increase it. \end{proof} 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. \section{Choi transfer and product-free range} \label{sec:choi} \begin{lemma}[Choi separability and entanglement breaking] \label{lem:choiEB} A CP map \(F\) is entanglement breaking if and only if \(J(F)\) is separable. This equivalence does not require trace preservation. \end{lemma} \begin{proof} If \(J(F)\) is separable, refine its positive factors spectrally: \[ J(F)=\sum_\alpha \kb{a_\alpha}{a_\alpha}\otimes \kb{b_\alpha}{b_\alpha}. \] Comparison of matrix-unit blocks gives \[ F(X)=\sum_\alpha \Tr\!\left[(\kb{a_\alpha}{a_\alpha})^\T X\right] \kb{b_\alpha}{b_\alpha}. \] On a positive referenced input this is a sum of positive product operators. Conversely, apply the defining entanglement-breaking property to \(\kb{\Omega_a}{\Omega_a}\). \end{proof} This is the standard measure-and-prepare characterization \cite{HSR2003}; the CP and matrix-unit conventions are fixed by the Choi correspondence \cite{Choi1975,Watrous}. \begin{lemma}[Product-free range is a sufficient witness] \label{lem:range} Every nonzero separable positive matrix has a nonzero product vector in its range. Hence a nonzero positive matrix with product-free range is entangled. \end{lemma} \begin{proof} Write a separable positive matrix as \(Z=\sum_\alpha\kb{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=\ran Z\). At least one is nonzero. \end{proof} Only this sufficient failure of a necessary separability condition is used. It is not an equivalence \cite{HorodeckiRange}. \begin{lemma}[Transpose-adjoint Choi transfer] \label{lem:transfer} For CP maps \(F:\Mat a\to\Mat b\) and \(G:\Mat b\to\Mat c\), define \[ F^\sharp=T_aF^\dagger T_b. \] Then \begin{equation} J(GF)=(F^\sharp\otimes G)(\kb{\Omega_b}{\Omega_b}). \label{eq:transfer} \end{equation} If both maps are PPT and \(Z=J(GF)\ne0\), then \[ \frac Z{\Tr Z} = (F^\sharp\otimes G) \left(\frac{\kb{\Omega_b}{\Omega_b}}{\Tr Z}\right) \in\mathscr C. \] \end{lemma} \begin{proof} For Kraus matrices \(A_r\) of \(F\) and \(B_s\) of \(G\), the Kraus matrices of \(F^\sharp\) are \(A_r^\T\), and \[ (A_r^\T\otimes B_s)\ket{\Omega_b} =(I_a\otimes B_sA_r)\ket{\Omega_a}. \] Sum their rank-one projectors to prove \eqref{eq:transfer}. Lemma~\ref{lem:stability} supplies the four CP conditions. Finally \(\Tr Z>0\) because \(Z\) is positive and nonzero. \end{proof} The identity is also part of the established PPT-composition framework \cite{CMHW2019}. The normalization is by the actual Choi trace, with no additional factor \(b\). \begin{corollary}[Conditional zero-key entangled-state construction] \label{cor:state} If PPT maps \(F,G\) have nonzero \(Z=J(GF)\) with product-free range, then \(Z/\Tr Z\) is an entangled PPT state with zero distillable key for Specification~\ref{spec:protocol}, and every completed bit protocol has the \(1/5\) gap. \end{corollary} \begin{proof} Apply Lemmas~\ref{lem:range} and \ref{lem:transfer}, then Theorem~\ref{thm:bit-gap}. \end{proof} The external dimension-ten arithmetic must establish the hypotheses of this corollary. The corollary does not establish those hypotheses by referring to the catalogue. \section{The channel-completion interface} \label{sec:completion} \begin{theorem}[A PPT pair gives a \(2d+1\)-dimensional channel] \label{thm:completion} Let \(F,G:\Mat d\to\Mat d\) be PPT. There are explicit \(s,t>0\) and a trace-preserving PPT channel \(\Theta:\Mat{2d+1}\to\Mat{2d+1}\) whose squared Choi matrix has a coordinate-local corner equal to \(stJ(GF)\). If \(J(GF)\) is entangled, \(\Theta^2\) is not entanglement breaking. \end{theorem} \begin{proof} Set \[ A=F^\dagger(I),\quad B=G^\dagger(I),\qquad s=\frac1{1+\Tr A},\quad t=\frac1{1+\Tr B}, \] \[ D=I-sA,\qquad E=I-tB. \] Since \(A,B\succeq0\), \[ D\succeq sI\succ0,\qquad E\succeq tI\succ0. \] Use the real coordinate inclusions \(V_0,V_1\) in \[ \C^{2d+1}=\C^d_0\oplus\C^d_1\oplus\C\ket\star, \qquad P_\star=\kb\star\star. \] Write \(X_{jj}=V_j^\dagger XV_j\). Define \begin{align} \Theta(X) ={}&sV_1F(X_{00})V_1^\dagger +tV_0G(X_{11})V_0^\dagger \notag\\ &+\left[ \Tr(DX_{00})+\Tr(EX_{11}) +\bra\star X\ket\star \right]P_\star . \label{eq:completion} \end{align} 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_dF,T_dG\) 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\Mat d\), \[ V_0^\dagger\Theta^2(V_0YV_0^\dagger)V_0=st\,GF(Y). \] Expanding in input matrix units gives \begin{equation} (V_0^\dagger\otimes V_0^\dagger) J(\Theta^2)(V_0\otimes V_0)=stJ(GF). \label{eq:corner} \end{equation} Local compression preserves separability. Therefore a separable \(J(\Theta^2)\) would force separability of its entangled corner, a contradiction. \end{proof} This switch-and-flag mechanism has precedents in PPT-composition and trace-decreasing-map completion \cite{CMHW2019,Filippov2021}. It is proved here for the stated interface rather than inferred from a channel-synthesis template. \begin{remark}[The reference inclusion must be conjugated correctly] For general complex input and output isometries \(W,V\), \[ J\bigl(Y\mapsto V^\dagger\Gamma(WYW^\dagger)V\bigr) = (W^\T\otimes V^\dagger) J(\Gamma)(\overline W\otimes V). \] The real coordinate inclusions in \eqref{eq:corner} remove this otherwise important distinction. \end{remark} \begin{remark}[Product-free range belongs to the corner] 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. \end{remark} \begin{proposition}[Second-iterate failure need not persist forever] \label{prop:cube} Assume a PPT pair \(F,G:\Mat d\to\Mat d\) has entangled \(J(GF)\). There is a trace-preserving PPT channel \(\Xi:\Mat{3d+1}\to\Mat{3d+1}\) such that \[ \Xi^2\text{ is not entanglement breaking}, \qquad \Xi^3(X)=\Tr(X)P_\star. \] \end{proposition} \begin{proof} Replace the two-block cycle in \eqref{eq:completion} by the acyclic transitions \[ \C^d_0\xrightarrow{sF}\C^d_1 \xrightarrow{tG}\C^d_2 \xrightarrow{\Tr(\cdot)P_\star}\C\ket\star. \] 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 \(\Tr X\). \end{proof} 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. \section{Stage 2: what local resource and recovery certificates price} \label{sec:templates} \subsection{A readout obstruction is not a key obstruction} \begin{proposition}[Sharp record-only quantum-recovery bound] \label{prop:record} Let \(\dim Q=d\ge2\). If the only input-dependent accessible output is a classical measurement record, then every quantum decoder implements an entanglement-breaking channel \(\Lambda\), and \[ \ddia(\Lambda,\id_Q)\ge1-\frac1d. \] Basis measurement followed by basis-state preparation attains the bound. \end{proposition} \begin{proof} The decoded channel has the form \[ \Lambda(X)=\sum_z\Tr(E_zX)\sigma_z. \] Its Bell-input output is separable. For normalized product states, \[ \bra{\Phi_d}\alpha\otimes\beta\ket{\Phi_d} =\frac1d\Tr(\alpha^\T\beta)\le\frac1d. \] 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\). \end{proof} This is the finite distinction emphasized in Cheung's Landmark I, VIII-B, and Hawk04-B \cite{CheungI,CheungVIIIB,CheungHawk04B}. It does not apply when an authorized input-dependent quantum memory is also retained. \begin{example}[The retained-memory exception is real] The channel \[ X\longmapsto\kb00_{\rm record}\otimes X_{\rm memory} \] has a constant selected record and exact recovery from the retained memory. Replacing it by a record-only interface changes the task. \end{example} 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 \cite{HHHO2009}. \subsection{A one-shot resource ledger} \begin{proposition}[One-shot environment accounting] \label{prop:ledger} For a finite instrument \(\{\mathcal A_x\}_x\), let \(r_x=\rank J(\mathcal A_x)\) after zero maps are removed, and \(R_0=\sum_xr_x\). A pure-environment isometric implementation with orthogonal outcome blocks has minimum environment dimension \(R_0\). Its full-readout environment register needs \[ \left\lceil\log_2R_0\right\rceil \] qubits. A prescribed rectangular outcome/index split needs \[ \left\lceil\log_2|\{x:r_x>0\}|\right\rceil + \left\lceil\log_2\max_xr_x\right\rceil. \] \end{proposition} \begin{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. \end{proof} This is the declared one-shot model in En02-A \cite[{\texttt{thm:Dprime}}]{CheungEn02A}. It is not a lower bound on every adaptive peak memory and does not replace \eqref{eq:four}. \subsection{Comparison ledger} \begin{longtable}{@{}p{.24\linewidth}p{.34\linewidth}p{.34\linewidth}@{}} \toprule Component & Permitted role & Non-transfer\\ \midrule \endfirsthead \toprule Component & Permitted role & Non-transfer\\ \midrule \endhead \bottomrule \endfoot En07-A; Hawk04-B & Complete outputs, classical records, and operational discard must be distinguished. & No universal secret-bit obstruction follows from a recovery comparison.\\[4pt] Landmark I; VIII-B & Measure-and-prepare structure and its Bell-reference recovery obstruction. & Not a proof that a specified Choi support is product-free.\\[4pt] En02-A/B/C & Explicit one-shot, streaming, gate, and communication ledgers. & A decoder's memory optimum is not the \(1/5\) fidelity argument.\\[4pt] Oai283-A & Normalization of full-diamond and half-diamond allowances on fixed comparison interfaces. & No classification of PPT maps or entanglement breaking.\\[4pt] Oai265-B; Oai290-A & A named Choi statistic, error-transfer budget, and acceptance, exclusion, or inconclusive decision. & No certification of the external matrices or of every key protocol.\\[4pt] Oai280-C & Reference-stable complete-channel comparison, where its declared model is actually supplied. & Privacy of an erased code subsystem is not automatically a distillable-key rate.\\[4pt] En01-C; En10-B & Bounded complete-record statistics for predeclared families. & A sample interval is not an arithmetic proof or an exhaustive protocol quantifier.\\[4pt] Em03-F & A specified measure-and-prepare channel and its quantum-recovery obstruction. & Not the Family 272 state or its complete key protocol.\\[4pt] Em03-G & Changing the source family can produce a resource-dependent recovery regime. & Receiver postprocessing cannot cancel a fixed uniform obstruction on another source class.\\ \end{longtable} The detailed supplied statements support the first three and the En01-C/Em03 comparisons \cite{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 \cite{ComparisonDossier}. \section{Stage 3: finite witness construction under an exact support promise} \label{sec:witness} \subsection{An entanglement witness, not a separable decomposition} For an entangled corner, the appropriate successor object is a \emph{separating entanglement witness}. A separable decomposition of that same corner cannot be the desired output. \begin{proposition}[A product-free support gives a witness] \label{prop:support-witness} Let \(0\ne Z\succeq0\) on \(\C^a\otimes\C^b\), and let \(P\) be its range projection and \(Q=I-P\). If \(\ran Z\) is product-free, then \[ \delta_*= \min_{\|x\|=\|y\|=1} \langle x\otimes y,Q(x\otimes y)\rangle>0. \] For every \(0<\epsilon\le\delta_*\), \[ W=Q-\epsilon I \] is nonnegative on every positive separable matrix and satisfies \[ \Tr(WZ)=-\epsilon\Tr Z<0. \] \end{proposition} \begin{proof} The product of the two unit spheres is compact. A zero minimum would give a unit product vector in \(\ker Q=\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. \end{proof} \begin{theorem}[An exact finite witness algorithm with a stated promise] \label{thm:witness-algorithm} Suppose \(Z\ne0\) is a positive matrix with entries in \(\Q+i\Q\), and its range is product-free. There is an exact-arithmetic procedure which terminates and outputs rational \(\epsilon>0\) and \[ W=Q-\epsilon I \] as in Proposition~\ref{prop:support-witness}. It supplies a finite rational certificate for global product nonnegativity. No polynomial running-time bound is asserted. \end{theorem} \begin{proof} Gaussian elimination selects a full-column-rank rational matrix \(V\) spanning \(\ran Z\). Therefore \[ P=V(V^\dagger V)^{-1}V^\dagger,\qquad Q=I-P \] have rational complex entries. For integers \(M\ge2(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\preceq Q\preceq I\) gives \[ |q(x,y)-q(x',y')| \le2\bigl(\|x-x'\|+\|y-y'\|\bigr), \] where \(q(x,y)=\langle x\otimes y,Q(x\otimes y)\rangle\). Consequently, with \[ m_M=\min_{\substack{x\in\mathcal N_a(M)\\ y\in\mathcal N_b(M)}}q(x,y), \qquad \epsilon_M=m_M-\frac{4(a+b)}M, \] every unit product vector has \(Q\)-expectation at least \(\epsilon_M\). Each grid expectation is rational. If \(x=g/\|g\|\) and \(y=h/\|h\|\), its value is \[ \frac{\langle g\otimes h,Q(g\otimes h)\rangle} {\|g\|^2\|h\|^2}, \] with rational numerator and denominator. Thus all comparisons are exact. Try successively doubled \(M\) until \(\epsilon_M>0\). Because \(m_M\ge\delta_*>0\), termination follows. For a fixed \(M\), at most \[ \bigl((2M+1)^{2a}-1\bigr) \bigl((2M+1)^{2b}-1\bigr) \] pairs are tested. Their rational values and the Lipschitz allowance certify the global lower bound. The potentially very small unknown \(\delta_*\) prevents a claimed efficient complexity bound. \end{proof} 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. \subsection{Transporting the witness to the channel square} \begin{corollary}[Witness for the completed channel] \label{cor:channel-witness} Under Theorem~\ref{thm:completion}, suppose \(Z=J(GF)\ne0\) has a witness \(W=Q-\epsilon I\) from Proposition~\ref{prop:support-witness}. For \(D=2d+1\), set \[ \widehat W=(V_0\otimes V_0)W(V_0^\dagger\otimes V_0^\dagger). \] Then \(\widehat W\) is nonnegative on the full separable cone and \[ \Tr[\widehat W\,j(\Theta^2)] = -\frac{st\epsilon\Tr Z}{D}=:-g<0. \] \end{corollary} \begin{proof} Compression of a product vector is a product vector, possibly zero. This proves block positivity of \(\widehat W\). Equation~\eqref{eq:corner} gives the expectation and the factor \(1/D\) from normalized Choi convention. \end{proof} \subsection{What ``explicit'' does and does not provide} An algorithmic or execution theorem must specify: \begin{enumerate} \item the input matrices or generating formulas and their exact arithmetic representation; \item every needed positivity, rank, support, or geometric promise; \item output format, bit precision, and normalization; \item computational cost and termination conditions; \item whether the task is generating a matrix, verifying a certificate, measuring a witness, or classifying an arbitrary input. \end{enumerate} 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 \cite{CheungOai265A,ComparisonDossier}. \section{Finite-sample certification and its limitations} \label{sec:statistics} \subsection{A specified entanglement-witness experiment} Assume \(0<\epsilon\le1\) and let \(\widehat W\) be as above. Its spectrum is contained in \([-\epsilon,1-\epsilon]\), with zero on the unused corner complement. Thus \[ H=\widehat W+\epsilon I \] is an effect. Every normalized separable state obeys \[ \Tr(H\sigma)\ge\epsilon, \] whereas the target normalized Choi state obeys \[ \Tr[Hj(\Theta^2)]=\epsilon-g. \] \begin{specification}[Trusted complete-record experiment] \label{spec:experiment} A finite test specifies: \begin{enumerate} \item a preparation of the identified normalized Choi state; \item the effect \(H\), its implementation, and a complete outcome alphabet retaining failures; \item independent attempted runs and a predeclared bounded score in \([0,1]\); \item preparation and measurement allowances on the same complete comparison interface. \end{enumerate} No success-only postselection, unpriced apparatus memory, or access to an unprepared Eve system is assumed. \end{specification} \begin{theorem}[Bounded complete-record certificate] \label{thm:statistics} Under Specification~\ref{spec:experiment}, let \(\widehat p\) be the mean of \(N\) independent scores. If the actual expectation differs from the intended \(\Tr(H\omega)\) by at most \(b\), then, with probability at least \(1-\alpha\), \[ \Tr(H\omega) \le \widehat p+\sqrt{\frac{\log(2/\alpha)}{2N}}+b. \] If this upper endpoint is below \(\epsilon\), the intended \(\omega\) is entangled. More generally, if the actual separable-null mean is at least \(\epsilon-b_0\), and a named target-family mean is at most \(\epsilon-g+b_1\), put \[ g_*=g-b_0-b_1. \] For \(g_*>0\), the midpoint test has each error at most \[ e^{-Ng_*^2/2}. \] Thus \[ N\ge\frac{2}{g_*^2}\log\frac1\alpha \] is sufficient for each error to be at most \(\alpha\). \end{theorem} \begin{proof} Hoeffding's inequality for independent observations in \([0,1]\) gives the confidence radius \cite{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_*/2\). The one-sided Hoeffding bound is \(e^{-2N(g_*/2)^2}\). \end{proof} This is the bounded-statistic architecture used in En01-C and related Cheung certificates, on a different declared observable \cite{CheungEn01C,CheungEn01B}. It is not an asserted laboratory calibration or a rerun of an external script. \subsection{Why a Bell-overlap test is not the required witness} \begin{proposition}[PPT states cannot pass the usual Bell-entanglement test] \label{prop:pptbell} For a normalized PPT state \(\sigma\) on \(\C^d\otimes\C^d\), \[ \bra{\Phi_d}\sigma\ket{\Phi_d}\le\frac1d. \] \end{proposition} \begin{proof} If \(S\) is the swap operator, then \[ (\kb{\Phi_d}{\Phi_d})^{T_B}=S/d. \] Since \(\sigma^{T_B}\succeq0\), \(\Tr\sigma^{T_B}=1\), and \(S\preceq I\), \[ \Tr(\kb{\Phi_d}{\Phi_d}\sigma) =\Tr[(S/d)\sigma^{T_B}]\le1/d. \] \end{proof} Thus a high Bell-overlap memory certificate cannot detect the PPT entanglement at issue. A different separating witness or sufficiently complete tomography is needed. Non-entanglement-breaking behavior is not high-fidelity unknown-state transmission. \subsection{Finite data do not enumerate all key protocols} Theorem~\ref{thm:statistics} concerns one named observable and specified preparations. It does not validate all protocol outputs for every \(n\). For example, if complete single-copy input preparations differ by trace distance at most \(r\), the elementary tensor telescoping bound is \[ \dtr(\widehat\omega^{\otimes n},\omega^{\otimes n}) \le\min\{1,nr\}. \] This does not leave a nonzero uniform gap for all \(n\) at a fixed positive preparation tolerance. If Eve's purification or side information changes, even the complete comparison interface must first be supplied. A finite proof of a universally quantified theorem can use structural lemmas. A finite empirical sample cannot replace those lemmas merely by being called a certificate. \section{Stage 4: hypothesis changes and named-model tests} \label{sec:tests} \subsection{Product-free range is sufficient, not necessary} \begin{example}[An entangled full-range state] For \(1/31/2, \] whereas every separable two-qubit state has Bell overlap at most \(1/2\). This example is not PPT and is not a proposed zero-key state. \end{example} Moreover, product-free range is not a hypothesis of Theorem~\ref{thm:bit-gap}. It is used to prove that the proposed zero-key state is entangled. \begin{proposition}[Separable states illustrate the distinction] \label{prop:separableC} Every finite-dimensional separable density operator belongs to \(\mathscr C\). \end{proposition} \begin{proof} Write \[ R=\sum_{k=1}^m p_k\kb{a_k}{a_k}\otimes\kb{b_k}{b_k} \] with normalized local vectors. Take \[ \chi=\sum_k\sqrt{p_k}\ket{k,k}, \] \[ L(X)=\sum_k X_{kk}\kb{a_k}{a_k}, \qquad M(X)=\sum_k X_{kk}\kb{b_k}{b_k}. \] These measure-and-prepare maps are CP and unchanged by input transpose. Their tensor product kills the off-diagonal terms of \(\kb{\chi}{\chi}\) and gives \(R\). \end{proof} \subsection{Not every entangled state has zero key} \begin{example}[An exact positive-key control] A shared pure Bell pair has a trivial purifying environment. Measuring both halves in the same computational basis gives an exact uniform secret bit, with no communication. Independent Bell pairs give one exact bit per pair. Thus no statement here says that every entangled state has zero key. \end{example} PPT alone also does not imply zero key: the positive-key bound-entanglement constructions of Horodecki, Horodecki, Horodecki, and Oppenheim establish the opposite possibility \cite{HHHO2005,HHHO2009}. The represented-class restriction in Theorem~\ref{thm:bit-gap} is substantive. \subsection{Hypothesis ledger} \begin{longtable}{@{}p{.25\linewidth}p{.36\linewidth}p{.31\linewidth}@{}} \toprule Proposed change & Correct implication & Disposition\\ \midrule \endfirsthead \toprule Proposed change & Correct implication & Disposition\\ \midrule \endhead \bottomrule \endfoot Bound communication or impose one-way discussion & These are subclasses of the frozen protocol model. & The same zero upper bound is inherited; no game-repetition theorem is needed.\\[5pt] Allow extra shared private resources & The initial product-resource rule is removed. & A supplied private bit already changes the task. The theorem does not cover it.\\[5pt] Replace represented class by all PPT states & PPT is weaker than the representing-map hypotheses. & Not justified; positive-key PPT examples prevent a universal zero-key conclusion.\\[5pt] Allow non-PPT inputs & The state class is enlarged. & No result about a non-PPT zero-key state is proved here.\\[5pt] Remove product-free range & The sufficient entanglement certificate is lost. & Zero-key theorem may still apply through \(\mathscr C\); entanglement needs another proof.\\[5pt] Reduce dimensions \(10\) or \(21\) & The external construction is changed. & No minimality or dimension reduction is established.\\[5pt] Replace two different maps by one repeated channel & Trace preservation and map equality are additional requirements. & Use the completion theorem; do not identify the original dimension-ten maps as channels.\\[5pt] Infer failure of every later iterate & A second-iterate statement gives no such implication. & Blocked by logic, Proposition~\ref{prop:cube}, and the separately stated eventual-breaking literature.\\[5pt] Compare Families 265, 273, 276, or 277 & Spatial entropy, bosonic entropy, classical capacity, and game repetition have different operational inputs. & No key-rate or protocol-model transfer is made.\\ \end{longtable} The numbered-family descriptions are documentary comparisons from the supplied plan, not independently proved theorems used in this manuscript \cite{ComparisonDossier}. \section{Stage 5: secrecy, recovery, and gravity remain separate} \label{sec:separation} \begin{definition}[Independent completion of a static record] A finite state/map record may be augmented by preparation dynamics, access maps, emission registers, or geometric data. If no bridge theorem identifies those additions with the record, they are independent completions. A quantity is record-determined only if it is constant across the permitted completions with the comparison interfaces fixed. \end{definition} This is the non-identification discipline used in Oai265-A \cite{CheungOai265A}. \begin{proposition}[Selected data do not identify the relevant channel] \label{prop:selected} For \(C\simeq R\simeq B\simeq\C^d\), the isometries \[ V_0\ket\psi=\ket\psi_R\ket0_B, \qquad V_1\ket\psi=\ket0_R\ket\psi_B \] have identical accessible pure-input spectra, all with entropy zero. The first accessible channel exactly recovers the logical state; the second is constant and cannot do so. \end{proposition} \begin{proof} Their accessible channels are \(\id_C\) and \(X\mapsto\Tr(X)\kb00\). Every pure accessible output has spectrum \((1,0,\ldots,0)\). The first is inverted by identification of \(R,C\); every postprocessing of the second is constant. \end{proof} The proposition concerns quantum recovery, not a computation of the distillable key of an arbitrary state. Selected thermal occupations likewise do not supply Eve's full conditional states or an input-dependent key-distillation channel \cite{CheungEn07C}. \begin{proposition}[An entangled finite state does not identify its generator] \label{prop:generator} A specified finite bipartite density operator and its entanglement properties alone do not establish entanglement generation by a gravitational mediator or exclude a predeclared classical-gravity model. \end{proposition} \begin{proof} The same density operator can be taken as an initial shared preparation, with no mediator in the specified experiment. It can also be obtained by preparing a purification at an ordinary quantum source and distributing its subsystems. Neither completion changes the density operator. Thus its static entanglement data do not specify the input preparation, allowed mediator dynamics, interventions, or classical comparison family. Exclusion of that family requires those additional declarations and a distinguishing prediction. \end{proof} Accordingly: \begin{itemize} \item Hawk03-A's encoded partner algebra is not automatically Eve's purifying register; \item a SWAP transport witness is a declared channel operation, not a secrecy-rate theorem; \item a concurrence calculation for a specified dissipative chain is not a Family 272 protocol analysis; \item a perfect-code decoder and privacy of unauthorized code marginals are not a distillable-key conclusion without a matched purification and access model; \item Em03-F/G's source and packet interfaces are not the dimension-ten state construction; \item a static key obstruction specifies no radiation factor, emission dynamics, horizon, generalized entropy, or gravitational extremization problem. \end{itemize} These are scoped comparisons, not a claim to have inspected or verified every named manuscript \cite{CheungEn02B,CheungEm03F,CheungEm03G,ComparisonDossier}. A temporal radiation-entropy history also requires time-labelled states and accessible factors. Appending a stationary evolution or an unrelated emission process to the same static record makes different temporal completions possible. No Page curve follows from either entanglement or zero key. \section{The five-stage source audit} \label{sec:audit} The external proof architecture is useful, but its components must be audited at their own quantifiers. \begin{longtable}{@{}p{.07\linewidth}p{.35\linewidth}p{.50\linewidth}@{}} \toprule Step & Source interface & Local audit and retained obligation\\ \midrule \endfirsthead \toprule Step & Source interface & Local audit and retained obligation\\ \midrule \endhead \bottomrule \endfoot 1 & Represented class and PPT stability. & Definitions, stability, and tensor closure are proved in Lemma~\ref{lem:stability}. No assumption that every PPT state is represented is made.\\[5pt] 2 & Complete transcripts and a four-effect estimate. & The complete-history model is explicit. Common factors, fidelity normalization, and the rational \(1/5\) terminal certificate are proved locally. Private outcomes are not promoted to public messages.\\[5pt] 3 & Choi transfer and product-range obstruction. & The unnormalized Choi convention, transpose-adjoint identity, and sufficient range test are proved in Section~\ref{sec:choi}.\\[5pt] 4 & Dimension-ten geometry from a map on \(\Mat4\), twenty singular directions, quadratic evaluations, and exact arithmetic. & The source describes this mechanism, but this manuscript does not recompute its elimination, field/Galois arguments, or all required evaluation determinants. This is the remaining external application-verification gate.\\[5pt] 5 & Trace-preserving completion with an entangled local corner. & The generic \(2d+1\) construction is proved. The instance \(d=10\) remains conditional on the qualifying external pair. The full channel Choi range is not asserted product-free.\\ \end{longtable} The twenty-direction and quadratic-evaluation mechanism is attributed to the external paper, not a premise drawn from Cheung's sheets \cite{OpenAI272}. No supplementary integer output is substituted for the missing geometric audit. \section{Stage 6: the single active certificate and the exact handoff} \label{sec:handoff} \subsection{What is completed} The intended next theorem has a finite terminal form: \[ \boxed{ \begin{gathered} \text{complete common-factor transcript law}\\ +\ \text{four-effect inequality} +\ \text{normalized ideal-key comparison}\\ \Longrightarrow\ \|\tau-\gamma^{(1)}_\sigma\|_1\ge1/5. \end{gathered}} \] Theorems~\ref{thm:transcript}, \ref{thm:bit-gap}, and \ref{thm:rational-gap} prove this implication with its model and normalization exposed. The final rational certificate is \eqref{eq:rational-certificate}. This does not require a claim that the supplementary arithmetic appendix proves the entire paper. It also does not require simulation, a tomography interval, or a decoder-memory bound. \begin{target}[External-instance verification of the finite package] \label{target:instance} For the source's specified dimension-ten maps: \begin{enumerate} \item pin the exact source version and complete input data; \item verify their CP and complete-copositivity certificates; \item verify \(Z=J(\Phi_2\Phi_1)\ne0\); \item verify the complete product-free range argument, including every required arithmetic and geometric implication; \item record which checks were proved analytically, recomputed exactly, or left unexecuted. \end{enumerate} Only after these tasks may Corollary~\ref{cor:state} and Theorem~\ref{thm:completion} be instantiated as independently verified claims about those particular matrices. \end{target} This is one application-verification handoff, not a simultaneous opening of dimension minimization, new protocol classes, and failure of eventual entanglement breaking. \subsection{Deferred successors} \begin{longtable}{@{}p{.29\linewidth}p{.63\linewidth}@{}} \toprule Candidate & Missing interface or correction\\ \midrule \endfirsthead \toprule Candidate & Missing interface or correction\\ \midrule \endhead \bottomrule \endfoot Lean proof of the zero-key theorem & A faithful formal model of instruments, complete histories, matrix-valued measures, ideal keys, and the operational quantifiers. The inspected pair/channel targets do not supply it and contain proof placeholders.\\[5pt] Dimension reduction & New maps or channels with complete positivity, range, and normalization certificates. No minimality conclusion is inherited.\\[5pt] Efficient witness production & Theorem~\ref{thm:witness-algorithm} supplies finite termination under an exact support promise, not an efficient complexity bound or an executed Family 272 witness.\\[5pt] One-way/two-way comparison & Both rates are already zero conditional on the same universal obstruction. A different finite-block optimum or assisted resource task must be specified to obtain a nontrivial new comparison.\\[5pt] Failure of eventual entanglement breaking & Does not follow from square failure. It would require a separate claim confronting the stated eventual-breaking theorem in \cite{Park}.\\ \end{longtable} \subsection{Conditional assembly} \begin{theorem}[Oai272-A conditional assembly] \label{thm:assembly} Suppose exact finite PPT maps \(F,G:\Mat d\to\Mat d\) are supplied with certified nonzero product-free \(Z=J(GF)\). Then the locally proved package establishes: \begin{enumerate} \item \(Z/\Tr Z\) is an entangled PPT state in \(\mathscr C\); \item every admitted completed bit protocol on every tensor power has unhalved error at least \(1/5\), and its model-specific distillable key is zero; \item \(GF\) is not entanglement breaking; \item the explicit channel \eqref{eq:completion} is trace preserving and PPT on dimension \(2d+1\), with non-entanglement-breaking square; \item a certified product-support lower bound produces a separating witness for the square's normalized Choi state; \item an independently implemented witness experiment has the finite-confidence conclusions of Theorem~\ref{thm:statistics}. \end{enumerate} The theorem does not supply its own external maps, their geometric certificate, or an experimental implementation. \end{theorem} \begin{proof} Items 1--2 are Lemma~\ref{lem:transfer}, Lemma~\ref{lem:range}, and Theorem~\ref{thm:bit-gap}. Item 3 is Lemma~\ref{lem:choiEB}. Item 4 is Theorem~\ref{thm:completion}. Item 5 is Proposition~\ref{prop:support-witness} and Corollary~\ref{cor:channel-witness}, with Theorem~\ref{thm:witness-algorithm} available on its rational input promise. Item 6 follows only after the additional experimental contract is satisfied. \end{proof} \section{Debugging and release ledger} \label{sec:release} \subsection{Corrections to the proposed reading} \begin{enumerate} \item The number \(1/5\) is an unhalved trace-norm gap; the conventional trace-distance gap is \(1/10\). \item The dimension-ten maps are not silently trace-preserving channels. Normalize their Choi state by \(\Tr Z\). \item The represented-class hypothesis is stronger than merely being PPT. Some PPT states have positive distillable key. \item Common local transcript factors are required simultaneously for all four bit branches. Separate branchwise factorizations without shared local pairs are insufficient. \item A complete public record cannot be replaced by a selected bit, a finite prefix without a justified limit, or a transcript with inconvenient messages removed. \item Completion on the actual input is not completion on the probe input. The positive-filter argument explicitly removes auxiliary defaults. \item Unrestricted joint local processing of copies is retained: tensor closure applies to arbitrary effects on all of each party's copies, not merely product effects across copies. \item Restricting communication preserves an already universal impossibility statement. It does not require a new entangled-game theorem. \item Product-free range certifies entanglement, not the key gap by itself, and it is not necessary for general entanglement. \item The full channel Choi matrix contains product vectors from its absorbing flag. Its entangled corner, not its entire range, certifies non-entanglement-breaking square. \item A Bell-overlap test for recovery cannot witness PPT entanglement. The required separating observable must be specified independently. \item An entanglement witness is not a separable decomposition. The witness algorithm's input promises and non-polynomial cost exposure must be retained. \item The supplementary combinatorial integer checks and the dimension-ten arithmetic certificate are distinct proof components. \item The inspected Comparator statements contain \texttt{sorry}. Their scope note is not evidence of completed formal proofs, and neither statement formalizes \(\KD(\rho)=0\). \item Finite statistical coverage and universal mathematical certification are different evidence types. No finite sample enumerates all copy numbers and protocols. \item A second-iterate counterexample is compatible with later entanglement breaking and supplies no gravitational conclusion. \end{enumerate} \subsection{Stage-by-stage disposition} \begin{longtable}{@{}p{.07\linewidth}p{.48\linewidth}p{.37\linewidth}@{}} \toprule Stage & Completed object & Exact status\\ \midrule \endfirsthead \toprule Stage & Completed object & Exact status\\ \midrule \endhead \bottomrule \endfoot 0 & Three separate external records; protocol, Choi, and distance conventions; formalization split. & Frozen, with proof-placeholder and arithmetic-scope corrections.\\[5pt] 1 & Represented-class algebra, common transcript factors, four-effect inequality, Choi transfer, range test, and generic channel completion. & Local implications proved. External geometric instance not independently verified.\\[5pt] 2 & Resource, recovery, reference, and complete-record pricing interfaces. & Local bounds and comparison ledger supplied; no false premise transfer.\\[5pt] 3 & Finite support-witness procedure and witness transport to the completed channel. & Termination proved under exact promises. No external instance or execution asserted.\\[5pt] 4 & Protocol-subclass monotonicity and named finite counterexamples. & Logical weakenings corrected. No unsupported dimension or non-PPT theorem claimed.\\[5pt] 5 & Static-data, recovery, secrecy, temporal, and gravitational non-identifications. & Scoped separation established; no gravitational test constructed.\\[5pt] 6 & Exact rational \(1/5\) terminal certificate and a conditional assembly theorem. & Finite certificate completed. External-instance verification remains the single handoff.\\ \end{longtable} \subsection{Submission claim} The submission claim is the finite certificate and conditional reduction package proved in this manuscript. It is not an independently verified resolution of the source's entangled-state existence construction merely because the conditional implications are complete. The resulting separation is precise: \[ \boxed{ \begin{gathered} \text{a verified qualifying PPT pair} \Longrightarrow \text{entangled zero-key state in the frozen protocol model},\\ \text{a static entanglement or key record} \not\Longrightarrow \text{a gravitational generator, exclusion test, or entropy history}. \end{gathered}} \] \appendix \section{Source policy and unchanged programme boundaries} Cheung citations identify supplied manuscript versions, excerpts, or explicitly labelled comparison nominations. They are not a comprehensive corpus scan or a reconstructed proof-dependency graph. Locally proved theorems do not become registered Cheung results by using the requested Oai272-A identifier. The supplied IX-Free-2/IX-D, XI-E/F/G, XIV-A/B, and XVI-B/D passages concern different equation spaces, kernels, ghost sectors, response maps, and quantum-admission problems. They are not prerequisites of the finite-dimensional proofs here \cite{AnalyticDossier}. In particular, no result above constructs a time-ordered extension, a characteristic quantum product, an interacting ghost differential, or an admission \[ Q_HR_1^{(1)}\in\mathscr E_H. \] This manuscript does not change any version-specific verdict by replacing its actual hypotheses with a similarly named finite-channel object. \section*{Declarations} \addcontentsline{toc}{section}{Declarations} \paragraph{External source status.} Family 272 is an external OpenAI record. The dimension-ten geometric and arithmetic construction is not independently verified by this manuscript and is not assumed in its local theorems. The companion is not a proof checker. \paragraph{Formalization.} The source-matched scope note and the inspected pair/channel Comparator files were read. Their relevant proof bodies contain \texttt{sorry}. No successful Lean build, completed proof, or secret-key formalization is asserted. \paragraph{Computation and experiment.} No supplementary program, witness search, matrix-generation routine, tomography procedure, or laboratory experiment was executed here. Reported arithmetic outputs in another release are not independent reruns. \paragraph{Compilation.} The source uses a standard single-file pdfLaTeX structure. No successful pdfLaTeX execution is asserted. \paragraph{Standing refusals.} This manuscript proves no Page curve, island, horizon, gravity-generated-entanglement test, exclusion of classical gravity, or Hawking-emission law. It does not say that every entangled state has zero key, that dimensions \(10\) and \(21\) are minimal, or that every later iterate of the stated channel is non-entanglement-breaking. For the separate programme described in the supplied dossier, \[ \boxed{ \begin{gathered} \text{O.1 remains }\NOTCLOSED,\\ \text{the downstream XV-B admission exit is not opened},\\ \text{remaining XVI-N obligations and the series Route B are not discharged},\\ \text{no inherited characteristic quantum coefficient is admitted}. \end{gathered}} \] These declarations do not overwrite separately scoped later results or claim that a technical continuation manuscript does not exist. \begin{thebibliography}{99} \bibitem{OpenAI272} OpenAI. \emph{Entanglement with zero distillable secret key in local dimension ten}. Edition dated 27 September 2026. External Family 272-01 manuscript. Consulted source sections include foundations, coherence, transcripts, secret key, introduction, applications, and the supplementary-checks scope. The dimension-ten geometric/arithmetic construction is not independently verified in the present manuscript. \url{https://github.com/openai/math/tree/main/preprints/Entanglement-with-zero-distillable-secret-key-in-local-dimension-ten-September-27-2026} \bibitem{Companion272} N.~Cheung. \emph{Enter Calculus Companion: OpenAI 272-01 identification page}. Consulted 14 October 2026. A source-identification and scope record, not proof verification. \url{https://enter.grok.me/openai/272-01} \bibitem{LeanScope} OpenAI. \emph{Entanglement without distillable secret key: Lean scope note}. Repository file \texttt{lean/docs/272.md}. Consulted 14 October 2026. The listed pair and channel targets exclude the zero-key theorem. \url{https://github.com/openai/math/blob/main/lean/docs/272.md} \bibitem{LeanPair} OpenAI. \emph{DimensionTenPair.lean}. Repository file \texttt{lean/ComparatorChallenges/DimensionTenPair.lean}. Consulted 14 October 2026. The inspected \texttt{main\_pair} proof body contains \texttt{sorry}; no completed formal proof is asserted. \url{https://github.com/openai/math/blob/main/lean/ComparatorChallenges/DimensionTenPair.lean} \bibitem{LeanChannel} OpenAI. \emph{DimensionTenChannel.lean}. Repository file \texttt{lean/ComparatorChallenges/DimensionTenChannel.lean}. Consulted 14 October 2026. The inspected \texttt{exists\_channel\_fin21} proof body contains \texttt{sorry}. \url{https://github.com/openai/math/blob/main/lean/ComparatorChallenges/DimensionTenChannel.lean} \bibitem{Supplementary272} OpenAI. \emph{Supplementary exact checks}. Appendix in the Family 272-01 source, \texttt{build/source/appendices/supplementary-checks.tex}. Scope of the two small integer-check programs for the separate combinatorial construction. No execution is reproduced here. \url{https://github.com/openai/math/blob/main/preprints/Entanglement-with-zero-distillable-secret-key-in-local-dimension-ten-September-27-2026/build/source/appendices/supplementary-checks.tex} \bibitem{Watrous} J.~Watrous. \emph{The Theory of Quantum Information}. Cambridge University Press, 2018. Finite-dimensional channels, reference systems, Choi operators, and completely bounded trace norms. \url{https://cs.uwaterloo.ca/~watrous/TQI/} \bibitem{Choi1975} M.-D.~Choi. Completely positive linear maps on complex matrices. \emph{Linear Algebra and its Applications} \textbf{10} (1975), 285--290. doi:10.1016/0024-3795(75)90075-0. \bibitem{HSR2003} M.~Horodecki, P.~W.~Shor, and M.~B.~Ruskai. Entanglement breaking channels. \emph{Reviews in Mathematical Physics} \textbf{15} (2003), 629--641. doi:10.1142/S0129055X03001709. Preprint title: \emph{General Entanglement Breaking Channels}. \url{https://arxiv.org/abs/quant-ph/0302031} \bibitem{HorodeckiRange} P.~Horodecki. Separability criterion and inseparable mixed states with positive partial transposition. \emph{Physics Letters A} \textbf{232} (1997), 333--339. doi:10.1016/S0375-9601(97)00416-7. \url{https://arxiv.org/abs/quant-ph/9703004} \bibitem{HHHO2005} K.~Horodecki, M.~Horodecki, P.~Horodecki, and J.~Oppenheim. Secure key from bound entanglement. \emph{Physical Review Letters} \textbf{94} (2005), 160502. doi:10.1103/PhysRevLett.94.160502. \url{https://arxiv.org/abs/quant-ph/0309110} \bibitem{HHHO2009} K.~Horodecki, M.~Horodecki, P.~Horodecki, and J.~Oppenheim. General paradigm for distilling classical key from quantum states. \emph{IEEE Transactions on Information Theory} \textbf{55} (2009), 1898--1929. doi:10.1109/TIT.2008.2009798. \url{https://arxiv.org/abs/quant-ph/0506189} \bibitem{FuchsVanDeGraaf} C.~A.~Fuchs and J.~van de Graaf. Cryptographic distinguishability measures for quantum-mechanical states. \emph{IEEE Transactions on Information Theory} \textbf{45} (1999), 1216--1227. \url{https://arxiv.org/abs/quant-ph/9712042} \bibitem{CLMOW} E.~Chitambar, D.~Leung, L.~Man\v{c}inska, M.~Ozols, and A.~Winter. Everything you always wanted to know about LOCC (but were afraid to ask). \emph{Communications in Mathematical Physics} \textbf{328} (2014), 303--326. \url{https://arxiv.org/abs/1210.4583} \bibitem{Kallenberg} O.~Kallenberg. \emph{Foundations of Modern Probability}. Second edition, Springer, 2002. Standard Borel kernels, conditional distributions, countable history extensions, and conditional expectation. \bibitem{CMHW2019} M.~Christandl, A.~M\"uller-Hermes, and M.~M.~Wolf. When do composed maps become entanglement breaking? \emph{Annales Henri Poincar\'e} \textbf{20} (2019). PPT-composition framework, Choi transfer, and block-switch comparisons. \url{https://arxiv.org/abs/1807.01266} \bibitem{Filippov2021} S.~N.~Filippov. \emph{Capacity of trace decreasing quantum operations and superadditivity of coherent information for a generalized erasure channel}. 2021. Trace-preserving flag completion is a comparison mechanism, not a key-distillation theorem. \url{https://arxiv.org/abs/2101.05686} \bibitem{HansonRouzeFranca} E.~P.~Hanson, C.~Rouz\'e, and D.~Stilck Fran\c{c}a. Eventually entanglement breaking Markovian dynamics: structure and characteristic times. \emph{Annales Henri Poincar\'e} \textbf{21} (2020), 1517--1571. doi:10.1007/s00023-020-00906-4. \bibitem{Park} S.-J.~Park. \emph{Every PPT channel has finite entanglement-breaking index}. Preprint, 2026, arXiv:2608.13551. First submitted 13 August 2026. Cited for its stated eventual-breaking theorem, not independently verified here. \url{https://arxiv.org/abs/2608.13551} \bibitem{Hoeffding} W.~Hoeffding. Probability inequalities for sums of bounded random variables. \emph{Journal of the American Statistical Association} \textbf{58} (1963), 13--30. doi:10.1080/01621459.1963.10500830. \bibitem{CheungI} N.~Cheung. \emph{Landmark I}, version 2. Supplied manuscript \texttt{I.tex}. Relevant items: \texttt{prop:classical-recovery} and the record/continuation, destructive-readout, and retained-memory interfaces. Enter Calculus Companion. The structural measurement class is not replaced by a secret-key or gravity model. \bibitem{CheungVIIIB} N.~Cheung. \emph{VIII-B}, version 3. Supplied manuscript \texttt{VIII-B-v3.tex}. Relevant supplied label: \texttt{prop:classical-recovery}. Sharp record-only recovery obstruction and its retained-quantum-memory exception. Enter Calculus Companion. \bibitem{CheungHawk04B} N.~Cheung. \emph{Hawk04-B}. Supplied source descriptions and comparative excerpts. Typed readout, operational discard, complete preservation, and record-only quantum-recovery limitations. No evaporation endpoint or secret-key theorem is imported. Enter Calculus Companion. \bibitem{CheungEn02A} N.~Cheung. \emph{En02-A}, version 1. Supplied manuscript \texttt{En02-A-v1.tex}. Relevant label: \texttt{thm:Dprime}. Exact one-shot environment ledger and its distinction from adaptive live-memory occupancy. Enter Calculus Companion. \bibitem{CheungEn02B} N.~Cheung. \emph{En02-B}, version 1. Supplied manuscript \texttt{En02-B-v1.tex}. Relevant labels: \texttt{thm:batch}, \texttt{thm:B5}, \texttt{prop:observable}, and \texttt{thm:communication}. Specified subsystem decoders, streaming access, and communication costs; not Family 272 inputs. Enter Calculus Companion. \bibitem{CheungEn02C} N.~Cheung. \emph{En02-C}, version 1. Supplied manuscript \texttt{En02-C-v1.tex}. Relevant labels: \texttt{thm:C1}, \texttt{thm:C2}, \texttt{thm:C3}, and \texttt{cor:robustgap}. Complete sequential soundness and model-specific memory/recovery obstructions. Enter Calculus Companion. \bibitem{CheungEn01B} N.~Cheung. \emph{En01-B}, version 2. Supplied manuscript \texttt{En01-B-v2.tex}. Relevant label: \texttt{thm:bounded}. Predeclared bounded complete-record statistics, uniform family gaps, and implementation allowances. Enter Calculus Companion. \bibitem{CheungEn01C} N.~Cheung. \emph{En01-C}, version 1. Supplied manuscript \texttt{En01-C.tex}. Relevant label: \texttt{thm:certificate}. Clipping, complete attempted-run records, implementation allowances, and finite-sample coverage for its declared statistic. No diffusion parameter or apparatus is transferred here. Enter Calculus Companion. \bibitem{CheungOai265A} N.~Cheung. \emph{Oai265-A}, supplied version 1. Relevant labels: \texttt{def:determination} and \texttt{thm:separation}. Static entropy records, selected spectra, complete channels, and radiation histories are distinct interfaces. The earlier conversation development under that identifier is not independently registered or machine-verified here. Enter Calculus Companion. \bibitem{CheungEn07C} N.~Cheung. \emph{En07-C}, version 1, as supplied in the comparative material. Relevant comparison: selected entropy and thermal spectra do not determine a complete channel or its referenced recovery behavior. No thermal input is identified with the Family 272 state. Enter Calculus Companion. \bibitem{CheungEm03F} N.~Cheung. \emph{Em03-F}, version 1. Supplied manuscript \texttt{Em03-F-v1.tex}. Relevant labels: \texttt{thm:EB}, \texttt{thm:recovery}, \texttt{thm:witness}, and \texttt{thm:counts}. A declared packet channel, a classical signal, and a referenced quantum-recovery obstruction. No Family 272 or gravitational identification is imported. Enter Calculus Companion. \bibitem{CheungEm03G} N.~Cheung. \emph{Em03-G}, version 1. Supplied manuscript \texttt{Em03-G-v1.tex}. Relevant labels: \texttt{prop:Fobstruction}, \texttt{thm:compacttransmission}, and \texttt{thm:lower}. Receiver postprocessing, changed source dynamics, resource-dependent recovery, and finite-coupling obstructions are distinguished. Enter Calculus Companion. \bibitem{ComparisonDossier} \emph{User-supplied Oai272-A development plan and comparative source dossier}. Includes Family 272 and comparison-family records, supplied Cheung excerpts, and nominations including En07-A, Oai265-B, Oai290-A, Oai280-C, En10-B, and Oai283-A. A nomination is not a complete theorem statement, an inherited premise, or independent verification. Retrieval label supplied by the user: \texttt{178f233f (retrieval-3)}. \bibitem{AnalyticDossier} N.~Cheung. Supplied version-specific excerpts from \emph{IX-Free-2}, \emph{IX-D}, \emph{XI-E/F/G}, \emph{XIV-A/B}, and \emph{XVI-B/D}, together with the stated XIV--XV--XVI programme boundaries. Separate analytic source records, not premises of this finite-dimensional certificate. No quantum-admission or standing-problem conclusion is transferred. Enter Calculus Companion. \end{thebibliography} \end{document}