Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
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.

Channel Composition Hybrid Bound

Statement

Let H0,H1,H2 be nonzero finite-dimensional complex Hilbert spaces, and let Φ0,Ψ0:L(H0)→L(H1) and Φ1,Ψ1:L(H1)→L(H2) be finite-dimensional channels. Then ∥Ψ1∘Ψ0−Φ1∘Φ0∥⋄≤∥Ψ0−Φ0∥⋄+∥Ψ1−Φ1∥⋄.

Facts & Assumptions

Given: Nonzero finite-dimensional H0,H1,H2 and four channels with the indicated domains and codomains.

[F1]

A channel is a completely positive trace-preserving linear map (Finite-dimensional quantum channel).

[L1]

The diamond norm is the supremum of induced trace norms over all finite ancillas and equals the induced norm at input dimension (Diamond Norm, Diamond Norm Ancilla Dimension Bound). The ancilla theorem is a current draft.

[L2]

Every finite trace norm satisfies its triangle inequality and the induced norm is submultiplicative under composition (Trace Norm Duality And Norm Properties).

[L3]

Each channel has diamond norm one (Channel Diamond Norm One). The QC06 supplier is draft.

[L4]

For each finite R, the operators built from products of matrix units span L(H⊗R) (Tensor products of operator matrix units form a basis); on them, factorwise tensor-map composition gives (A⊗id⁡R)∘(B⊗id⁡R)=(A∘B)⊗id⁡R (Tensor products of finitely many linear maps, Tensor maps preserve composition, identities, and adjoints).

Proof

1.1givenL1L2L4algebra

For any fixed ancillary space R, write ΛR(T)=T⊗id⁡R. By [L4], the amplification respects composition, so ∥((A∘B)⊗id⁡R)(X)∥1≤∥A⊗id⁡R∥1→1∥B⊗id⁡R∥1→1∥X∥1 for each X. Taking suprema over nonzero X and then over R proves ∥A∘B∥⋄≤∥A∥⋄∥B∥⋄. The pointwise trace-norm triangle inequality likewise gives the triangle inequality for the diamond norm.

2.1givenF1L2L3step 1.1algebra∎

The algebraic identity Ψ1Ψ0−Φ1Φ0=Ψ1(Ψ0−Φ0)+(Ψ1−Φ1)Φ0 holds on every input by expansion. Apply step 1.1 and [L3] to the two terms: the first has diamond norm at most ∥Ψ1∥⋄∥Ψ0−Φ0∥⋄=∥Ψ0−Φ0∥⋄, and the second at most ∥Ψ1−Φ1∥⋄∥Φ0∥⋄=∥Ψ1−Φ1∥⋄. The triangle inequality from step 1.1 proves the claimed sum.

Depends on

Used by

Dependency tree · two levels

44 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources