Metadata
slug: sekatski-guryanova-kothakonda-skotiniotis-2025-amplitude-damping-measure-prepare-cloning
bibkey: sekatskiguryanovakothakondaskotiniotis2025cloning
doi: 10.48550/arXiv.2509.08059
url: https://arxiv.org/abs/2509.08059v1
triage: theorem
motivation_gids:
- D5/S3/Quantum/QuantumChannels/AmplitudeDampingMeasurePrepareCloning.result
No finite measure-and-prepare process perfectly clones the amplitude-damping family
Problem
P. Sekatski, Y. Guryanova, N. B. T. Kothakonda and M. Skotiniotis, Cloning Quantum Channels, arXiv:2509.08059v1 (2025), Section V, amplitude-damping channels, performance comparison, state:
In particular, it achieves ${\rm F}_{\rm CJ}^{\ADset|\rm coh}=1N=M$, which, for amplitude-damping channels, we conjecture to be impossible for any measure-and-prepare process.
This quotation is from the downloaded v1 source arxiv_v1.tex, lines 1684–1685, md5 abcdd29ea99d1c5adf0206c6b9a9d211. The source macro \ADset denotes the amplitude-damping family; the coherent process is the subject of “it”. The arXiv abstract page supplies the arXiv-issued DOI in the front matter.
The source defines measure-and-prepare processes as a measurement consuming channel queries, followed by an outcome-dependent global -qubit channel preparation (TeX lines 1094–1103). Its preparations need not be tensor powers of an estimated channel; that narrower class is introduced separately at lines 1105–1115.
Issue #20683 fixes the target as impossibility of one such process reproducing for every , at . This is proved for finite outcome sets with the trace-pairing interpretation specified below. The compiled statement also allows every and every independently.
Precisely, the module defines the following objects:
adChoiis the unnormalized, reference-first Choi matrix of the source’s Kraus operators and (source TeX lines 1538–1553). Its entry at is .D5.S3.Quantum.Recovery.ProductPrefixRigidity.productMap (H := fun _ => Fin 2 × Fin 2) (fun _ : Fin n => J_γ)supplies the coordinate tensor power: for assignments , its entry is . At this is the one-dimensional matrix with entry one.IsChannelChoirequires a preparation matrix to be positive semidefinite and to have reference marginal equal to the identity: , where and each pair denotes its sitewise assignment.claimsays that, for every pair of natural numbers with , there are no finite , fixed complex matrices on the -fold Choi space and fixed preparation matrices on the -fold Choi space satisfyingIsChannelChoi, such that for every the numbers are real and nonnegative, sum to one, and satisfy . The real nonnegative requirement is expressed using the complex order. No further positivity or tester constraints are imposed on .
The definitions and the source quotations are also described in the literature note.
Motivation
The conjecture asks whether passing the unknown channels coherently can achieve an exact task that extracting a classical outcome and preparing a channel cannot. The source’s coherent construction retains the queried channels and is exact at (TeX lines 1639–1658). A finite-outcome impossibility result supplies the corresponding obstruction to measure-and-prepare realization, including arbitrary global preparations rather than only copies of an estimate. Exactness is a separate question from the source’s approximate cloning rates and numerical comparisons.
Gap
The bounded literature check recorded in #20683 reports:
- arXiv lists only v1, whose conjecture remains in the source text;
- INSPIRE record 2968672 lists four citing works, arXiv:2610.06723, 2607.29054, 2606.25124 and 2603.23628, with no settlement identified; OpenAlex W4416069009 reports zero citations;
- MathDB searches by title words and author surnames and a search of google-deepmind/formal-conjectures found no matching problem;
- the recorded search of
Problems/,Library/and repository issues found no prior record on dev.
The v1 text and the single-version listing are directly checked. The other readings retain the attribution and limits of the issue report.
not-found-in-searched-scope.
Route
Put with , and write . In the ordered basis this unnormalized matrix is , with and .
- One-qubit reduction. For , fix the last reference inputs to zero and trace their output sites. This sends every global channel Choi matrix to a qubit channel Choi matrix and sends to . It commutes with finite weighted sums.
- Extremality. In a decomposition with nonnegative weights and channel Choi matrices, every summand of nonzero weight annihilates the kernel vectors and of . Positivity gives these kernel relations; Hermitian symmetry and the identity reference marginal determine all remaining entries, forcing that summand to equal . This includes and .
- Polynomial probabilities. Every entry of is polynomial in . Thus is the evaluation of a complex polynomial. If it is nonzero, the fixed must equal . The entry of is , so this can occur at at most one point for each outcome.
- Contradiction. Each outcome polynomial vanishes on the interval except possibly at one point, hence has infinitely many roots and is zero. At , equivalently , all outcome weights are therefore zero, contradicting their sum being one.
Falsifier
The settlement would not answer the preregistered reading if the matrices or the measurement representation changed the task. The relevant boundaries are:
- Normalization. The source defines channel fidelity through normalized Choi states (TeX lines 400–407). The module uses , of trace two and reference marginal ; the source’s state is , and its -qubit target is . Scaling both sides preserves equality. Identifying fidelity one with equality of the normalized Choi states, and hence equality of channels, is an interpretive bridge, not a declaration of this module.
- Measurement stage. Applying the result to a physical finite-outcome -query tester assumes that each probability has the form for a fixed matrix , with any convention-dependent transpose or scaling absorbed into . This tester representation is a modeling premise in #20683, not a theorem of the module. In particular, is not restricted to a POVM obtained by measuring parallel Choi states.
- Preparations and outcomes. Preparations are arbitrary positive semidefinite global Choi matrices with the identity reference marginal. They are fixed independently of . The outcome set is exactly finite, indexed by
Fin L; arbitrary continuous outcome spaces are not quantified over. - Exactness. The conclusion excludes one process that is exact throughout . It does not provide a quantitative fidelity deficit uniform over processes or a strict upper bound on their fidelity supremum.
Evidence
The canonical source is D5/S3/Quantum/QuantumChannels/AmplitudeDampingMeasurePrepareCloning.lean (258 lines).
- Proof. It proves
result : claim. - Axioms. It uses only the standard axioms
propext,Classical.choiceandQuot.sound; nosorry,native_decide, or new axiom.
Frozen state: Golden/Frozen/state/D5/S3/Quantum/QuantumChannels/AmplitudeDampingMeasurePrepareCloning.lean.json, statement sha256:7e7bdea6c385b54c5bc13eeb1bfd75c72c021137e234c6b70c839654d65982bd.
Declaration statements:
result:sha256:37c62e80be4817f0ea53a2bf11fe854fd1b42cca1ffb84c29ffe807c2c542658;claim:sha256:7cc9162707ea84842faf01e9ec6a62dac85b70369dc7650876f52d6164ad3f96.
Triage
Tier 1 conjecture of a 2025 preprint, preregistered in issue #20683 before any Lean.
theorem; resolution proved.
The module is admitted under the open-problem-resolution basis of CLAUDE.md §3.2; the per-declaration proof shapes are listed in the delivery PR. There is no digestion atom.
What the settlement shows
Proved by result: for every natural query count , including zero, and every natural output count , no finite family of fixed matrices and global channel Choi preparations has nonnegative trace-pairing weights summing to one and weighted output equal to for every .
Computed, not formalized. None. No numerical computation is reported here; #20683 records no numerical cloning test.
Argued, not formalized.
- Decisive mechanism and extension. The obstruction is already present in one output channel: extremality prevents averaging different fixed preparations into an amplitude-damping target. In fact, for finite outcomes, the same extremality gives a stronger prose argument that needs no polynomial assumption on the weights. For each , normalization supplies an outcome of positive weight, whose reduced preparation must be . Consequently the finite set of reduced preparations would have to contain the infinitely many distinct . This is impossible. The argument applies to any infinite subfamily of distinct amplitude-damping channels and to arbitrary nonnegative normalized weight functions; that extension is not the type of
result. - Boundaries and sharpness. Positive output count is essential: at , one scalar tester and one scalar preparation, both equal to one, give weight one and the empty target exactly. Nor does impossibility for the entire interval imply impossibility for every restricted family. For the two-point family , one query on input gives or , respectively. Measuring in that basis identifies the channel and permits any number of perfect prepared outputs. These are explicit mathematical constructions, not additional compiled declarations.
- Neighbouring questions. The formal result covers arbitrary finite and all positive , including , and . It supplies no numerical approximation bound. Removing the finite-outcome restriction, proving the tester and fidelity bridges in Lean, and bounding the optimal fidelity away from one remain outside this settlement; no conclusion on those questions is asserted.
- Effect on the paper. With the stated tester and fidelity bridges, the conjectured exactness separation at is established for finite-outcome processes: the coherent construction is exact, while each such measure-and-prepare process misses at least one amplitude-damping channel. The source’s approximate comparisons near (TeX lines 1687–1695), its separate SDP/PPT comparison for (lines 1088 and 2898–2912), and its asymptotic replication estimates (lines 1574–1607 and 1673–1679) receive no quantitative verification from this result. No theorem conditional on the conjecture is identified in the source’s performance-comparison and conclusion passages (lines 1662–1771); the settlement supplies the exact finite-outcome separation proposed there.
Application to finite adaptive testers in a fixed causal order
The existing quantum-network source
supplies the following modeling bridge for the operational class specified
here. This is an ordinary source-backed application of its comb results
to claim, not an additional declaration or kernel verification. The
formal statement and evidence above retain their stated scope.
Operational assumptions. Fix finite , finite , finite input and output spaces , and fixed product bases. There are exactly chronological slots, each invoking the same unknown memoryless CPTP map . Every invocation has fresh inaccessible environment: a device with persistent hidden memory need not meet this contract. The initial state, finite-dimensional quantum memories, finite classical record registers, controls and final measurement are fixed independently of . A fixed finite adaptive policy may condition controls on earlier records. Its record probabilities depend on ; its control table does not. The final outcome set is , with all outcomes, including failures, retained and total probability one. There is no source-dependent postselection in this normalized tester.
After outcome , prepare a fixed global CPTP channel , independently of the unknown parameter and with no further call to . For the cloning application, and . These are channel preparations, not preparations of Choi states, and need not be tensor powers of a one-qubit channel.
Source and convention map. CDP §II.A, Eqs. (1)–(4) and Lemmas 1 and 3, use the unnormalized output-first operator . The module instead uses
Thus , with no normalization factor. The two conventions differ by a swap, not a partial transpose. Label the tested ports , , and choose the source factor order
The module’s sitewise assignment coordinates correspond to . Fix the real permutation unitary by
Disjoint memoryless channel slots have tested comb
by the link product on disjoint ports (CDP §II.B, Eq. (15)). This tensor expression describes the inserted process; the adaptive surrounding circuit need not run in parallel.
CDP Corollary 2 and Eq. (38) give the forward composition-to-probability rule. Definition 11/Eq. (66), Lemma 8 and Theorem 11 (§IV.E, PDF p. 17) characterize and realize the finite testers: the surrounding experiment has fixed with
Here is full ordinary matrix transpose in the fixed product basis, not an adjoint or a partial transpose. All are independent of . Finite adaptive records can be included as orthogonal memory states: an instrument writes a record, and later fixed CPTP controls read it. Coarse-graining the final histories sums positive tester elements. This is within CDP’s finite-dimensional network and instrument realization (§III.C, Theorems 3–4; §IV.D, Definition 10 and Theorem 10).
Causal normalization. Use Lemma 8 with the general deterministic comb recursion, CDP Eq. (25), equivalently Theorem 5/Eq. (40). The tester’s own ports are . Removing these scalar endpoints gives
where, for , acts on , and on . Consequently, with ,
Each . These identities are obtained by the stated port relabeling of the general recursion; the pairing consistently follows Eqs. (38) and (66). They are not the ordinary POVM condition . Indeed, for a deterministic tested comb, . In the total pairing, first trace , then use , and repeat. The total reduces to . Positive and make the weights real and nonnegative. At the normalization is , with a density matrix.
The single-slot super-instrument source also gives this scalar-output pairing and its parallel grouped-slot specialization. Its common-preprocessor theorem is not being used as an adaptive -slot theorem.
Application to the existing obstruction. Let ,
with the fixed shuffle to sitewise reference/output coordinates.
Positivity and are exactly
IsChannelChoi at the chosen . Linearity gives
Physical testers therefore supply a sufficient subclass of the
module’s allowed arbitrary : they obey additional positivity
and causal normalization that claim does not require.
Specialize to amplitude damping.
Under the operational assumptions above, result excludes a single
such measure-and-prepare process reproducing
for every ,
for any finite and , including .
For , the separate scalar pairing
, with fixed normalized
probabilities, connects the same no-query class to claim.
This supplies the stated tester modeling premise for this finite operational class; its physical-to-matrix correspondence remains an ordinary derivation outside the Lean module. Theorem 11’s existence of a realization supplies no bound meeting a separately prescribed memory, gate, time or efficiency budget. No continuous outcomes, unbounded records, infinite memory, indefinite causal order, coherently controlled unknown dilation or fidelity gap/rate are included. Retaining and normalizing only successful outcomes would change the probability contract; failures here remain part of the deterministic mixture. The native same-source state task in VIII, §§248–250 has no supplied callable-channel interface. This application grants it no queries, state-to-channel conversion or resources and settles neither its uniform conditional error nor its polynomial original success .
ASSUMED-UNVERIFIED
The bounded literature check does not establish exhaustive worldwide novelty or priority. The INSPIRE, OpenAlex, MathDB, formal-conjectures, citing-work and historical repository-search readings are reported in #20683 and are not independently reproduced. The source reading covers arXiv:2509.08059v1; no journal publication is identified on its abstract page. The DOI is the arXiv-issued DOI, recorded also in the Library note.
The representation of physical testers by fixed trace-pairing matrices, the correspondence between positive Choi matrices with identity reference marginal and physical channel preparations, and the fidelity-one/equality bridge are not formalized in this module. No reduction of arbitrary continuous-outcome measure-and-prepare processes to its finite-outcome statement is established. The stronger arbitrary-weight and infinite-subfamily argument, the boundary constructions, and the consequences for the source under the modeling bridges are prose arguments, not additional formal results. No uniform fidelity gap, optimal fidelity, asymptotic rate, continuous-outcome impossibility, or SDP numerical reading is verified by the settlement.