Oai276-A A Finite Certificate for a Generalized Amplitude-Damping Holevo Optimum One-use proof, seven-stage audit, and operational separations

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

we specify the unique maximizing population as an isolated zero of an explicit strictly decreasing derivative and prove

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.

The principal new deliverable requested by the plan is an explicit finite certificate for one frozen scalar optimization. That deliverable is Theorem 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 ({\mathcal{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 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.

The plan expressly calls for an audit without importing the external capacity theorem and for one subsequent finite certificate. Accordingly, completion has the following meaning:

1. the external claims and their quantifiers are frozen;

2. their five mathematical interfaces are audited separately;

3. comparison manuscripts are used only in their stated roles;

4. a concrete optimizer and a certified value interval are supplied;

5. unverified multi-use and partner-channel assertions remain external claims, rather than being relabelled as local theorems.

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

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

The scope note 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 LeanScope276.

There is an additional distinction. In the inspected ComparatorChallenges/AmplitudeDamping.lean, the theorem OAI.GAD.main ends with by sorry 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.

All Hilbert spaces in the mathematical arguments are nonzero and finite dimensional. Entropies in the local theorems are in bits:

with $0{\log }_{2}0=0$. Define

Natural-logarithm versions are denoted by

For a channel $\mathcal{N}$, its one-use Holevo information is

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

The operational coding input is the Holevo–Schumacher–Westmoreland theorem, not an inference from the existence of a Kraus representation Holevo1998,SchumacherWestmoreland,Watrous.

For $\gamma ,\nu \in [0,1]$, write $k=\sqrt{1-\gamma }$. The channel is

Here $\nu$ is the stationary excited-state population, not an unidentified bosonic occupation number.

A Kraus family is

The matrices in (eq:kraus) satisfy

and implement (eq:channel). Thus the formula defines a CPTP map, including all parameter endpoints.

Proof. The two diagonal contributions to the completeness sum are

The jump contributions are $\gamma (1-\nu )|1⟩⟨1|+\gamma \nu |0⟩⟨0|$. Their sum is $I_2$. Direct multiplication gives excited-state population $(1-\gamma )p+\gamma \nu$ and coherence multiplier $k$.

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

Set

Family 276 asserts, for every $(\gamma ,\nu )\in [0,1{]}^2$ and $n\ge 1$,

It further asserts that every maximizing $p$ gives attaining equiprobable phase-pair products, where

The maximum is one-dimensional; this is not a closed algebraic evaluation of its maximizer OpenAI276.

The source separately asserts, for every finite-dimensional CPTP partner $\mathcal{N}$,

The partner retains its own regularization. This quantifier is stronger than repeated uses of $\mathcal{A}$, and it is outside the inspected Lean scope OpenAI276,LeanScope276.

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 $\ln 2$. In (eq:objective), both functions are already in bits, so no further factor is present.

Neither external record is assumed in the proof of Theorem thm:finite-certificate.

For finite-dimensional states:

1. $S(\rho )\le H(\mathrm{diag}\rho )$ in any orthonormal basis;

2. $S$ is concave;

3. $S(\rho \otimes \sigma )=S(\rho )+S(\sigma )$;

4. a two-by-two state of determinant $u$ has entropy $g_2(u)$.

Proof. The diagonal is obtained from the eigenvalue vector by the doubly stochastic matrix of squared moduli of unitary entries. Concavity of $-x{\log }_{2}x$, 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 (eq:g).

The function $s\mapsto g_2(s^2)$ is nondecreasing and convex on $[0,1/2]$. Consequently,

is convex on $[0,1]$ for every $\gamma ,\nu \in [0,1]$.

Proof. It suffices to calculate in nats. For $0<u<1/4$, set

Differentiation gives

The inequality follows from $\mathrm{atanh}r\ge r$. Therefore

Continuous endpoint limits extend the conclusion to the closed interval.

Finally,

is convex. Compose it with the nondecreasing convex function just proved.

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

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,

Proof. For a pure input, $|z{|}^2=p(1-p)$, so the determinant of (eq:channel) is

Expansion gives

This is in $[0,1/4]$ because it is the determinant of a state.

For a spectral decomposition $\rho ={\sum }_a{w}_a|{\psi }_a⟩⟨{\psi }_a|$, let $p_a$ be the component populations. Entropy concavity and Lemma lem:convex give

For all $\gamma ,\nu \in [0,1]$,

At every maximizing $p$, the equiprobable pair

attains the maximum.

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

Proof. Take any ensemble $\{q_a,{\rho }_a\}$, with populations $p_a$, and put $\overline{p}={\sum }_a{q}_a{p}_a$. The average output has population $t(\overline{p})$. Lemma lem:entropy gives

Lemma lem:determinant and convexity give

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 $n{F}_{\gamma ,\nu }(p)$. No unrestricted tensor-power upper bound has been proved in this argument.

For $0\le \gamma <1$, the function $F_{\gamma ,\nu }$ is strictly concave, has a unique maximizer in $(0,1)$, and satisfies

At $\gamma =1$, the channel is a replacement channel, $F_{\gamma ,\nu }\equiv 0$, and every $p$ maximizes.

The one-use minimum output entropy is

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 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

The determinant entropy is strictly increasing in the interior, so $F_{\gamma ,\nu }(p)>0$. The unique maximum is therefore interior.

At $\gamma =1$, (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 $g_2$ prove the formula.

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$.

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.

For rectangular $A,B,C$ of the same shape, set

The source's thm:block asserts

with zero-weight terms omitted SourceBlock276.

The audit obligations are:

1. prove the inequality for noncommuting blocks;

2. retain the direction of the entropy inequality;

3. justify singular blocks without inverses of those blocks;

4. preserve the nonzero singular values under rectangular zero padding.

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.

The source's thm:thermal concerns matrices $X,Y$ with $\mathrm{Tr}X{X}^{†}=\mathrm{Tr}Y{Y}^{†}=1$ and coefficients

Its state has the form

Writing $U_0=\alpha +\beta$, $U_1=\eta +\delta$, and $u=U_0{U}_1-K^2$, the asserted bound is

The source obtains it from zero-block factorizations SourceThermal276.

The relevant algebra is

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 same scalar term $g_2(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.

The substitution itself is elementary and can be checked without assuming (eq:audit-thermal). Put

Then

For a normalized pure input

and a CPTP partner with Kraus matrices $V_{\ell }$, form rectangular matrices with columns

Their common column index gives

No orthogonality of ${\psi }_0,{\psi }_1$ is required.

The thermal coefficients are

Equation (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.

The nontrivial multi-use assertion is the lower bound

for every block state $\rho$, including entangled signals. It is not obtained by subadditivity: subadditivity has the opposite direction for a joint entropy.

Fix $(\gamma ,\nu )$. If (eq:population-bound) holds for every $n$ and every block input, then

Every maximizing phase-pair product ensemble attains the block Holevo value.

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

The assumed bound and convexity of $e$ bound the average conditional output entropy below by ${\sum }_{j}e({\overline{p}}_j)$. Subtracting gives at most $n{\max }_p{F}_{\gamma ,\nu }(p)$. Theorem thm:oneuse supplies a product ensemble attaining it. Equation (eq:regularized) then gives the capacity identity.

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

When $\chi (\mathcal{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 (\mathcal{A})$. Coding uses suitable codebooks and decoding POVMs; it is a different construction.

For a pure signal on a damping input and a partner input, the source uses the stronger branch estimate

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_a{p}_a$, have mean equal to the partner marginal of the mean full output. If (eq:partner-branch) is supplied, subtracting conditional entropies from

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 SourcePartners276.

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

From now on,

The objective in nats is

Define

The determinant eigenvalue radius is $\sqrt{q(p)}$.

For the frozen channel, $f$ is smooth on $[0,1]$ and

Moreover,

Consequently $D$ is strictly decreasing and, for every $p_0$,

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}$,

Differentiate (eq:f) and use $1-2(p/2+1/8)=x(p)$ to obtain (eq:D).

The determinant entropy term is convex by Lemma lem:convex. For the first term,

This proves (eq:curvature).

Integrating the curvature bound gives

The maximum of the quadratic on the whole real line is $f(p_0)+D(p_0{)}^2/2$, proving (eq:quadratic).

For $0\le z<1$, define

Put

For $0\le z<1$,

Also,

Therefore

Proof. Expand $1/(1-r^2)$ geometrically and integrate from zero to $r$. This gives the $\mathrm{atanh}$ series. The derivative of $\ln 2-h_{\mathrm{e}}((1+r)/2)$ is $\mathrm{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 (eq:fseries) follows because binary entropy is symmetric and $x(p)=1-2t(p)$.

Only rational arithmetic is needed when $p$ is rational. No numerical square-root evaluation is required.

Fix

For $p\in [a,b]$, both $x(p)$ and $d(p)$ are positive. Define the rational derivative bounds

Then $D_N^{-}(p)\le D(p)\le D_N^{+}(p)$.

A rational enclosure of $\ln 2$ is

Indeed, $\ln 2=2\mathrm{atanh}(1/3)$.

At $p_0$, the exact arguments are

Define

The rational numbers in (eq:certificate-data)–(eq:value-certificate) satisfy

Proof. These are finite rational comparisons, not transcendental evaluations. Substitute (eq:sums) and (eq:tails) into the displayed definitions.

For complete arithmetic reproducibility, the comparisons are equivalently the following positive-rational checks:

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_{\mathrm{cert}}<U_{\mathrm{cert}}$ follows from the definitions.

Appendix 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.

Lemma 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.

For the frozen channel $\mathcal{A}={\mathcal{A}}_{1/2,1/4}$, define $p^{\star }$ to be the unique zero in $(469/1000,47/100)$ of

Then:

1. $p^{\star }$ is the unique global maximizer of the one-use Holevo objective;

2. its value has the exact finite enclosure

   $$L_{\mathrm{cert}}\le \chi (\mathcal{A})\le U_{\mathrm{cert}},\frac{412377}{10^6}<\chi (\mathcal{A})<\frac{412378}{10^6}\text{bits};$$

3. the equiprobable pair

   $${{\varphi }^{\star }}_{\pm }=\sqrt{1-p^{\star }}|0⟩\pm \sqrt{p^{\star }}|1⟩$$

   attains this one-use value;

4. the explicitly algebraic pair

   $${{\varphi }^0}_{\pm }=\sqrt{\frac{1061}{2000}}|0⟩\pm \sqrt{\frac{939}{2000}}|1⟩$$

   has Holevo information $F_{1/2,1/4}(p_0)$, with

   $$0\le \chi (\mathcal{A})-F_{1/2,1/4}(p_0)<\frac{1}{2000000\ln 2}<10^{-6}\text{bits}.$$

No arbitrary-partner additivity, repeated-use upper bound, or separate-measurement optimality is a hypothesis or conclusion of this certificate.

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

At $p_0$, Lemma lem:series gives $A_{-}\le f(p_0)\le A_{+}$. The positive lower bound for $A_{-}$ and (eq:ln2) imply

Also $0<D(p_0)<1/1000$. Therefore (eq:quadratic) gives

Division by $\ln 2\ge {\ell }_{-}$ proves the upper enclosure. The strict outer interval is Lemma lem:arithmetic.

Theorem thm:oneuse supplies the exact maximizing pair and identifies its value with $\chi (\mathcal{A})$. The same quadratic bound gives (eq:nearoptimal). Finally, $\ln 2>1/2$, for example from the first term ${\ell }_{-}\ge 2/3$, proving the last inequality.

Equation (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 (eq:finite-pair) is supplied when a finite preparation description with a certified information loss is preferred.

The output states of the finite pair are

Their average is diagonal, and

These identities are direct substitutions into (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 }$:

This writes the binary ensemble explicitly without supplying an asymptotic decoding circuit.

The ordinary coding theorem and the one-use ensemble give the unconditional lower bound

The upper endpoint in (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({\mathcal{A}}_{1/2,1/4})$.

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

Use the unnormalized Choi convention

For the frozen channel,

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.

Proof. The middle diagonal entries of (eq:choi) are positive. The determinant of its remaining two-by-two block is

Thus its rank is four.

A Kraus decomposition gives $J(\mathcal{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.

This is the model-specific use of the one-shot accounting distinguished in Cheung's En02-A CheungEn02A ({thm:Dprime}). The Kraus matrices were constructed in Lemma 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 CheungEn02B ({thm:B1}). No such collective decoding implementation is asserted here.

For an orthonormal basis $\{|z⟩\}$ of a measured register, the destructive readout channel

satisfies

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.

Proof. Summing the diagonal input blocks is exactly the partial trace. The same block calculation includes a reference.

A classical-record decoder has form

On half of a maximally entangled input its output is separable. The identity preserves that entanglement, so the two channels cannot coincide.

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

For compatible channels define

The reference is included in this norm Watrous. Put

For two qubit-output channels on the same input interface, if $d_{\diamond }(\mathcal{N},\hat{\mathcal{N}})\le \delta$, then

In particular, a certified implementation allowance for the frozen channel gives

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

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.

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 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.

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.

Let ${\overline{Z}}_N$ be the mean of $N$ scores under Specification spec:statistics, with common expectation $s$. Then

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$.

Proof. Apply Hoeffding's inequality to independent variables in $[0,1]$, then the triangle inequality and a union bound Hoeffding.

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

The supplied Cheung passages support these scoped uses 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 Dossier276.

The displayed maximum in (eq:oneuse) has several different interpretations:

1. continuity and compactness prove that a maximizer exists;

2. strict concavity identifies uniqueness when $\gamma <1$;

3. an isolated derivative zero names an exact real optimizer;

4. finite rational bounds certify a value to a stated precision;

5. a preparation or decoder implementation requires additional operations, precision, and resource data.

These are not interchangeable.

For the frozen instance, all of items 1–4 have been supplied. The algebraic pair (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.

The one-use proof gives the following exact specializations:

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 King; the symmetric GAD channel also has an explicit classical-channel treatment SiddhuEtAl. Those special regimes do not establish every thermal parameter or every claimed entropy inequality.

The channel ${\mathcal{A}}_{1/2,1/4}$ is not entanglement breaking.

Proof. The partial transpose of (eq:choi) contains the principal block

whose determinant is

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 HSR.

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.

The qubit channel