CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Transpose positivity fails ancillary positivity

Statement refuted

Every complex-linear positive trace-preserving map between finite matrix algebras is completely positive.

Facts & Assumptions

Given: The standard ordered basis of $C^{2}$ , finite matrix transpose $T (X) = X^{T}$ , and the finite channel definitions.

[F1]

Finite completely positive trace-preserving maps: a positive map sends positive semidefinite inputs to positive semidefinite outputs; complete positivity additionally requires positivity of ${id}_{r} \otimes Φ$ for every finite $r$ .

[F2]

Finite matrix spectral and state calculus: every positive semidefinite finite matrix has a positive square root, finite Hermitian matrices have spectral decompositions, and the finite trace is cyclic.

[F3]

Complete finite Choi-Kraus equivalence: with the unnormalized Choi matrix $J (Φ) = \sum_{i, j} E_{i j} \otimes Φ (E_{i j})$ , a finite map is completely positive if and only if $J (Φ) \geq 0$ .

Counterexample

1.1givenF1F2algebra

The transpose is complex-linear and preserves trace because it fixes the diagonal entries. For any $X \geq 0$ , [F2] gives $X = Y Y^{*}$ for some matrix $Y$ ; hence $T (X) = X^{T} = \overline{Y} Y^{T} = \overline{Y} (\overline{Y})^{*} \geq 0$ . Thus $T$ is positive and trace-preserving.

2.1givenF3step 1.1algebra∎

Its Choi matrix is $J (T) = \sum_{i, j = 0}^{1} E_{i j} \otimes E_{j i}$ , the swap operator $F (∣ a ⟩ \otimes ∣ b ⟩) = ∣ b ⟩ \otimes ∣ a ⟩$ . For $η = (∣ 0 ⟩ \otimes ∣ 1 ⟩ - ∣ 1 ⟩ \otimes ∣ 0 ⟩) / \sqrt{2}$ , one has $F η = - η$ ; therefore $J (T) \geq̸ 0$ . By [F3], $T$ is not completely positive.

Transpose positivity fails ancillary positivity

Statement refuted

Facts & Assumptions

Counterexample

Depends on

Dependency tree · 2 levels

Sources