% Oai276-A.tex
% Single-file manuscript for pdfLaTeX.
%
% Suggested build commands (not executed in this response):
%   pdflatex -interaction=nonstopmode -halt-on-error Oai276-A.tex
%   pdflatex -interaction=nonstopmode -halt-on-error Oai276-A.tex
%
% Mathematical release:
%   * A locally proved one-use Holevo optimization.
%   * An explicit finite certificate at (gamma,nu)=(1/2,1/4).
%   * A source-qualified audit of the external repeated-use and
%     arbitrary-partner claims.
%
% Not claimed:
%   * Independent verification of the complete Family 276 proof.
%   * A completed Lean proof from a Comparator target containing sorry.
%   * Generalized amplitude-damping quantum or secret-key capacity.
%   * A gravitational interpretation.
%
% The optional exact-rational checker in Appendix A is included as text.
% Its execution is not required by pdfLaTeX and is not asserted here.

\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{record}[theorem]{External claim record}
\newtheorem{specification}[theorem]{Specification}
\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{\A}{\mathcal A}
\newcommand{\Tr}{\operatorname{Tr}}
\newcommand{\id}{\operatorname{id}}
\newcommand{\diag}{\operatorname{diag}}
\newcommand{\rank}{\operatorname{rank}}
\newcommand{\atanh}{\operatorname{atanh}}
\newcommand{\ket}[1]{|#1\rangle}
\newcommand{\bra}[1]{\langle#1|}
\newcommand{\kb}[2]{|#1\rangle\langle#2|}
\newcommand{\proj}[1]{\kb{#1}{#1}}
\newcommand{\dtr}{d_{\mathrm{tr}}}
\newcommand{\ddia}{d_{\diamond}}
\newcommand{\E}{\mathbb E}
\newcommand{\Prob}{\mathbb P}
\newcommand{\Smin}{S_{\min}}
\newcommand{\NOTCLOSED}{\texttt{NOT\_CLOSED}}
\newcommand{\hbin}{h_2}
\newcommand{\gbin}{g_2}
\newcommand{\hnat}{h_{\mathrm e}}
\newcommand{\gnat}{g_{\mathrm e}}
\newcommand{\snat}{S_{\mathrm e}}

\title{\textbf{Oai276-A}\\
A Finite Certificate for a Generalized\\
Amplitude-Damping Holevo Optimum\\[3pt]
\large One-use proof, seven-stage audit, and operational separations}
\author{Ngo Cheung}
\date{14 October 2026}

\begin{document}
\maketitle

\begin{abstract}
We complete the proposed finite-certificate programme for one
specified generalized amplitude-damping channel, without assuming
the external Family 276 repeated-use or arbitrary-partner
additivity claims. We first prove the one-use Holevo formula
directly from qubit output determinants, entropy concavity, and
a scalar convexity argument. For the genuinely thermal,
nonunital parameter pair
\[
(\gamma,\nu)=(1/2,1/4),
\]
we specify the unique maximizing population as an isolated zero
of an explicit strictly decreasing derivative and prove
\[
\frac{469}{1000}<p^\star<\frac{47}{100},
\qquad
\frac{412377}{10^6}
<
\chi(\A_{1/2,1/4})
<
\frac{412378}{10^6}
\quad\text{bits}.
\]
The proof uses finite rational sums with rigorous tails, not
floating-point optimization. Both the exact maximizing phase
pair and a fully algebraic near-optimal pair are written out.

The remaining stages audit the block-entropy, thermal-extension,
channel-substitution, ensemble, and partner-channel interfaces;
price specified implementation and statistical comparisons; and
separate one-use information, asymptotic classical transmission,
quantum recovery, and secrecy. The inspected Comparator target
contains a proof placeholder, so its scope description is not
treated as an executed formal proof. The finite certificate does
not verify the complete external capacity theorem, prove
arbitrary-partner additivity, or establish optimality of
separate measurements. No Page curve, gravitational test,
quantum-capacity formula, secret-key formula, or spacetime
emergence is inferred.
\end{abstract}

\tableofcontents

\section{Scope, source status, and the completed task}
\label{sec:scope}

\subsection{The precise submission claim}

The principal new deliverable requested by the plan is an
explicit finite certificate for one frozen scalar optimization.
That deliverable is Theorem~\ref{thm:finite-certificate}.
Its proof is independent of the external multi-use entropy
inequality.

The manuscript also supplies the elementary one-use results
needed to identify the certified scalar maximum with
\(\chi(\A_{1/2,1/4})\). These are not presented as new discoveries:
the one-use generalized amplitude-damping optimization has
precedents in Hou--Fang and in the discussion of Khatri,
Sharma, and Wilde \cite{HouFang,KhatriSharmaWilde}.
A local proof is included so that the finite certificate has
no dependency on the unverified part of Family 276.

The identifier Oai276-A is used as requested. It does not assign
authorship of this development to N.~Cheung or assert its
registration, endorsement, or acceptance in another series.

\subsection{What ``complete the plan'' means here}

The plan expressly calls for an audit \emph{without importing}
the external capacity theorem and for one subsequent finite
certificate. Accordingly, completion has the following meaning:
\begin{enumerate}
\item the external claims and their quantifiers are frozen;
\item their five mathematical interfaces are audited separately;
\item comparison manuscripts are used only in their stated roles;
\item a concrete optimizer and a certified value interval are supplied;
\item unverified multi-use and partner-channel assertions remain
external claims, rather than being relabelled as local theorems.
\end{enumerate}

This is a completed certificate manuscript, not an assertion that
a finite numerical instance verifies an all-parameter capacity
theorem.

\subsection{Source edition and formalization correction}

The publicly accessible Family 276 source is titled
\emph{Classical capacity and entropy inequalities for generalized
amplitude damping}, attributed to OpenAI, and dated
24 September 2026 \cite{OpenAI276}.
The source uses natural logarithms in its entropy functions and
a factor \(1/\ln2\) when reporting information in bits.

The scope note \texttt{lean/docs/276.md} describes repeated-use
Holevo additivity, equality with operational capacity, and
attaining phase-pair product ensembles. It excludes
arbitrary different partner channels and separate-measurement
optimality \cite{LeanScope276}.

There is an additional distinction. In the inspected
\texttt{ComparatorChallenges/AmplitudeDamping.lean},
the theorem \texttt{OAI.GAD.main} ends with
\texttt{by sorry} \cite{LeanTarget276}.
That target file supplies a specification, not a completed proof
of its theorem body. This observation is not a claim that every
other repository artifact has been inspected. No Lean execution
or verification of a different implementation is asserted.

\section{Stage 0: freeze the channel, units, and claims}
\label{sec:freeze}

\subsection{Information quantities}

All Hilbert spaces in the mathematical arguments are nonzero and
finite dimensional. Entropies in the local theorems are in bits:
\[
S(\rho)=-\Tr(\rho\log_2\rho),
\qquad
\hbin(x)=-x\log_2x-(1-x)\log_2(1-x),
\]
with \(0\log_2 0=0\). Define
\begin{equation}
\gbin(u)
=
\hbin\!\left(\frac{1+\sqrt{1-4u}}2\right),
\qquad 0\le u\le\frac14.
\label{eq:g}
\end{equation}
Natural-logarithm versions are denoted by
\[
\snat=(\ln2)S,\qquad
\hnat=(\ln2)\hbin,\qquad
\gnat=(\ln2)\gbin .
\]

For a channel \(\mathcal N\), its one-use Holevo information is
\begin{equation}
\chi(\mathcal N)
=
\sup_{\{q_a,\rho_a\}}
\left[
S\!\left(\sum_aq_a\mathcal N(\rho_a)\right)
-\sum_aq_a S(\mathcal N(\rho_a))
\right].
\label{eq:holevo}
\end{equation}
The supremum is over finite ensembles of arbitrary input states.
For \(\mathcal N^{\otimes n}\), this includes input signals
entangled across the \(n\) uses.

The unassisted classical capacity \(C(\mathcal N)\) concerns
equiprobable classical messages encoded into arbitrary block
states, with one output POVM on the whole block, no preshared
entanglement, no feedback, and average error tending to zero.
The coding theorem gives
\begin{equation}
C(\mathcal N)
=
\sup_{n\ge1}\frac1n\chi(\mathcal N^{\otimes n}).
\label{eq:regularized}
\end{equation}
The operational coding input is the Holevo--Schumacher--Westmoreland
theorem, not an inference from the existence of a Kraus
representation \cite{Holevo1998,SchumacherWestmoreland,Watrous}.

\subsection{The generalized amplitude-damping convention}

For \(\gamma,\nu\in[0,1]\), write \(k=\sqrt{1-\gamma}\).
The channel is
\begin{equation}
\A_{\gamma,\nu}
\begin{pmatrix}
1-p&z\\
\overline z&p
\end{pmatrix}
=
\begin{pmatrix}
1-t&kz\\
k\overline z&t
\end{pmatrix},
\qquad
t=(1-\gamma)p+\gamma\nu.
\label{eq:channel}
\end{equation}
Here \(\nu\) is the stationary excited-state population, not an
unidentified bosonic occupation number.

A Kraus family is
\begin{align}
L_0&=\sqrt{1-\nu}\,\diag(1,k),
&
L_1&=\sqrt{\gamma(1-\nu)}\,\kb01,
\notag\\
L_2&=\sqrt{\nu}\,\diag(k,1),
&
L_3&=\sqrt{\gamma\nu}\,\kb10.
\label{eq:kraus}
\end{align}

\begin{lemma}[Complete channel specification]
\label{lem:kraus}
The matrices in \eqref{eq:kraus} satisfy
\[
\sum_{r=0}^3L_r^\dagger L_r=I_2
\]
and implement \eqref{eq:channel}. Thus the formula defines a CPTP
map, including all parameter endpoints.
\end{lemma}

\begin{proof}
The two diagonal contributions to the completeness sum are
\[
(1-\nu)\diag(1,1-\gamma)
+\nu\diag(1-\gamma,1).
\]
The jump contributions are
\(\gamma(1-\nu)\kb11+\gamma\nu\kb00\).
Their sum is \(I_2\).
Direct multiplication gives excited-state population
\((1-\gamma)p+\gamma\nu\) and coherence multiplier \(k\).
\end{proof}

These standard channel conventions agree with the parameterization
used in the source and in the information-theoretic study
\cite{OpenAI276,KhatriSharmaWilde}.

\subsection{The external claims, not local premises}

Set
\begin{equation}
v_{\gamma,\nu}(p)
=
\gamma\nu(1-\nu)+\gamma(1-\gamma)(p-\nu)^2,
\qquad
F_{\gamma,\nu}(p)
=
\hbin((1-\gamma)p+\gamma\nu)-\gbin(v_{\gamma,\nu}(p)).
\label{eq:objective}
\end{equation}

\begin{record}[Repeated uses and operational capacity]
\label{rec:main}
Family 276 asserts, for every \((\gamma,\nu)\in[0,1]^2\) and
\(n\ge1\),
\[
\chi(\A_{\gamma,\nu}^{\otimes n})
=
n\max_{0\le p\le1}F_{\gamma,\nu}(p),
\qquad
C(\A_{\gamma,\nu})=\chi(\A_{\gamma,\nu}).
\]
It further asserts that every maximizing \(p\) gives attaining
equiprobable phase-pair products, where
\[
\phi_\pm(p)=\sqrt{1-p}\ket0\pm\sqrt p\ket1.
\]
The maximum is one-dimensional; this is not a closed algebraic
evaluation of its maximizer \cite{OpenAI276}.
\end{record}

\begin{record}[Arbitrary finite-dimensional partner]
\label{rec:partner}
The source separately asserts, for every finite-dimensional CPTP
partner \(\mathcal N\),
\[
\chi(\A\otimes\mathcal N)=\chi(\A)+\chi(\mathcal N),
\]
\[
\Smin(\A\otimes\mathcal N)=\Smin(\A)+\Smin(\mathcal N),
\qquad
C(\A\otimes\mathcal N)=C(\A)+C(\mathcal N).
\]
The partner retains its own regularization.
This quantifier is stronger than repeated uses of \(\A\), and it
is outside the inspected Lean scope \cite{OpenAI276,LeanScope276}.
\end{record}

\begin{remark}[Units correction]
If the source's \(h\) and \(g\) are retained as natural-logarithm
functions, the right-hand side of its information formula must
be divided by \(\ln2\). In \eqref{eq:objective}, both functions
are already in bits, so no further factor is present.
\end{remark}

Neither external record is assumed in the proof of
Theorem~\ref{thm:finite-certificate}.

\section{Local one-use proof}
\label{sec:oneuse}

\subsection{Elementary entropy facts}

\begin{lemma}[Entropy comparisons]
\label{lem:entropy}
For finite-dimensional states:
\begin{enumerate}
\item \(S(\rho)\le H(\diag\rho)\) in any orthonormal basis;
\item \(S\) is concave;
\item \(S(\rho\otimes\sigma)=S(\rho)+S(\sigma)\);
\item a two-by-two state of determinant \(u\) has entropy \(\gbin(u)\).
\end{enumerate}
\end{lemma}

\begin{proof}
The diagonal is obtained from the eigenvalue vector by the doubly
stochastic matrix of squared moduli of unitary entries.
Concavity of \(-x\log_2x\), applied row by row, proves item 1.

For a mixture, choose a basis diagonalizing that mixture.
Classical entropy concavity in this basis, followed by item 1
for each component, proves item 2.
The eigenvalues of a tensor product are pairwise products,
which proves item 3.
For item 4, the characteristic polynomial is
\(\lambda^2-\lambda+u\), giving the two eigenvalues used in
\eqref{eq:g}.
\end{proof}

\begin{lemma}[Scalar convexity]
\label{lem:convex}
The function \(s\mapsto\gbin(s^2)\) is nondecreasing and convex
on \([0,1/2]\).
Consequently,
\[
e_{\gamma,\nu}(p):=\gbin(v_{\gamma,\nu}(p))
\]
is convex on \([0,1]\) for every \(\gamma,\nu\in[0,1]\).
\end{lemma}

\begin{proof}
It suffices to calculate in nats.
For \(0<u<1/4\), set
\[
r=\sqrt{1-4u},
\qquad
L=\frac{\atanh r}{r}.
\]
Differentiation gives
\[
\gnat'(u)=2L,
\qquad
u\gnat''(u)+\frac12\gnat'(u)=\frac{L-1}{r^2}\ge0.
\]
The inequality follows from \(\atanh r\ge r\).
Therefore
\[
\frac{d}{ds}\gnat(s^2)\ge0,
\qquad
\frac{d^2}{ds^2}\gnat(s^2)
=
4\left(s^2\gnat''(s^2)+\frac12\gnat'(s^2)\right)\ge0.
\]
Continuous endpoint limits extend the conclusion to the closed
interval.

Finally,
\[
\sqrt{v_{\gamma,\nu}(p)}
=
\left\|
\begin{pmatrix}
\sqrt{\gamma\nu(1-\nu)}\\
\sqrt{\gamma(1-\gamma)}(p-\nu)
\end{pmatrix}
\right\|_2
\]
is convex. Compose it with the nondecreasing convex function
just proved.
\end{proof}

This scalar entropy function also appears in the two-qubit
entropy--concurrence relation \cite{Wootters}.
No additivity property of entanglement of formation is used.

\subsection{Population-resolved output entropy}

\begin{lemma}[One-qubit output determinant]
\label{lem:determinant}
Every pure qubit input with excited-state probability \(p\) has
output determinant \(v_{\gamma,\nu}(p)\).
For every mixed input \(\rho\) with the same population,
\[
S(\A_{\gamma,\nu}(\rho))\ge e_{\gamma,\nu}(p).
\]
\end{lemma}

\begin{proof}
For a pure input, \(|z|^2=p(1-p)\), so the determinant of
\eqref{eq:channel} is
\[
t(1-t)-(1-\gamma)p(1-p).
\]
Expansion gives
\[
\gamma\nu(1-\nu)+\gamma(1-\gamma)(p-\nu)^2.
\]
This is in \([0,1/4]\) because it is the determinant of a state.

For a spectral decomposition
\(\rho=\sum_aw_a\proj{\psi_a}\), let \(p_a\) be the component
populations. Entropy concavity and Lemma~\ref{lem:convex} give
\[
S(\A(\rho))
\ge\sum_aw_ae(p_a)
\ge e\!\left(\sum_aw_ap_a\right)=e(p).
\]
\end{proof}

\begin{theorem}[One-use Holevo formula and phase-pair attainment]
\label{thm:oneuse}
For all \(\gamma,\nu\in[0,1]\),
\begin{equation}
\chi(\A_{\gamma,\nu})
=
\max_{0\le p\le1}F_{\gamma,\nu}(p).
\label{eq:oneuse}
\end{equation}
At every maximizing \(p\), the equiprobable pair
\[
\left\{
\frac12,\sqrt{1-p}\ket0+\sqrt p\ket1;
\quad
\frac12,\sqrt{1-p}\ket0-\sqrt p\ket1
\right\}
\]
attains the maximum.

For every \(n\), its independent product ensemble has Holevo
information \(n\chi(\A_{\gamma,\nu})\). This last assertion is
an attained lower bound on
\(\chi(\A_{\gamma,\nu}^{\otimes n})\), not an upper bound on
entangled block signals.
\end{theorem}

\begin{proof}
Take any ensemble \(\{q_a,\rho_a\}\), with populations \(p_a\),
and put \(\overline p=\sum_aq_ap_a\).
The average output has population \(t(\overline p)\).
Lemma~\ref{lem:entropy} gives
\[
S\!\left(\sum_aq_a\A(\rho_a)\right)
\le\hbin(t(\overline p)).
\]
Lemma~\ref{lem:determinant} and convexity give
\[
\sum_aq_aS(\A(\rho_a))
\ge\sum_aq_ae(p_a)\ge e(\overline p).
\]
Subtracting proves the upper bound by
\(F_{\gamma,\nu}(\overline p)\).
Continuity on \([0,1]\) gives existence of a maximizing \(p\).

For the displayed pair, the opposite coherences cancel in the
average. Its average output is diagonal with population \(t(p)\),
and each individual output has entropy \(e(p)\).
Its Holevo information is exactly \(F_{\gamma,\nu}(p)\).

For products, both the average output and each conditional output
are tensor products. Entropy additivity gives \(nF_{\gamma,\nu}(p)\).
No unrestricted tensor-power upper bound has been proved in
this argument.
\end{proof}

\begin{proposition}[Optimizer structure and endpoints]
\label{prop:optimizer}
For \(0\le\gamma<1\), the function \(F_{\gamma,\nu}\) is strictly
concave, has a unique maximizer in \((0,1)\), and satisfies
\[
F_{\gamma,\nu}(0)=F_{\gamma,\nu}(1)=0.
\]
At \(\gamma=1\), the channel is a replacement channel,
\(F_{\gamma,\nu}\equiv0\), and every \(p\) maximizes.

The one-use minimum output entropy is
\[
\Smin(\A_{\gamma,\nu})
=
\gbin(\gamma\nu(1-\nu)).
\]
\end{proposition}

\begin{proof}
When \(\gamma<1\), the first term of \(F\) is strictly concave
as binary entropy composed with an injective affine map.
The second term is convex by Lemma~\ref{lem:convex}.
Thus their difference is strictly concave.

At \(p=0,1\), the pure input is a computational-basis vector,
its output is diagonal, and the two entropy terms coincide.
For \(0<p<1\), the output determinant satisfies
\[
v_{\gamma,\nu}(p)
<
t(p)(1-t(p)).
\]
The determinant entropy is strictly increasing in the interior,
so \(F_{\gamma,\nu}(p)>0\). The unique maximum is therefore
interior.

At \(\gamma=1\), \eqref{eq:channel} is independent of the input.
For the minimum entropy, a pure input suffices by concavity.
The completed square for \(v\), its minimum at \(p=\nu\), and
monotonicity of \(\gbin\) prove the formula.
\end{proof}

\begin{remark}[Maximum information is not minimum output entropy]
The population minimizing an individual output entropy need
not maximize Holevo information. In the certificate below,
the former population is \(1/4\), whereas
\(p^\star>469/1000\).
\end{remark}

\section{Stage 1: audit the five external proof interfaces}
\label{sec:audit}

This section distinguishes a source assertion, an algebraic
substitution, and a verified capacity implication.
The source's block and thermal entropy inequalities are not
premises of the finite certificate.

\subsection{Gate 1: the rectangular zero-block assertion}

For rectangular \(A,B,C\) of the same shape, set
\[
M=
\begin{pmatrix}
A&B\\
C&0
\end{pmatrix},
\qquad
x=\Tr AA^\dagger,\quad
y=\Tr BB^\dagger,\quad
z=\Tr CC^\dagger,
\quad x+y+z=1.
\]
The source's \texttt{thm:block} asserts
\begin{equation}
S(MM^\dagger)
\ge
xS(AA^\dagger/x)+yS(BB^\dagger/y)
+zS(CC^\dagger/z)+\gbin(yz),
\label{eq:audit-block}
\end{equation}
with zero-weight terms omitted \cite{SourceBlock276}.

The audit obligations are:
\begin{enumerate}
\item prove the inequality for noncommuting blocks;
\item retain the direction of the entropy inequality;
\item justify singular blocks without inverses of those blocks;
\item preserve the nonzero singular values under rectangular
zero padding.
\end{enumerate}
A scalar check, commuting special case, or numerical singular-value
comparison does not discharge the first obligation.
A matrix entropy inequality is not yet a coding theorem.

\subsection{Gate 2: the thermal extension}

The source's \texttt{thm:thermal} concerns matrices \(X,Y\) with
\(\Tr XX^\dagger=\Tr YY^\dagger=1\) and coefficients
\[
\alpha,\beta,\eta,\delta\ge0,\qquad
\alpha+\beta+\eta+\delta=1,\qquad
\alpha\delta-\beta\eta=K^2,\quad K\ge0.
\]
Its state has the form
\[
T=
\begin{pmatrix}
\alpha XX^\dagger+\beta YY^\dagger&KXY^\dagger\\
KYX^\dagger&\eta XX^\dagger+\delta YY^\dagger
\end{pmatrix}.
\]
Writing \(U_0=\alpha+\beta\), \(U_1=\eta+\delta\), and
\(u=U_0U_1-K^2\), the asserted bound is
\begin{equation}
S(T)\ge
(\alpha+\eta)S(XX^\dagger)
+(\beta+\delta)S(YY^\dagger)+\gbin(u).
\label{eq:audit-thermal}
\end{equation}
The source obtains it from zero-block factorizations
\cite{SourceThermal276}.

The relevant algebra is
\[
u=\beta U_1+\eta U_0.
\]
For \(u>0\), the two coefficient endpoints used in the source
have \((\beta,\eta)=(u/U_1,0)\) and \((0,u/U_0)\), with weights
\(\beta U_1/u\) and \(\eta U_0/u\).
The essential audit is that both endpoint bounds retain the
\emph{same} scalar term \(\gbin(u)\).
Otherwise entropy concavity would not give the advertised
thermal statement.
The cases \(u=0\), vanished row sums, and zero mixture weights
must be handled separately.

Nothing in this coefficient condition identifies a Hawking
occupation, a bath spectrum, or a temporal radiation history.

\subsection{Gate 3: the channel substitution}

The substitution itself is elementary and can be checked without
assuming \eqref{eq:audit-thermal}. Put
\[
a=1-\gamma\nu,\quad
b=\gamma(1-\nu),\quad
c=\gamma\nu,\quad
d=1-\gamma(1-\nu),\quad
k=\sqrt{1-\gamma}.
\]
Then
\begin{equation}
a+c=b+d=1,\qquad ad-bc=k^2.
\label{eq:coefficients}
\end{equation}

For a normalized pure input
\[
\psi=\sqrt{1-p}\ket0\otimes\psi_0
+\sqrt p\ket1\otimes\psi_1
\]
and a CPTP partner with Kraus matrices \(V_\ell\), form rectangular
matrices with columns
\[
X_\ell=V_\ell\psi_0,\qquad Y_\ell=V_\ell\psi_1.
\]
Their common column index gives
\[
XX^\dagger=\mathcal N(\proj{\psi_0}),\quad
YY^\dagger=\mathcal N(\proj{\psi_1}),\quad
XY^\dagger=\mathcal N(\kb{\psi_0}{\psi_1}).
\]
No orthogonality of \(\psi_0,\psi_1\) is required.

The thermal coefficients are
\[
\alpha=a(1-p),\quad
\beta=bp,\quad
\eta=c(1-p),\quad
\delta=dp,\quad
K=k\sqrt{p(1-p)}.
\]
Equation~\eqref{eq:coefficients} verifies their required identity,
and their scalar \(u\) is \(v_{\gamma,\nu}(p)\).

The algebra therefore identifies exactly where the thermal
entropy theorem would enter. It does not prove that theorem.
In particular, a Kraus representation is not a decoder.

\subsection{Gate 4: entangled block signals and attainment}

The nontrivial multi-use assertion is the lower bound
\begin{equation}
S(\A_{\gamma,\nu}^{\otimes n}(\rho))
\ge
\sum_{j=1}^n e_{\gamma,\nu}(p_j)
\label{eq:population-bound}
\end{equation}
for every block state \(\rho\), including entangled signals.
It is not obtained by subadditivity: subadditivity has the
opposite direction for a joint entropy.

\begin{proposition}[Conditional repeated-use reduction]
\label{prop:conditional}
Fix \((\gamma,\nu)\). If \eqref{eq:population-bound} holds for
every \(n\) and every block input, then
\[
\chi(\A_{\gamma,\nu}^{\otimes n})
=
n\chi(\A_{\gamma,\nu}),
\qquad
C(\A_{\gamma,\nu})=\chi(\A_{\gamma,\nu}).
\]
Every maximizing phase-pair product ensemble attains the
block Holevo value.
\end{proposition}

\begin{proof}
For an arbitrary ensemble of block signals, let
\(\overline p_j\) be its mean population at site \(j\).
Diagonal entropy and classical subadditivity bound the mean
output entropy above by
\[
\sum_j\hbin(t(\overline p_j)).
\]
The assumed bound and convexity of \(e\) bound the average
conditional output entropy below by
\(\sum_je(\overline p_j)\).
Subtracting gives at most \(n\max_pF_{\gamma,\nu}(p)\).
Theorem~\ref{thm:oneuse} supplies a product ensemble attaining it.
Equation~\eqref{eq:regularized} then gives the capacity identity.
\end{proof}

The hypothesis of this proposition is not verified here.
The source's route to it uses the thermal branch inequality,
iteration, and convexity \cite{SourceOutput276}.

\begin{remark}[An attaining ensemble is not a reliable full codebook]
When \(\chi(\A)<1\), the \(2^n\) equiprobable phase-pair products
do not thereby become \(2^n\) reliably distinguishable messages.
Their ensemble entropy difference is \(n\chi(\A)\).
Coding uses suitable codebooks and decoding POVMs; it is a
different construction.
\end{remark}

\subsection{Gate 5: an arbitrary partner is a stronger quantifier}

For a pure signal on a damping input and a partner input, the
source uses the stronger branch estimate
\begin{equation}
S((\A\otimes\mathcal N)(\proj\psi))
\ge
e(p)+(1-p)S(\mathcal N(\proj{\psi_0}))
+pS(\mathcal N(\proj{\psi_1})).
\label{eq:partner-branch}
\end{equation}
This is the rectangular thermal application, not a consequence
of same-channel additivity.

The key ensemble identity is that the conditional partner
outputs, weighted by \(q_a(1-p_a)\) and \(q_ap_a\), have mean
equal to the partner marginal of the mean full output.
If \eqref{eq:partner-branch} is supplied, subtracting conditional
entropies from
\[
S(\overline\sigma)\le
\hbin(t(\overline p))+S(\overline\sigma_{\rm partner})
\]
leaves one damping objective and one partner Holevo expression.
The same branch estimate supplies the minimum-output lower bound.
For regularized capacity, the partner must still be
\(\mathcal N^{\otimes n}\), not replaced by its one-use value
\cite{SourcePartners276}.

This identifies the proof obligation without importing
Record~\ref{rec:partner}. Neither this arbitrary-partner bound
nor separate-measurement optimality is part of the finite
certificate below.

\section{Stages 3 and 6: the explicit finite maximum certificate}
\label{sec:certificate}

\subsection{Freeze a genuinely thermal, nonunital channel}

From now on,
\begin{equation}
\gamma=\frac12,\qquad
\nu=\frac14,\qquad
\A=\A_{1/2,1/4}.
\label{eq:frozen}
\end{equation}
The objective in nats is
\begin{equation}
f(p):=(\ln2)F_{1/2,1/4}(p)
=
\hnat\!\left(\frac p2+\frac18\right)
-
\gnat\!\left(\frac3{32}+\frac{(p-1/4)^2}{4}\right).
\label{eq:f}
\end{equation}
Define
\begin{equation}
d(p)=p-\frac14,\qquad
x(p)=\frac34-p,\qquad
q(p)=\frac58-d(p)^2.
\label{eq:xq}
\end{equation}
The determinant eigenvalue radius is \(\sqrt{q(p)}\).

\begin{lemma}[Strict derivative and quantitative curvature]
\label{lem:derivative}
For the frozen channel, \(f\) is smooth on \([0,1]\) and
\begin{equation}
D(p):=f'(p)
=
\atanh(x(p))
-
d(p)\frac{\atanh\sqrt{q(p)}}{\sqrt{q(p)}}.
\label{eq:D}
\end{equation}
Moreover,
\begin{equation}
f''(p)\le-1
\qquad(0\le p\le1).
\label{eq:curvature}
\end{equation}
Consequently \(D\) is strictly decreasing and, for every \(p_0\),
\begin{equation}
\max_{p\in[0,1]}f(p)
\le
f(p_0)+\frac{D(p_0)^2}{2}.
\label{eq:quadratic}
\end{equation}
\end{lemma}

\begin{proof}
The output population lies in \([1/8,5/8]\).
The determinant is strictly between zero and \(1/4\), so all
functions used here are smooth.

For \(r=\sqrt{1-4u}\),
\[
\gnat'(u)=\frac1r\ln\frac{1+r}{1-r}.
\]
Differentiate \eqref{eq:f} and use
\(1-2(p/2+1/8)=x(p)\) to obtain \eqref{eq:D}.

The determinant entropy term is convex by
Lemma~\ref{lem:convex}. For the first term,
\[
\frac{d^2}{dp^2}\hnat\!\left(\frac p2+\frac18\right)
=
-\frac1{4t(p)(1-t(p))}\le-1.
\]
This proves \eqref{eq:curvature}.

Integrating the curvature bound gives
\[
f(p)\le f(p_0)+D(p_0)(p-p_0)-\frac12(p-p_0)^2.
\]
The maximum of the quadratic on the whole real line is
\(f(p_0)+D(p_0)^2/2\), proving \eqref{eq:quadratic}.
\end{proof}

\subsection{Rational sums and explicit remainder bounds}

For \(0\le z<1\), define
\begin{align}
\mathcal L(z)&=\sum_{k=0}^{\infty}\frac{z^k}{2k+1},
&
L_N(z)&=\sum_{k=0}^{N-1}\frac{z^k}{2k+1},
\notag\\
J(z)&=\sum_{k=1}^{\infty}\frac{z^k}{2k(2k-1)},
&
J_N(z)&=\sum_{k=1}^{N}\frac{z^k}{2k(2k-1)}.
\label{eq:sums}
\end{align}
Put
\begin{equation}
T_N(z)=\frac{z^N}{(2N+1)(1-z)},
\qquad
R_N(z)=
\frac{z^{N+1}}{(2N+2)(2N+1)(1-z)}.
\label{eq:tails}
\end{equation}

\begin{lemma}[Certified series identities]
\label{lem:series}
For \(0\le z<1\),
\[
0\le\mathcal L(z)-L_N(z)\le T_N(z),
\qquad
0\le J(z)-J_N(z)\le R_N(z).
\]
Also,
\begin{equation}
\atanh r=r\mathcal L(r^2),
\qquad
\hnat\!\left(\frac{1+r}{2}\right)=\ln2-J(r^2)
\quad (|r|<1).
\label{eq:series-identities}
\end{equation}
Therefore
\begin{equation}
f(p)=J(q(p))-J(x(p)^2).
\label{eq:fseries}
\end{equation}
\end{lemma}

\begin{proof}
Expand \(1/(1-r^2)\) geometrically and integrate from zero
to \(r\). This gives the \(\atanh\) series.
The derivative of
\(\ln2-\hnat((1+r)/2)\) is \(\atanh r\); integrating again
gives the \(J\) series.

For each tail, replace every denominator by its first omitted
denominator and sum the remaining geometric series.
Equation~\eqref{eq:fseries} follows because binary entropy is
symmetric and \(x(p)=1-2t(p)\).
\end{proof}

Only rational arithmetic is needed when \(p\) is rational.
No numerical square-root evaluation is required.

\subsection{The finite arithmetic certificate}

Fix
\begin{equation}
N=32,\qquad
a=\frac{469}{1000},\quad
b=\frac{47}{100},\quad
p_0=\frac{939}{2000}.
\label{eq:certificate-data}
\end{equation}
For \(p\in[a,b]\), both \(x(p)\) and \(d(p)\) are positive.
Define the rational derivative bounds
\begin{align}
D_N^-(p)
&=
x(p)L_N(x(p)^2)
-d(p)\bigl(L_N(q(p))+T_N(q(p))\bigr),
\notag\\
D_N^+(p)
&=
x(p)\bigl(L_N(x(p)^2)+T_N(x(p)^2)\bigr)
-d(p)L_N(q(p)).
\label{eq:derivative-bounds}
\end{align}
Then \(D_N^-(p)\le D(p)\le D_N^+(p)\).

A rational enclosure of \(\ln2\) is
\begin{equation}
\ell_-=\frac23L_{12}\!\left(\frac19\right),
\qquad
\ell_+=
\ell_-+\frac23T_{12}\!\left(\frac19\right),
\qquad
\ell_-\le\ln2\le\ell_+.
\label{eq:ln2}
\end{equation}
Indeed, \(\ln2=2\atanh(1/3)\).

At \(p_0\), the exact arguments are
\begin{equation}
x_0=\frac{561}{2000},\qquad
x_0^2=\frac{314721}{4000000},\qquad
q_0=\frac{2307279}{4000000}.
\label{eq:arguments}
\end{equation}
Define
\begin{align}
A_-&=J_{32}(q_0)-J_{32}(x_0^2)-R_{32}(x_0^2),
\notag\\
A_+&=J_{32}(q_0)+R_{32}(q_0)-J_{32}(x_0^2),
\notag\\
L_{\rm cert}&=\frac{A_-}{\ell_+},
&
U_{\rm cert}&=
\frac{A_++1/2000000}{\ell_-}.
\label{eq:value-certificate}
\end{align}

\begin{lemma}[Finite rational comparisons]
\label{lem:arithmetic}
The rational numbers in
\eqref{eq:certificate-data}--\eqref{eq:value-certificate}
satisfy
\begin{align}
D_{32}^-(a)&>\frac1{1000},
&
D_{32}^+(b)&<-\frac1{10000},
\label{eq:sign-checks}\\
0<D_{32}^-(p_0)
&\le D_{32}^+(p_0)<\frac1{1000},
\label{eq:midpoint-check}\\
A_-&>0,
&
\frac{412377}{10^6}
&<L_{\rm cert}<U_{\rm cert}<\frac{412378}{10^6}.
\label{eq:value-checks}
\end{align}
\end{lemma}

\begin{proof}
These are finite rational comparisons, not transcendental
evaluations. Substitute \eqref{eq:sums} and \eqref{eq:tails}
into the displayed definitions.

For complete arithmetic reproducibility, the comparisons are
equivalently the following positive-rational checks:
\[
D_{32}^-(a)-\frac1{1000}>0,\qquad
-\frac1{10000}-D_{32}^+(b)>0,
\]
\[
D_{32}^-(p_0)>0,\qquad
\frac1{1000}-D_{32}^+(p_0)>0,
\]
\[
10^6A_- -412377\ell_+>0,
\]
\[
412378\ell_-
-10^6\left(A_++\frac1{2000000}\right)>0.
\]
All denominators in these substitutions are positive:
the series arguments are rational numbers in \([0,1)\),
and \(\ell_->0\).
Expansion and collection over their positive common denominators
gives the asserted signs. The inequality
\(D_{32}^-\le D_{32}^+\) follows directly from the nonnegative
tail terms, and \(L_{\rm cert}<U_{\rm cert}\) follows from the
definitions.

Appendix~\ref{app:checker} gives a short exact-rational
implementation of precisely these finite substitutions.
It uses no floating-point arithmetic, logarithms, numerical
root finder, or external optimizer.
\end{proof}

\begin{remark}[Arithmetic proof versus execution claim]
Lemma~\ref{lem:arithmetic} specifies the finite arithmetic
certificate explicitly. The appendix is an independent way
to check its integer comparisons. Inclusion of that code does
not assert that the code, a proof assistant, or pdfLaTeX has
been executed in preparing this response.
\end{remark}

\subsection{The completed next theorem}

\begin{theorem}[Oai276-A finite certificate]
\label{thm:finite-certificate}
For the frozen channel \(\A=\A_{1/2,1/4}\), define
\(p^\star\) to be the unique zero in
\((469/1000,47/100)\) of
\begin{equation}
\atanh\!\left(\frac34-p\right)
-
\left(p-\frac14\right)
\frac{
\atanh\sqrt{\frac58-(p-\frac14)^2}
}{
\sqrt{\frac58-(p-\frac14)^2}
}
=0.
\label{eq:pstar}
\end{equation}
Then:
\begin{enumerate}
\item \(p^\star\) is the unique global maximizer of the one-use
Holevo objective;
\item its value has the exact finite enclosure
\begin{equation}
L_{\rm cert}
\le
\chi(\A)
\le
U_{\rm cert},
\qquad
\frac{412377}{10^6}
<
\chi(\A)
<
\frac{412378}{10^6}
\quad\text{bits};
\label{eq:final-interval}
\end{equation}
\item the equiprobable pair
\begin{equation}
\phi^\star_\pm
=
\sqrt{1-p^\star}\ket0
\pm
\sqrt{p^\star}\ket1
\label{eq:optimal-pair}
\end{equation}
attains this one-use value;
\item the explicitly algebraic pair
\begin{equation}
\phi^0_\pm
=
\sqrt{\frac{1061}{2000}}\ket0
\pm
\sqrt{\frac{939}{2000}}\ket1
\label{eq:finite-pair}
\end{equation}
has Holevo information \(F_{1/2,1/4}(p_0)\), with
\begin{equation}
0\le
\chi(\A)-F_{1/2,1/4}(p_0)
<
\frac1{2000000\ln2}
<
10^{-6}\quad\text{bits}.
\label{eq:nearoptimal}
\end{equation}
\end{enumerate}
No arbitrary-partner additivity, repeated-use upper bound, or
separate-measurement optimality is a hypothesis or conclusion
of this certificate.
\end{theorem}

\begin{proof}
The series bounds and Lemma~\ref{lem:arithmetic} give
\(D(a)>0>D(b)\). Continuity and strict decrease of \(D\) give
exactly one zero in the stated interval.
By Lemma~\ref{lem:derivative} and
Proposition~\ref{prop:optimizer}, it is the unique global
maximizer.

At \(p_0\), Lemma~\ref{lem:series} gives
\(A_-\le f(p_0)\le A_+\).
The positive lower bound for \(A_-\) and \eqref{eq:ln2} imply
\[
F(p_0)\ge A_-/\ell_+.
\]
Also \(0<D(p_0)<1/1000\). Therefore
\eqref{eq:quadratic} gives
\[
\max_pf(p)
\le
A_++\frac1{2000000}.
\]
Division by \(\ln2\ge\ell_-\) proves the upper enclosure.
The strict outer interval is Lemma~\ref{lem:arithmetic}.

Theorem~\ref{thm:oneuse} supplies the exact maximizing pair
and identifies its value with \(\chi(\A)\).
The same quadratic bound gives \eqref{eq:nearoptimal}.
Finally, \(\ln2>1/2\), for example from the first term
\(\ell_-\ge2/3\), proving the last inequality.
\end{proof}

\begin{remark}[An exact real specification is not a rounded decimal]
Equation~\eqref{eq:pstar}, its isolating interval, and uniqueness
name one exact real number. The rational midpoint \(p_0\) is not
asserted to equal \(p^\star\).
A generic optimizer need not have a finite algebraic expression.
The explicitly written algebraic pair
\eqref{eq:finite-pair} is supplied when a finite preparation
description with a certified information loss is preferred.
\end{remark}

\subsection{Explicit output matrices}

The output states of the finite pair are
\begin{equation}
\rho^0_\pm
=
\begin{pmatrix}
2561/4000&
\displaystyle\pm\sqrt{\frac{996279}{8000000}}\\[4pt]
\displaystyle\pm\sqrt{\frac{996279}{8000000}}&
1439/4000
\end{pmatrix}.
\label{eq:outputs}
\end{equation}
Their average is diagonal, and
\[
\det\rho^0_\pm=\frac{1692721}{16000000},
\qquad
1-4\det\rho^0_\pm=\frac{2307279}{4000000}=q_0.
\]
These identities are direct substitutions into
\eqref{eq:channel}; they also independently check the scalar
arguments in the certificate.

The exact optimal outputs are obtained by replacing \(p_0\) by
the uniquely specified \(p^\star\):
\[
\rho^\star_\pm
=
\begin{pmatrix}
7/8-p^\star/2&
\displaystyle\pm\sqrt{\frac{p^\star(1-p^\star)}2}\\[3pt]
\displaystyle\pm\sqrt{\frac{p^\star(1-p^\star)}2}&
1/8+p^\star/2
\end{pmatrix}.
\]
This writes the binary ensemble explicitly without supplying
an asymptotic decoding circuit.

\subsection{What the certificate says about operational capacity}

The ordinary coding theorem and the one-use ensemble give the
unconditional lower bound
\[
C(\A_{1/2,1/4})
\ge
\chi(\A_{1/2,1/4})
>
\frac{412377}{10^6}.
\]
The \emph{upper} endpoint in \eqref{eq:final-interval} is an
upper bound for the one-use Holevo information. It is not
presented as an independently verified upper bound for
\(C(\A_{1/2,1/4})\).

If the external repeated-use theorem is independently established,
then Proposition~\ref{prop:conditional} transfers the same interval
to \(C\). That is an additional theorem input, not a consequence
of evaluating one scalar maximum.

\section{Stage 2: implementation, readout, and statistical pricing}
\label{sec:pricing}

\subsection{One-shot channel resources}

Use the unnormalized Choi convention
\[
J(\mathcal N)=\sum_{i,j}\kb ij\otimes\mathcal N(\kb ij).
\]
For the frozen channel,
\begin{equation}
J(\A)=
\begin{pmatrix}
7/8&0&0&1/\sqrt2\\
0&1/8&0&0\\
0&0&3/8&0\\
1/\sqrt2&0&0&5/8
\end{pmatrix}.
\label{eq:choi}
\end{equation}

\begin{proposition}[A priced coherent one-shot realization]
\label{prop:ledger}
The frozen channel has Choi rank four.
In a pure-environment isometric realization, its minimum
environment dimension is four, encodable in two qubits.
The coherent output-plus-environment interface therefore
occupies three qubits before any environmental readout.

This is a one-shot dilation ledger, not a lower bound on every
adaptive implementation or on a collective decoder's memory.
\end{proposition}

\begin{proof}
The middle diagonal entries of \eqref{eq:choi} are positive.
The determinant of its remaining two-by-two block is
\[
\frac78\frac58-\frac12=\frac3{64}>0.
\]
Thus its rank is four.

A Kraus decomposition gives \(J(\A)\) as a sum of rank-one
Kraus-vector projectors, so at least four Kraus matrices are
needed. Conversely, its spectral decomposition gives four.
The minimal pure dilation environment has that dimension.
A two-qubit environment and one output qubit attain the stated
coherent interface count.
\end{proof}

This is the model-specific use of the one-shot accounting
distinguished in Cheung's En02-A
\cite[{\texttt{thm:Dprime}}]{CheungEn02A}.
The Kraus matrices were constructed in
Lemma~\ref{lem:kraus}; they were not supplied by the resource
ledger.

A resource-certified decoder would additionally require its
actual instruction tree, complete selective maps, and live-name
ledger, as in En02-B
\cite[{\texttt{thm:B1}}]{CheungEn02B}.
No such collective decoding implementation is asserted here.

\subsection{Destructive readout is not an unknown-state decoder}

\begin{proposition}[Readout-and-drop and record-only recovery]
\label{prop:readout}
For an orthonormal basis \(\{\ket z\}\) of a measured register,
the destructive readout channel
\[
\mathcal M(X)=
\sum_z\kb zz_R\otimes
(\bra z\otimes I)X(\ket z\otimes I)
\]
satisfies
\[
\Tr_R\mathcal M(X)=\Tr_{\rm measured}X,
\]
including after every untouched reference extension.

If the only input-dependent output available to a quantum
decoder is a classical record, the decoded channel is
measure-and-prepare and cannot equal the identity on a code of
dimension at least two.
\end{proposition}

\begin{proof}
Summing the diagonal input blocks is exactly the partial trace.
The same block calculation includes a reference.

A classical-record decoder has form
\[
\Lambda(\rho)=\sum_z\Tr(E_z\rho)\sigma_z.
\]
On half of a maximally entangled input its output is separable.
The identity preserves that entanglement, so the two channels
cannot coincide.
\end{proof}

This separates complete readout from quantum recovery, as in
Landmark I, En07-A, and Hawk04-B
\cite{CheungI,CheungEn07A,CheungHawk04B}.
It is also the standard entanglement-breaking mechanism
\cite{HSR}.
It does not prohibit reliable transmission of a classical
message: a classical communication decoder is supposed to
return a classical estimate.

\subsection{A diamond allowance is not a Holevo value}

For compatible channels define
\[
\ddia(\mathcal N,\widehat{\mathcal N})
=
\frac12\|\mathcal N-\widehat{\mathcal N}\|_\diamond.
\]
The reference is included in this norm \cite{Watrous}.
Put
\[
b(\delta)=\hbin(\min\{\delta,1/2\}).
\]

\begin{proposition}[One-use information transfer under implementation error]
\label{prop:continuity}
For two qubit-output channels on the same input interface,
if \(\ddia(\mathcal N,\widehat{\mathcal N})\le\delta\), then
\[
|\chi(\mathcal N)-\chi(\widehat{\mathcal N})|
\le\min\{1,2b(\delta)\}.
\]
In particular, a certified implementation allowance for the
frozen channel gives
\[
\chi(\widehat{\A})
\in
\bigl[
L_{\rm cert}-2b(\delta),
\ U_{\rm cert}+2b(\delta)
\bigr]\cap[0,1].
\]
\end{proposition}

\begin{proof}
For qubit states, trace distance \(\delta\) bounds the difference
of their larger eigenvalues by \(\delta\), as follows from
the Bloch-vector formula and the reverse triangle inequality.

The binary entropy modulus is
\[
|\hbin(s)-\hbin(t)|\le\hbin(|s-t|).
\]
For fixed \(|s-t|\), this follows by differentiating the entropy
difference and using the decreasing derivative of binary entropy.
For a distance upper bound greater than \(1/2\), use the trivial
entropy bound one. Thus output entropy differences are at most
\(b(\delta)\).

Apply this once to the ensemble-average output and once to the
average of the conditional output entropies.
Every fixed-ensemble Holevo value changes by at most \(2b(\delta)\).
Take suprema over the same ensemble class.
Both channel Holevo informations are between zero and one.
\end{proof}

This is an actual conversion from a specified channel allowance
to a one-use information allowance. Merely quoting a diamond
budget would not perform that conversion.
The general entropy-continuity framework is due to
Fannes-type inequalities and their sharp refinements
\cite{Audenaert}.

The proposition does not by itself yield a uniform
all-block-length capacity comparison. A telescoping estimate
for \(n\) uses has allowance at most \(n\delta\), capped at one.
It cannot silently be treated as the same fixed allowance for
every block length.

\subsection{Finite statistical coverage for a specified code}

\begin{specification}[Complete attempted-run scoring]
\label{spec:statistics}
Fix one finite code, its block length, its message distribution,
and its decoder. Repeat it on independent preparations.
Each attempted run receives a predeclared score in \([0,1]\);
failure events remain in the record and receive their declared
scores. No success-only postselection or unaccounted stopping
rule is substituted.
\end{specification}

\begin{proposition}[Finite coverage is not an asymptotic rate]
\label{prop:statistics}
Let \(\overline Z_N\) be the mean of \(N\) scores under
Specification~\ref{spec:statistics}, with common expectation \(s\).
Then
\[
\Prob\left\{
|\overline Z_N-s|>
\sqrt{\frac{\ln(2/\alpha)}{2N}}
\right\}\le\alpha.
\]
If the intended and actual mean differ by at most \(e\), enlarge
the interval by \(e\). A calibration-failure probability
\(\beta\) enlarges the total failure probability to at most
\(\alpha+\beta\).
\end{proposition}

\begin{proof}
Apply Hoeffding's inequality to independent variables in
\([0,1]\), then the triangle inequality and a union bound
\cite{Hoeffding}.
\end{proof}

These are the complete-record statistical disciplines of
En01-B and En01-C on a different named statistic
\cite{CheungEn01B,CheungEn01C}.
An interval for one finite code's error does not establish a
vanishing-error sequence or an optimal asymptotic rate.

\subsection{Debugged comparison ledger}

\begin{longtable}{@{}p{.23\linewidth}p{.35\linewidth}p{.34\linewidth}@{}}
\toprule
Template & Legitimate role & Boundary or correction\\
\midrule
\endfirsthead
\toprule
Template & Legitimate role & Boundary or correction\\
\midrule
\endhead
\bottomrule
\endfoot
En02-A, \texttt{thm:Dprime} &
Pure-dilation and instrument environment accounting. &
Not a Holevo formula or a decoder construction.\\[4pt]
En02-B, \texttt{thm:B1} &
Soundness and resource accounting of a supplied finite decoder. &
Not a collective decoder for this channel.\\[4pt]
En07-A &
Complete outputs, exact-complement recovery, and
readout-and-drop. &
Its supplied \texttt{thm:exact} is a recovery criterion,
not the label of a block entropy theorem.\\[4pt]
En07-C &
External thermal data and complete-complement distinctions. &
Its supplied \texttt{thm:exact} is also a recovery criterion,
not an identification of its thermal occupation with \(\nu\).\\[4pt]
Hawk04-B; Landmark I &
Typed destructive readout and record-only recovery. &
No coding theorem follows from those facts. An unsupplied
\texttt{cor:gravity} label is not invented here.\\[4pt]
Em03-F, \texttt{thm:EB} &
A particular measure-and-prepare channel. &
It is not identified with GAD. Some GAD parameters are
entanglement breaking and some are not.\\[4pt]
Em03-G, \texttt{thm:lower} &
A positive error lower bound at each finite source parameter. &
Vanishing along growing resources requires the separate
transmission theorem, not the lower bound alone.\\[4pt]
En01-B/C &
Finite-sample coverage on complete declared records. &
Not a universally optimal channel rate.\\[4pt]
Oai272-A &
A conversation-supplied secret-bit certificate in its stated
protocol model. &
Not a classical-channel capacity theorem or a verified external
state construction.\\[4pt]
Oai265-A &
Static-record/channel/history separation. &
An area-law record is not a specified communication channel.\\[4pt]
Oai283-A &
A nominated normalization and implementation-budget comparison. &
No missing lemma is imported; a distance is not an entropy
difference until a conversion is proved.\\[4pt]
Oai290-A &
Complete-complement criteria and finite-channel comparison. &
The supplied recovery statements do not specify the present
GAD ensemble or its decoder.\\
\end{longtable}

The supplied Cheung passages support these scoped uses
\cite{CheungEn02A,CheungEn02B,CheungEn07A,CheungEn07C,
CheungHawk04B,CheungI,CheungEm03F,CheungEm03G,
CheungOai265A,CheungOai290A}.
Where the dossier only nominated a sheet, no full theorem or
unseen proof is attributed to it \cite{Dossier276}.

\section{Stage 3: existence, evaluation, and construction are distinct}
\label{sec:evaluation}

The displayed maximum in \eqref{eq:oneuse} has several different
interpretations:
\begin{enumerate}
\item continuity and compactness prove that a maximizer exists;
\item strict concavity identifies uniqueness when \(\gamma<1\);
\item an isolated derivative zero names an exact real optimizer;
\item finite rational bounds certify a value to a stated precision;
\item a preparation or decoder implementation requires additional
operations, precision, and resource data.
\end{enumerate}
These are not interchangeable.

For the frozen instance, all of items 1--4 have been supplied.
The algebraic pair \eqref{eq:finite-pair} also gives a finite
signal specification and a quantitative optimality allowance.
Its physical preparation, error budget, and the receiver's
asymptotic decoding circuit have not thereby been implemented.

The entropy, derivative, and value bounds in the certificate use
finitely many rational powers and rational divisions. Refining
their truncations decreases their explicit tails.
Thus this is more than an existence proof for the scalar
maximum. It is not a claim that the maximizer is algebraic,
or that arbitrary real channel parameters have been encoded
by a finite input representation.

Neither En02-A/B nor an oracle-synthesis template constructs
the missing scalar certificate automatically. Likewise,
same-channel additivity cannot produce an arbitrary-partner
theorem by a change of notation.

\section{Stage 4: change one hypothesis at a time}
\label{sec:hypotheses}

\subsection{Special cases are not the thermal theorem}

The one-use proof gives the following exact specializations:
\begin{align*}
\gamma=0:\quad&
\A_{\gamma,\nu}=\id,\qquad
\max_pF_{\gamma,\nu}(p)=1,\qquad p^\star=1/2;\\
\gamma=1:\quad&
\A_{\gamma,\nu}(X)=\Tr(X)\diag(1-\nu,\nu),
\qquad \chi=0;\\
\nu=0:\quad&
F_{\gamma,0}(p)
=
\hbin((1-\gamma)p)
-
\gbin(\gamma(1-\gamma)p^2);\\
\nu=1/2:\quad&
\max_pF_{\gamma,1/2}(p)
=
1-\hbin\!\left(\frac{1+\sqrt{1-\gamma}}2\right).
\end{align*}
For the unital case with \(\gamma<1\), symmetry around \(1/2\)
and strict concavity identify \(p^\star=1/2\).

Unital qubit channels have an independent additivity theory
\cite{King}; the symmetric GAD channel also has an explicit
classical-channel treatment \cite{SiddhuEtAl}.
Those special regimes do not establish every thermal parameter
or every claimed entropy inequality.

\subsection{The frozen channel is not the entanglement-breaking specimen}

\begin{proposition}[A direct non-identification check]
\label{prop:notEB}
The channel \(\A_{1/2,1/4}\) is not entanglement breaking.
\end{proposition}

\begin{proof}
The partial transpose of \eqref{eq:choi} contains the principal
block
\[
\begin{pmatrix}
1/8&1/\sqrt2\\
1/\sqrt2&3/8
\end{pmatrix},
\]
whose determinant is
\[
\frac3{64}-\frac12=-\frac{29}{64}<0.
\]
It is therefore not positive.
Every separable positive operator has positive partial
transpose, so the Choi operator is entangled.
An entanglement-breaking channel would send half of a
maximally entangled input to a separable Choi state
\cite{HSR}.
\end{proof}

This distinguishes the frozen example from Em03-F's
measure-and-prepare mechanism. It does not identify a quantum
capacity or establish optimal quantum recovery.

\subsection{Classical capacity, quantum recovery, and secrecy}

\begin{example}[Classical transmission can survive complete dephasing]
The qubit channel
\[
\Delta(X)=\kb00X\kb00+\kb11X\kb11
\]
transmits the two computational-basis symbols without error.
Thus its classical capacity is one bit per use, attaining
the qubit-output dimension bound.

It is measure-and-prepare, so no receiver-only postprocessing
recovers the identity on an unknown qubit.
The classical transmission task and unknown-state recovery
task are different even in this elementary example.
\end{example}

A density operator has distillable key, not a channel classical
capacity, unless a state-to-channel interface is explicitly
provided. Accordingly, the sentence ``a zero-key state has
positive classical capacity'' is ill-typed without that
interface. The correct separation is that a zero-key theorem
for a state/protocol pair supplies no zero upper bound on an
unrelated channel's Holevo information.

The Oai272-A conversation draft is retained only as a scoped
secret-bit comparison \cite{Oai272Draft}. It is not used to
prove any entropy statement in this manuscript.

\subsection{Collective decoding is not separate measurement}

The one-use phase-pair calculation contains no receiver POVM.
The repeated-use external record permits a collective POVM.
The inspected Lean scope explicitly excludes a theorem that
separate measurements always attain the optimum
\cite{LeanScope276}.

At the frozen interior parameters the two displayed output
states have opposite nonzero coherences and nonzero population
bias. They need not be simultaneously diagonalizable.
Their entropy difference does not by itself identify a
one-copy measurement with equal mutual information.

No separate-measurement optimum, quantum-capacity formula,
or secret-key-capacity formula is proved here.

\subsection{Hypothesis ledger}

\begin{longtable}{@{}p{.27\linewidth}p{.35\linewidth}p{.30\linewidth}@{}}
\toprule
Change or proposed inference & What actually changes & Disposition\\
\midrule
\endfirsthead
\toprule
Change or proposed inference & What actually changes & Disposition\\
\midrule
\endhead
\bottomrule
\endfoot
Replace classical messages by an unknown quantum input &
The coding criterion and target output change. &
No quantum-capacity formula follows.\\[5pt]
Require secrecy from a complementary output &
An adversary and privacy criterion are added. &
No private or secret-key formula follows.\\[5pt]
Restrict the decoder to separate measurements &
The allowed receiver class is smaller. &
A new optimality proof would be needed.\\[5pt]
Replace repeated GAD uses by an arbitrary partner &
The quantifier over channels is enlarged. &
Same-channel additivity is insufficient.\\[5pt]
Use ordinary or unital damping only &
A parameter subfamily is selected. &
The full thermal range is not proved by specialization.\\[5pt]
Replace independent uses by correlated bath noise &
The channel need not be \(\A^{\otimes n}\). &
The memoryless coding model no longer applies unchanged.\\[5pt]
Infer the coherence multiplier from population records &
Only part of the channel has been measured. &
The GAD structural promise or additional tomography is needed.\\[5pt]
Use an area law, one-round game value, or oracle budget &
The mathematical object and resource model change. &
No channel-capacity identification is supplied.\\[5pt]
Replace an asymptotic sequence by a finite confidence interval &
The quantifier over block length is removed. &
Coverage is not an asymptotic coding theorem.\\
\end{longtable}

General Holevo additivity is false; no statement in this
manuscript concerns every quantum channel
\cite{Hastings}.
The claims about external Families 265, 272, 273, 277, and 283
remain catalogue comparisons, not theorem premises
\cite{Dossier276}.

\section{Stage 5: thermal, gravitational, and recovery separations}
\label{sec:gravity}

\subsection{What the thermal parameter specifies}

The stationary qubit state for \eqref{eq:channel} is
\[
\tau_\nu=\diag(1-\nu,\nu).
\]
Indeed, \(t(\nu)=\nu\), and its coherence is zero.
This identifies a population within the specified channel.

A bosonic occupation number is a different quantity, on a
different Hilbert space. Even matching a numerical thermal
expectation does not specify the GAD coherence law, its
independence across uses, or a communication code.
The supplied En07-C and packet-state passages distinguish
thermal input data from a complete recovery channel
\cite{CheungEn07C,Dossier276}.

\subsection{Identical selected marginals do not determine a full channel}

\begin{example}[The missing coherences are an operational difference]
The channels \(\A\) and \(\A\Delta\) agree on the two
computational-basis inputs and have the same computational
population output for every input.
On the input \(\proj+\), however, their outputs differ by
\[
\begin{pmatrix}
0&k/2\\
k/2&0
\end{pmatrix},
\]
so their output trace distance is \(k/2\).
At the frozen parameters this is \(1/(2\sqrt2)>0\).

Thus the population-transition records alone do not certify
the full GAD channel. The Holevo calculation uses the coherence
term as well.
\end{example}

This is a finite instance of the complete-channel discipline
in Oai265-A, Oai290-A, and the readout manuscripts
\cite{CheungOai265A,CheungOai290A,CheungHawk04B}.
It does not transfer their model-specific decoder optima.

\subsection{No gravitational identification}

A qubit damping channel specifies input and output matrix
algebras and a CPTP map. The capacity task additionally
specifies messages, allowed coding operations, channel uses,
and decoding error. None of these data specifies:
\begin{itemize}
\item a spacetime metric or gravitational mediator;
\item a horizon, radiation algebra, or evaporation dynamics;
\item a generalized entropy functional or island extremization;
\item a gravity-generated-entanglement preparation experiment;
\item an exhaustive classical-gravity comparison family.
\end{itemize}

The same finite channel can be installed as a laboratory noise
model with no gravitational interpretation. A classical
capacity value therefore does not determine those additional
objects.

Likewise, a thermal population is not a time-indexed
radiation-entropy history. No Page curve follows from a
stationary channel parameter or from an optimized entropy
difference.

Cheung's static-record and source/readout separations are
appropriate methodological comparisons
\cite{CheungOai265A,CheungI,CheungEn07C}.
They are not missing gravitational premises supplied by the
capacity formula.

\section{Completed seven-stage release and remaining boundaries}
\label{sec:release}

\subsection{Stage-by-stage completion}

\begin{longtable}{@{}p{.07\linewidth}p{.47\linewidth}p{.38\linewidth}@{}}
\toprule
Stage & Completed object & Exact status\\
\midrule
\endfirsthead
\toprule
Stage & Completed object & Exact status\\
\midrule
\endhead
\bottomrule
\endfoot
0 &
Channel convention, units, external main claim, partner claim,
specializations, and Lean split. &
Frozen; the natural-logarithm conversion and proof-placeholder
distinction are explicit.\\[5pt]
1 &
Five-interface audit: rectangular block, thermal extension,
channel substitution, block ensemble, and arbitrary partner. &
Algebraic substitutions checked; external entropy-engine
verification is not silently imported.\\[5pt]
2 &
One-shot resource ledger, readout identity, one-use diamond
transfer, and complete-run statistical coverage. &
Local implications proved. No decoder or asymptotic rate is
manufactured from a template.\\[5pt]
3 &
Existence, exact-real optimizer specification, rational value
evaluation, and finite signal construction separated. &
The frozen evaluation is supplied, not merely proposed.\\[5pt]
4 &
Protocol and quantity changes made one at a time. &
No same-channel-to-partner, classical-to-quantum, or
population-to-channel transfer is made.\\[5pt]
5 &
Thermal, recovery, temporal, and gravitational readings
distinguished. &
No Page curve or gravitational test is constructed.\\[5pt]
6 &
One finite certificate at \((1/2,1/4)\), naming \(p^\star\),
enclosing \(\chi\), and printing two signal pairs. &
Completed by Theorem~\ref{thm:finite-certificate}.\\
\end{longtable}

\subsection{What remains outside the certificate}

Completion of the finite certificate does \emph{not} establish:
\begin{enumerate}
\item verification of the complete external 276-01 entropy proof;
\item a completed formal proof from the inspected Comparator target;
\item arbitrary-partner additivity from same-channel additivity;
\item optimality of decoding by separate measurements;
\item a quantum-capacity or secret-key-capacity formula;
\item additivity for all channels;
\item a Page curve, island, horizon, gravity-generated-entanglement
test, or exclusion of classical gravity.
\end{enumerate}

These are scope boundaries, not a claim that future work on any
of them is logically forbidden until this manuscript exists.

\subsection{The exact completed conclusion}

\[
\boxed{
\begin{gathered}
(\gamma,\nu)=\left(\frac12,\frac14\right),\\[2pt]
p^\star\text{ is the unique zero of \eqref{eq:pstar}},\qquad
\frac{469}{1000}<p^\star<\frac{47}{100},\\[2pt]
\frac{412377}{10^6}
<
\chi(\A_{1/2,1/4})
<
\frac{412378}{10^6}
\quad\text{bits},\\[2pt]
\phi^\star_\pm
=\sqrt{1-p^\star}\ket0\pm\sqrt{p^\star}\ket1,\\[2pt]
\phi^0_\pm
=\sqrt{\frac{1061}{2000}}\ket0
\pm\sqrt{\frac{939}{2000}}\ket1,
\qquad
\text{one-use loss}<10^{-6}\text{ bits}.
\end{gathered}}
\]

A finite maximum certificate is now present.
It is not the external all-block-length converse.
An entropy optimum is not a decoder circuit.
A classical transmission rate is not quantum recovery or secrecy.
A thermal parameter is not a gravitational dictionary.

\appendix

\section{Exact rational checker for the finite comparisons}
\label{app:checker}

The following optional code checks only the arithmetic comparisons
in Lemma~\ref{lem:arithmetic}. It is not a checker for the
external entropy inequalities, coding theorem, or manuscript.
Every stored number is rational. No successful execution is
asserted.

\begingroup
\small
\begin{verbatim}
from fractions import Fraction as F

ZERO = F(0)
ONE = F(1)

def L(z, n):
    return sum((z**k / F(2*k + 1) for k in range(n)), ZERO)

def T(z, n):
    return z**n / (F(2*n + 1) * (ONE-z))

def J(z, n):
    return sum(
        (z**k / F(2*k*(2*k-1)) for k in range(1, n+1)),
        ZERO
    )

def R(z, n):
    return z**(n+1) / (
        F((2*n+2)*(2*n+1)) * (ONE-z)
    )

def x(p):
    return F(3,4)-p

def d(p):
    return p-F(1,4)

def q(p):
    return F(5,8)-d(p)**2

N = 32
a = F(469,1000)
b = F(47,100)
p0 = F(939,2000)

def D_lower(p):
    xx = x(p)
    dd = d(p)
    zz = q(p)
    assert xx > 0 and dd > 0
    assert 0 <= xx**2 < 1 and 0 <= zz < 1
    return xx*L(xx**2,N)-dd*(L(zz,N)+T(zz,N))

def D_upper(p):
    xx = x(p)
    dd = d(p)
    zz = q(p)
    return xx*(L(xx**2,N)+T(xx**2,N))-dd*L(zz,N)

assert D_lower(a) > F(1,1000)
assert D_upper(b) < -F(1,10000)
assert F(0) < D_lower(p0)
assert D_lower(p0) <= D_upper(p0) < F(1,1000)

ell_lower = F(2,3)*L(F(1,9),12)
ell_upper = ell_lower + F(2,3)*T(F(1,9),12)

x0sq = F(314721,4000000)
q0 = F(2307279,4000000)

assert x(p0) == F(561,2000)
assert x(p0)**2 == x0sq
assert q(p0) == q0

A_lower = J(q0,N)-J(x0sq,N)-R(x0sq,N)
A_upper = J(q0,N)+R(q0,N)-J(x0sq,N)

assert A_lower > 0
assert ell_lower > F(1,2)

# These are the two cleared-denominator value checks.
assert 10**6*A_lower - 412377*ell_upper > 0
assert (
    412378*ell_lower
    - 10**6*(A_upper+F(1,2000000))
) > 0

Lcert = A_lower/ell_upper
Ucert = (A_upper+F(1,2000000))/ell_lower

assert F(412377,10**6) < Lcert < Ucert < F(412378,10**6)

# Independent output-matrix determinant check.
population = F(1439,4000)
coherence_squared = F(996279,8000000)
determinant = population*(1-population)-coherence_squared

assert determinant == F(1692721,16000000)
assert 1-4*determinant == q0
\end{verbatim}
\endgroup

The arithmetic cost is explicitly finite: fixed sums of at most
32 terms and fixed rational powers, followed by rational
comparisons. No efficiency theorem for arbitrary channel inputs
or exact closed-form maximizers is claimed.

\section{Source-label corrections and documentary limits}
\label{app:sources}

The comparison dossier contains theorem labels from different
manuscripts. The following corrections prevent a label from
being used for the wrong mathematical task:
\begin{itemize}
\item En07-A's supplied \texttt{thm:exact} is an exact
complete-complement recovery criterion.
\item En07-C's supplied \texttt{thm:exact} is another
complete-complement criterion, not a theorem equating a Hawking
occupation to the GAD parameter \(\nu\).
\item Em03-G's supplied \texttt{thm:lower} gives a strictly
positive lower bound at every fixed finite source parameter.
Its compatible growing-resource transmission conclusion is a
different theorem.
\item A nominated Oai283-A normalization lemma or an unsupplied
Hawk04-B corollary is not silently reconstructed from its label.
\item The Oai272-A draft in the conversation is not an
independently verified Family 272 construction and is not a
Cheung-authored theorem by virtue of its identifier.
\end{itemize}

The extensive XIV--XV--XVI passages in the supplied dossier
concern different equation spaces, distributions, reconstruction
maps, and admission problems. They are not prerequisites of this
qubit optimization. In particular, finite rational entropy
evaluation does not define their missing joint characteristic
composition.

\section*{Declarations}
\addcontentsline{toc}{section}{Declarations}

\paragraph{Mathematical claim.}
The locally proved results are the one-use formula, the frozen
finite certificate, and the stated implementation, readout, and
statistical implications. The conditional repeated-use reduction
retains its explicit hypothesis.

\paragraph{External verification.}
The external all-parameter repeated-use and arbitrary-partner
claims are recorded and audited, not independently verified in
this manuscript. A source restatement is not verification.

\paragraph{Formalization.}
The inspected Comparator target contains \texttt{sorry}.
No successful Lean build, elimination of its placeholder, or
formalization of the partner-channel corollary is asserted.

\paragraph{Computation and compilation.}
The finite inequalities have an exact-rational specification.
The appendix is supplied for reproducibility.
No executed checker log, proof-assistant run, successful
pdfLaTeX build, laboratory realization, or independently
implemented decoder is asserted.

\paragraph{Cheung citations.}
Supplied Cheung manuscripts are cited by their supplied
identifiers, versions, and relevant labels. No exhaustive corpus
inspection, proof-dependency reconstruction, or manuscript
registration is claimed.

\paragraph{Standing boundaries.}
No Page curve, island, horizon, Hawking-radiation derivation,
gravity-generated entanglement, exclusion of classical gravity,
or spacetime emergence is established. Enter is used only with
its declared destructive-readout interface.

For the separate programme described in the dossier,
\[
\boxed{
\begin{gathered}
\text{O.1 remains }\NOTCLOSED,\\
\text{the downstream XV-B admission exit is not opened},\\
\text{the remaining XVI-N obligations are not discharged},\\
\text{no inherited characteristic quantum coefficient is admitted}.
\end{gathered}}
\]
These statements do not deny the existence of technical
continuation manuscripts or replace their version-specific
results by a blanket nonexistence theorem.

\begin{thebibliography}{99}

\bibitem{OpenAI276}
OpenAI.
\emph{Classical capacity and entropy inequalities for generalized
amplitude damping}.
External Family 276-01 manuscript, dated 24 September 2026.
Main claim and arbitrary-partner corollary are documentary
records here, not independently verified inputs.
\url{https://github.com/openai/math/blob/main/preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026/build/paper.tex}

\bibitem{SourceBlock276}
OpenAI.
\emph{An entropy inequality with one zero block}.
Section \texttt{block.tex} of the Family 276-01 source.
Relevant source label: \texttt{thm:block}.
\url{https://github.com/openai/math/blob/main/preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026/build/sections/block.tex}

\bibitem{SourceThermal276}
OpenAI.
\emph{A thermal block entropy inequality}.
Section \texttt{thermal.tex} of the Family 276-01 source.
Relevant source label: \texttt{thm:thermal}.
\url{https://github.com/openai/math/blob/main/preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026/build/sections/thermal.tex}

\bibitem{SourceOutput276}
OpenAI.
\emph{From the thermal inequality to channel outputs}.
Section \texttt{output.tex} of the Family 276-01 source.
Relevant labels:
\texttt{lem:partner-branch}, \texttt{prop:pure-bound},
and \texttt{cor:mixed-bound}.
\url{https://github.com/openai/math/blob/main/preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026/build/sections/output.tex}

\bibitem{SourcePartners276}
OpenAI.
\emph{Additivity with a finite-dimensional partner}.
Section \texttt{partners.tex} of the Family 276-01 source.
Documentary proof interface for
\texttt{cor:partner-additivity}.
\url{https://github.com/openai/math/blob/main/preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026/build/sections/partners.tex}

\bibitem{LeanScope276}
OpenAI.
\emph{Classical capacity of generalized amplitude damping:
Lean scope note}.
Repository file \texttt{lean/docs/276.md}.
Consulted 14 October 2026.
\url{https://github.com/openai/math/blob/main/lean/docs/276.md}

\bibitem{LeanTarget276}
OpenAI.
\emph{AmplitudeDamping.lean}.
Repository file
\texttt{lean/ComparatorChallenges/AmplitudeDamping.lean}.
Consulted 14 October 2026.
The inspected \texttt{OAI.GAD.main} theorem body contains
\texttt{sorry}; no completed proof is inferred from this target.
\url{https://github.com/openai/math/blob/main/lean/ComparatorChallenges/AmplitudeDamping.lean}

\bibitem{HouFang}
L.-Z.~Hou and M.-F.~Fang.
The Holevo capacity of a generalized amplitude-damping channel.
\emph{Chinese Physics}
\textbf{16} (2007), 1843--1847.
doi:10.1088/1009-1963/16/7/006.
\url{https://cpb.iphy.ac.cn/article/doi/10.1088/1009-1963/16/7/006}

\bibitem{KhatriSharmaWilde}
S.~Khatri, K.~Sharma, and M.~M.~Wilde.
Information-theoretic aspects of the generalized amplitude-damping
channel.
\emph{Physical Review A}
\textbf{102} (2020), 012401.
doi:10.1103/PhysRevA.102.012401.
\url{https://arxiv.org/abs/1903.07747}

\bibitem{Wootters}
W.~K.~Wootters.
Entanglement of formation of an arbitrary state of two qubits.
\emph{Physical Review Letters}
\textbf{80} (1998), 2245--2248.
doi:10.1103/PhysRevLett.80.2245.
The entropy--concurrence scalar function is a comparison;
no formation-additivity theorem is imported.
\url{https://arxiv.org/abs/quant-ph/9709029}

\bibitem{Holevo1998}
A.~S.~Holevo.
The capacity of the quantum channel with general signal states.
\emph{IEEE Transactions on Information Theory}
\textbf{44} (1998), 269--273.
doi:10.1109/18.651037.
\url{https://arxiv.org/abs/quant-ph/9611023}

\bibitem{SchumacherWestmoreland}
B.~Schumacher and M.~D.~Westmoreland.
Sending classical information via noisy quantum channels.
\emph{Physical Review A}
\textbf{56} (1997), 131--138.
doi:10.1103/PhysRevA.56.131.

\bibitem{Watrous}
J.~Watrous.
\emph{The Theory of Quantum Information}.
Cambridge University Press, 2018.
Finite-dimensional channels, complete norms, entropy,
and channel coding conventions.
\url{https://cs.uwaterloo.ca/~watrous/TQI/}

\bibitem{King}
C.~King.
Additivity for unital qubit channels.
\emph{Journal of Mathematical Physics}
\textbf{43} (2002), 4641--4653.
doi:10.1063/1.1500791.
Preprint: \emph{Additivity for a class of unital qubit channels}.
\url{https://arxiv.org/abs/quant-ph/0103156}

\bibitem{SiddhuEtAl}
V.~Siddhu, A.~Chatterjee, K.~Jagannathan, P.~Mandayam,
and S.~Tayur.
\emph{Queue-channel capacities with generalized amplitude damping}.
Preprint, 2021.
Cited for the symmetric GAD specialization, not for a general
thermal additivity theorem.
\url{https://arxiv.org/abs/2107.13486}

\bibitem{HSR}
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: \emph{General Entanglement Breaking Channels}.
\url{https://arxiv.org/abs/quant-ph/0302031}

\bibitem{Audenaert}
K.~M.~R.~Audenaert.
A sharp continuity estimate for the von Neumann entropy.
\emph{Journal of Physics A: Mathematical and Theoretical}
\textbf{40} (2007), 8127--8136.
doi:10.1088/1751-8113/40/28/S18.
\url{https://arxiv.org/abs/quant-ph/0610146}

\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{Hastings}
M.~B.~Hastings.
Superadditivity of communication capacity using entangled inputs.
\emph{Nature Physics}
\textbf{5} (2009), 255--257.
doi:10.1038/nphys1224.
\url{https://arxiv.org/abs/0809.3972}

\bibitem{CheungI}
N.~Cheung.
\emph{Landmark I}, version 2.
Supplied manuscript \texttt{I.tex}.
Relevant items:
the structural Born/destructive-readout characterization,
record and continuation interfaces, and
\texttt{prop:classical-recovery}.
Enter Calculus Companion.

\bibitem{CheungEn02A}
N.~Cheung.
\emph{En02-A}, version 1.
Supplied manuscript \texttt{En02-A-v1.tex}.
Relevant label: \texttt{thm:Dprime}.
One-shot environment accounting and its distinction from
adaptive live-memory accounting.
Enter Calculus Companion.

\bibitem{CheungEn02B}
N.~Cheung.
\emph{En02-B}, version 1.
Supplied manuscript \texttt{En02-B-v1.tex}.
Relevant labels:
\texttt{thm:B1}, \texttt{thm:batch},
\texttt{thm:B5}, and \texttt{prop:observable}.
Resource-certified decoder soundness and named access-model
comparisons, not a GAD collective decoder.
Enter Calculus Companion.

\bibitem{CheungEn07A}
N.~Cheung.
\emph{En07-A}, version 1.
Supplied manuscript \texttt{En07-A.tex}.
Relevant supplied label: \texttt{thm:exact}.
Complete-complement recovery and separately described
readout-and-drop conventions.
Enter Calculus Companion.

\bibitem{CheungEn07C}
N.~Cheung.
\emph{En07-C}, version 1.
Supplied manuscript \texttt{En07-C.tex}.
Relevant supplied labels:
\texttt{thm:exact} and \texttt{thm:release}.
Complete-complement recovery and thermal data as external input;
no identification with the present \(\nu\).
Enter Calculus Companion.

\bibitem{CheungHawk04B}
N.~Cheung.
\emph{Hawk04-B}, version 2.
Supplied manuscript \texttt{Hawk04-B.tex}.
Relevant items: exact complete-complement recovery,
typed readout, destructive discard, and record-only
recovery limitations.
No gravitational conclusion is imported.
Enter Calculus Companion.

\bibitem{CheungEn01B}
N.~Cheung.
\emph{En01-B}, version 2.
Supplied manuscript \texttt{En01-B-v2.tex}.
Relevant label: \texttt{thm:bounded}.
Bounded complete-record statistics and uniform family 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, calibration,
and finite-sample coverage for its named statistic.
Enter Calculus Companion.

\bibitem{CheungEm03F}
N.~Cheung.
\emph{Em03-F}, version 1.
Supplied manuscript \texttt{Em03-F-v1.tex}.
Relevant labels:
\texttt{thm:EB} and \texttt{thm:recovery}.
A specified measure-and-prepare packet channel and its
referenced recovery obstruction, not GAD.
Enter Calculus Companion.

\bibitem{CheungEm03G}
N.~Cheung.
\emph{Em03-G}, version 1.
Supplied manuscript \texttt{Em03-G-v1.tex}.
Relevant labels:
\texttt{thm:lower},
\texttt{thm:compacttransmission}, and
\texttt{prop:Fobstruction}.
Fixed finite-coupling lower bounds are distinguished from
growing-resource transmission families.
Enter Calculus Companion.

\bibitem{CheungOai265A}
N.~Cheung.
\emph{Oai265-A}, supplied version 1.
Relevant labels:
\texttt{def:determination} and \texttt{thm:separation}.
Static records, selected spectra, complete channels,
and radiation histories are separate interfaces.
Enter Calculus Companion.

\bibitem{CheungOai290A}
N.~Cheung.
\emph{Oai290-A}, supplied version 1.
Relevant supplied label:
\texttt{thm:exact}, complete-complement criterion.
The dossier's finite-certificate and selected-marginal
comparisons are documentary, not a specification of the present
ensemble.
Enter Calculus Companion.

\bibitem{Oai272Draft}
\emph{Oai272-A: Finite certificates for secret-bit obstructions
and PPT-composition counterexample interfaces}.
Conversation-supplied development draft.
Cited only as a scoped comparison. No Cheung authorship,
independent source verification, or registration is asserted.

\bibitem{Dossier276}
\emph{User-supplied Oai276-A plan and comparative source dossier}.
Includes version-specific Cheung excerpts, external-family
catalogue descriptions, and comparison nominations.
Supplied retrieval label:
\texttt{178f233f (retrieval-3)}.
Not an exhaustive corpus scan, proof verification, or declaration
that nominated manuscripts are theorem premises.

\end{thebibliography}

\end{document}