Alphabeta Math
LemmaStatement: 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.

Coherent information of a qudit erasure channel

Statement

Let Ed,ϵ be the finite-dimensional erasure channel with data dimension d≥1 and erasure probability ϵ∈[0,1], with the complementary dilation in Complement and degradation maps of the erasure channel. For every input state ρ,

Ic(ρ,Ed,ϵ)=(1−2ϵ)S(ρ).

Facts & Assumptions

Given: d≥1, ϵ∈[0,1], and the input state ρ in the Statement.

[F1]

Finite-dimensional quantum erasure channel and Complement and degradation maps of the erasure channel: respectively, the receiver state is (1−ϵ)ρ⊕ϵ∣eB⟩⟨eB∣ and the complementary state is ϵρ⊕(1−ϵ)∣eE⟩⟨eE∣ under the declared data-flag identifications.

[F2]

Coherent information equals output entropy minus environment entropy: Ic(ρ,E)=S(E(ρ))−S(Ec(ρ)).

[F3]

Entropy of a finite flagged state: S(pρ⊕(1−p)∣e⟩⟨e∣)=h(p)+pS(ρ), including p=0,1.

Proof

1.1F1F3givenalgebra

Apply [F3] to the two states in [F1]. Their entropies are h(ϵ)+(1−ϵ)S(ρ) and h(1−ϵ)+ϵS(ρ), respectively. By the definition of h and the logarithm product and reciprocal laws in Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, h(1−ϵ)=h(ϵ), including the endpoint convention 0ln⁡0=0.

2.1F2F3step 1.1algebracases∎

Subtract the complementary-output entropy from the receiver-output entropy as in [F2]. The equal binary-entropy terms from step 1.1 cancel, leaving (1−2ϵ)S(ρ). The derivation is valid at ϵ=0,1 by [F3], so no open-interval restriction is needed.

Depends on

Used by

Dependency tree · two levels

32 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