The single-letter Holevo capacity of the de-isolation channel is one bit

Category: 3-Local (W10 of specs/qit-chain-scoping.md).

Empirical/CSD/ChannelCapacity.lean computed, for the bare dephasing map, that the classical bit ensemble carries a Holevo quantity of log 2 and that a coherent input loses a bit of entropy: an example of a capacity, on a posited map. With W5–W7 the de-isolation channel is a genuine QuantumInfo.Channel produced by LF5's flow, and with W8 the Holevo bound is a theorem. This module states the capacity as a theorem:

• deisolationChannel_apply_eq_decohereReducedN — on Hermitian inputs the de-isolation channel is the empirical dephasing map, so every computation of ChannelCapacity.lean transfers;
• deisolationChannel_apply_single — it fixes the computational-basis states;
• ★ holevoChi_classicalBit_deisolation — the classical bit ensemble has Holevo quantity log 2 through it;
• ★★ deisolationChannel_holevoCapacity — log 2 is the greatest single-letter Holevo quantity any ensemble of qubit density matrices achieves through the de-isolation channel (IsGreatest (holevoRange (deisolationChannel 2)) (log 2)): the Holevo bound caps every ensemble, the classical bit attains it. One classical bit, the pointer-basis bit, is what the channel transmits.

Honest scope

Single-letter (one channel use). The regularised classical capacity is a limit over many uses with an additivity question, not defined in the corpus. The channel is the environment marginal of LF5's measurement flow (LF6/MeasurementFlowChannel.lean); that reading is inherited, with its hypotheses (the flow projects to the measurement flow; the preparation is a product with the apparatus ready).

References: specs/qit-chain-scoping.md (W10, W8); Mathlib/QuantumInfo/HolevoBound.lean; Empirical/CSD/ChannelCapacity.lean; LF6/DecoherenceChannel.lean; Thermo/SigmaSecondLaw.lean (deisolationChannel_apply_eq_pinch).

The de-isolation channel's single-letter Holevo capacity is one bit

theorem CSD.LF6.deisolationChannel_apply_eq_decohereReducedN {N : ℕ} [NeZero N] {ρ : Matrix (Fin N) (Fin N) ℂ} (hρ : ρ.IsHermitian) : (deisolationChannel N).apply ρ = Empirical.CSDBridge.Einselection.decohereReducedN ρ

The de-isolation channel acts on Hermitian inputs as the empirical dephasing map decohereReducedN (diagonal restriction).

theorem CSD.LF6.deisolationChannel_apply_single {N : ℕ} [NeZero N] (i : Fin N) : (deisolationChannel N).apply (LF2.outerProduct (EuclideanSpace.single i 1)) = LF2.outerProduct (EuclideanSpace.single i 1)

The de-isolation channel fixes the computational-basis states.

noncomputable def CSD.LF6.classicalBit : Fin 2 → Matrix (Fin 2) (Fin 2) ℂ

The classical bit ensemble {(½, |0⟩⟨0|), (½, |1⟩⟨1|)}, as a Fin 2-indexed ensemble.

Equations

• CSD.LF6.classicalBit i = CSD.LF2.outerProduct (EuclideanSpace.single i 1)

theorem CSD.LF6.classicalBit_posSemidef (i : Fin 2) : (classicalBit i).PosSemidef

theorem CSD.LF6.classicalBit_trace (i : Fin 2) : (classicalBit i).trace = 1

theorem CSD.LF6.classicalBit_avg : ∑ i : Fin 2, ↑((fun (x : Fin 2) => 1 / 2) i) • classicalBit i = ↑(1 / 2) • 1

The equal-weight average of the classical bit ensemble is ½ I.

theorem CSD.LF6.holevoChi_classicalBit_deisolation : QuantumInfo.holevoChi (fun (x : Fin 2) => 1 / 2) ⋯ ⋯ = Real.log 2

★ The Holevo quantity of the classical bit ensemble through the de-isolation channel is log 2: the channel fixes the ensemble, its average is ½ I with entropy log 2, and the components are pure.

theorem CSD.LF6.deisolationChannel_holevoCapacity : IsGreatest (QuantumInfo.holevoRange (deisolationChannel 2)) (Real.log 2)

★★ The single-letter Holevo capacity of the de-isolation channel is one classical bit. log 2 is the greatest single-letter Holevo quantity any ensemble of qubit density matrices achieves through deisolationChannel 2 — the Holevo bound caps every ensemble at log 2, and the classical bit ensemble attains it. The channel is the environment marginal of LF5's de-isolation flow (LF6/MeasurementFlowChannel.lean), so this is a statement about what a Σ-flow transmits: the pointer-basis bit in full, and nothing more.