slug: daly-2022-superchannel-minimal-extension-extremality
bibkey: daly2022axiomatic
doi: 10.48550/arXiv.2210.00370
url: https://arxiv.org/abs/2210.00370v1
triage: theorem
motivation_gids:
  - D5/S3/QuantumChannels/DalySuperchannelMinimalExtension.result

A non-extreme minimum-rank superchannel extension

Problem

P. C. Daly, Axiomatic Approach to Quantum Superchannels, arXiv:2210.00370v1, Remark 4.1, asks:

The set of possible superchannel extensions of a QSC is a convex set. In the example given the extensions with minimal e are extreme points. A natural question to ask is whether it is generally true that the extensions which give minimal dimensions e are extreme points.

The Library note quotes the definitions and locators. Here $e$ is exactly the source’s rank of the Choi matrix after tracing out both output factors. Convexity and extremality use real scalars. This question is the universal assertion about every minimizer; existence of some extreme minimizer is a weaker assertion.

Statement echo

All names in this table belong to D5.S3.QuantumChannels.DalySuperchannelMinimalExtension.

Fin n uses zero-based indices. Complex-linear spaces and real convex combinations express the two different scalar roles in the source; neither adds a hypothesis to the question. The input-first Choi owner used in e has the same matrix-unit expression as choi.

Motivation

In dimensions $(d_1,r_1,d_2,r_2)=(2,2,2,2)$, set $Z=\mathrm{diag}(1,-1)$, $\Omega =|00⟩+|11⟩$, and $P=|\Omega ⟩⟨\Omega |$. Define

$$F_s(X)=\frac{X}{2}+\frac{I\otimes {\mathrm{Tr}}_{A}X}{8}+\frac{\mathrm{Tr}(X)I}{16}+\frac{s\mathrm{Tr}((Z\otimes I)X)(Z\otimes I)}{32}.$$

Write $S_s=R^{-1}{F}_{s}R$, and let $\Gamma$ be the restriction of $S_0$ to $\mathrm{SCPTP}(2,2)$. Every extension of $\Gamma$ has $e=4$. The distinct extensions $S_1$ and $S_{-1}$ have midpoint $S_0$; hence this minimizer is not extreme.

Gap

Preregistration #19620 identifies Remark 4.1 as a tier-1 published question and fixes the full quantifiers, tensor maps and reduced-Choi-rank definition. Its literature screen reports the question also in Remark 3.3.1 of Daly’s thesis. Bibliographic completeness is ASSUMED-UNVERIFIED.

Route

The private theorem Rank.coherent_block_full_rank supplies the rank obstruction. For a positive semidefinite block matrix $J$, a kernel vector of its partial trace gives a positive semidefinite compression of trace zero. That compression is zero, while its prescribed off-diagonal entry is the strictly positive quadratic form of a positive definite matrix $K$. The contradiction gives full reduced rank.

The private adapters cp_iff_choi and cp_amplify are bind-only applications of MatrixMap.choi_PSD_iff_CP_map and MatrixMap.IsCompletelyPositive.of_Fintype from D5/S3/Quantum/Foundation/FiniteKrausRepresentation. The former transports positive semidefiniteness from the output-first Choi matrix through $Equiv.prodComm$; the latter supplies positivity for every finite auxiliary carrier. cp_induced_preserving consumes both adapters.

extension_fixed_coherence identifies the shared block; all_extensions_e applies the obstruction to every legal extension. super_extension provides the interval of legal extensions, and super_not_extreme uses the distinct endpoints and their midpoint. These are private proof components consumed by result.

Declaration classification

Falsifier

The refutation requires a legal QSC, two distinct legal endpoint extensions, midpoint equality and minimum rank for every extension. A CP-only construction, a statement only about the displayed family, or an alternative memory-cost definition would not refute this question. The theorem result proves the negation of the full claim.

Evidence

Kernel evidence is DalySuperchannelMinimalExtension.lean, with its Blueprint. The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9). There are no other public theorems or published owner declarations.

The experiment is the pinned numerical check. Command: /opt/homebrew/bin/python3 /Users/auric/trureturing-experiments/docs/reports/daly-2022-superchannel-minimal-extension-extremality/check.py; exit 0, RESULT PASS. Script SHA-256: cb6c4837fee13e9104a8c34e8e979230820189b2b8283b135406161fd294f394. Exact computations concern the two-qubit matrices and $s=-1,0,1$; the numerical sampling concerns 300 boundary extensions. Neither finite computation replaces the universal rank proof.

Triage

What the settlement shows

Proved in prose from the source’s convexity assertion: when the shared-block condition forces the same reduced rank for every extension, any two distinct extensions have a legal midpoint. That midpoint minimizes the rank and is not extreme. This conditional argument does not classify which QSCs have two extensions or which ones satisfy the shared-block condition.

The rank obstruction is stated for arbitrary finite carriers and a prescribed positive definite block in the private theorem; the public settlement is only the named universal question. The numerical sample makes no claim about all boundary points or all dimensions. Repository admission is separately determined by the required CI check.

ASSUMED-UNVERIFIED

The literature screen is the partial screen recorded in #19620: the preprint is read; Daly’s thesis repetition is reported there, while the published Lie–Jeong article and Wilson’s complete thesis are not verified. The inability to independently retrieve the thesis and the partial citing-work screen do not establish exhaustive novelty. No later-proof absence beyond that searched scope is asserted.

Repository reuse searches name search revision cff5748b7cf618dc1b348c18941d5b25bcdb2fcd. The mechanical sweep and supplemental exact-statement queries are bounded; some queries reach heartbeat limits. Exhaustive absence of another applicable theorem and helper-deletion/bypass retests remain ASSUMED-UNVERIFIED. Compilation and the refutation statement do not certify exhaustive reuse searches.