Empirical/CSD: channel capacities of the de-isolation / dephasing channel (Build 15e)

Category: 6-Local (the open-system / decoherence stratum of D1; the K1 von-Neumann-entropy reading of the de-isolation channel of 15a-d).

A dephasing (de-isolation) channel transmits CLASSICAL information but destroys QUANTUM coherence. This file gives the entropy-based, single-shot contrast on the completely-dephasing channel Φ_deph = decohereReducedN (15a, Einselection.lean), reusing the K1-A von Neumann entropy QuantumInfo.vonNeumannEntropy.

Part A: the information quantity (single-letter Holevo χ)

holevoChi2 h0 h1 havg := S(½ρ0 + ½ρ1) − (½ S(ρ0) + ½ S(ρ1)), the Holevo χ of the equal-weight two-element ensemble {(½,ρ0),(½,ρ1)}. This is the single-letter / single-shot Holevo quantity, NOT the regularized classical capacity (a limit over many channel uses with additivity, which is not formalised here).

Honest scope on the general bound. holevoChi2 ≥ 0 in general is concavity of the von Neumann entropy S(∑pᵢρᵢ) ≥ ∑pᵢS(ρᵢ). Entropy concavity is NOT in the K1 API (Subadditivity.lean proves S(ρAB) ≤ S(ρA)+S(ρB), a different statement; the SSA fork is open). So no general holevo_nonneg is asserted here; instead the headline value χ = log 2 > 0 is obtained by DIRECT computation on the concrete channel.

Part B: the classical-yes / quantum-no contrast (direct computation)

• Classical info survives. The computational-basis states |i⟩⟨i| are FIXED POINTS of Φ_deph (dephasing_fixes_basis_state, general N). For the qubit ensemble {(½,|0⟩⟨0|),(½,|1⟩⟨1|)} the Holevo χ through the channel is log 2, a full classical bit (holevo_classical_eq_log_two): S(½I) − ½·0 − ½·0 = log 2.
• Quantum coherence destroyed. The same channel maps the coherent |+⟩⟨+| to the maximally mixed ½I (dephasing_plus_eq_half_one), so a pure (zero-entropy) input becomes entropy log 2 (dephasing_destroys_coherence): the entropy jump 0 → log 2, the decoherence witness.
• dephasing_classical_vs_quantum (capstone): fixed points on the classical basis + |+⟩ → ½I + entropy jump + Holevo χ = log 2.

The entropy values are DERIVED (not gated): S(|i⟩⟨i|) = S(|+⟩⟨+|) = 0 from vonNeumannEntropy_eq_zero_of_pure; S(½I) = log 2 from the maximally-mixed value vonNeumannEntropy_const_smul_one (charpoly route, spectral_sum_eq_of_charpoly_prod).

Part C: the CSD reading and D1 gating

Channel capacity = how much Σ-volume distinguishability survives the de-isolation channel: the dephasing channel preserves the classical (pointer-basis) volume partition (fixed points) but collapses the coherent (off-diagonal) Σ-structure (the |+⟩ → ½I entropy increase). This is the operational / volume reading. The genuine ontic Σ-volume capacity (the de-isolation flow's information throughput as a property of Φ ≠ id) is D1-gated to the entangled tier (LF6); Φ = id in every concrete SectorData. No volume-capacity theorem is claimed here.

All exports are foundational-triple-only (off busch_effect_gleason): concrete Matrix spectral arithmetic on the 15a dephasing channel and the K1-A entropy.

Entropy of a scalar (maximally-mixed) state

The Cat-1 entropy facts const_smul_one_isHermitian, vonNeumannEntropy_const_smul_one (S((↑c)·I) = N·negMulLog c), and vonNeumannEntropy_maximally_mixed (S((1/N)·I) = log N, the saturating case of vonNeumannEntropy_le_log_card) live in the K1 staging tree Mathlib/QuantumInfo/Entropy.lean under namespace QuantumInfo (they are CSD-free); they are in scope here via open QuantumInfo.

theorem CSD.Empirical.CSDBridge.ChannelCapacity.vonNeumannEntropy_congr {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) (hAB : A = B) : QuantumInfo.vonNeumannEntropy hA = QuantumInfo.vonNeumannEntropy hB

Entropy is a function of the matrix only (proof-irrelevant in the Hermitian witness): A = B ⟹ S(hA) = S(hB).

The Holevo χ of a two-element equal-weight ensemble

noncomputable def CSD.Empirical.CSDBridge.ChannelCapacity.holevoChi2 {N : ℕ} {ρ0 ρ1 : Matrix (Fin N) (Fin N) ℂ} (h0 : ρ0.IsHermitian) (h1 : ρ1.IsHermitian) (havg : (↑(1 / 2) • ρ0 + ↑(1 / 2) • ρ1).IsHermitian) : ℝ

The single-letter Holevo χ of the equal-weight ensemble {(½,ρ0),(½,ρ1)}: χ = S(½ρ0 + ½ρ1) − (½ S(ρ0) + ½ S(ρ1)). This is the single-shot quantity, NOT the regularized classical capacity.

Equations

• CSD.Empirical.CSDBridge.ChannelCapacity.holevoChi2 h0 h1 havg = QuantumInfo.vonNeumannEntropy havg - (1 / 2 * QuantumInfo.vonNeumannEntropy h0 + 1 / 2 * QuantumInfo.vonNeumannEntropy h1)

Computational-basis facts (the classical ensemble)

theorem CSD.Empirical.CSDBridge.ChannelCapacity.compBasis_norm {N : ℕ} (i : Fin N) : ‖EuclideanSpace.single i 1‖ = 1

A computational basis vector has unit norm.

theorem CSD.Empirical.CSDBridge.ChannelCapacity.compBasis_entropy_zero {N : ℕ} (i : Fin N) : QuantumInfo.vonNeumannEntropy ⋯ = 0

S(|i⟩⟨i|) = 0: a computational-basis pure state has zero entropy.

Part B (classical-yes): the dephasing channel fixes the pointer basis

theorem CSD.Empirical.CSDBridge.ChannelCapacity.dephasing_fixes_basis_state {N : ℕ} (i : Fin N) : Einselection.decohereReducedN (LF2.outerProduct (EuclideanSpace.single i 1)) = LF2.outerProduct (EuclideanSpace.single i 1)

Classical info survives: |i⟩⟨i| is a fixed point of the dephasing channel. Φ_deph(|i⟩⟨i|) = |i⟩⟨i|, every N. The computational-basis density is already diagonal (outerProduct_single), so the off-diagonal-killing channel leaves it unchanged. The classical (pointer-basis) states are transmitted perfectly.

theorem CSD.Empirical.CSDBridge.ChannelCapacity.classical_avg_eq_half_one : ↑(1 / 2) • LF2.outerProduct (EuclideanSpace.single 0 1) + ↑(1 / 2) • LF2.outerProduct (EuclideanSpace.single 1 1) = ↑(1 / 2) • 1

The classical-ensemble average of the channel outputs is the maximally mixed ½I: ½|0⟩⟨0| + ½|1⟩⟨1| = ½I. The two computational-basis projectors sum to I.

theorem CSD.Empirical.CSDBridge.ChannelCapacity.classical_avg_isHermitian : (↑(1 / 2) • LF2.outerProduct (EuclideanSpace.single 0 1) + ↑(1 / 2) • LF2.outerProduct (EuclideanSpace.single 1 1)).IsHermitian

The classical-ensemble average is Hermitian (it is ½I).

theorem CSD.Empirical.CSDBridge.ChannelCapacity.holevo_classical_eq_log_two : holevoChi2 ⋯ ⋯ classical_avg_isHermitian = Real.log 2

The classical Holevo χ is a full bit: χ = log 2. For the computational-basis ensemble {(½,|0⟩⟨0|),(½,|1⟩⟨1|)}, which the dephasing channel transmits as fixed points (dephasing_fixes_basis_state), the single-letter Holevo quantity is S(½I) − ½·0 − ½·0 = log 2. The full classical bit survives the de-isolation.

Part B (quantum-no): the dephasing channel destroys coherence

theorem CSD.Empirical.CSDBridge.ChannelCapacity.degenerateWitness_norm : ‖Einselection.degenerateWitness‖ = 1

The coherent state |+⟩ = degenerateWitness has unit norm.

theorem CSD.Empirical.CSDBridge.ChannelCapacity.plus_entropy_zero : QuantumInfo.vonNeumannEntropy ⋯ = 0

S(|+⟩⟨+|) = 0: the coherent input is a pure (zero-entropy) state.

theorem CSD.Empirical.CSDBridge.ChannelCapacity.dephasing_plus_eq_half_one : Einselection.decohereReducedN (LF2.outerProduct Einselection.degenerateWitness) = ↑(1 / 2) • 1

Quantum-no: the dephasing channel maps the coherent |+⟩⟨+| to ½I. Φ_deph(|+⟩⟨+|) = ½I (the maximally mixed qubit): the off-diagonal coherences of the equal-population superposition are killed, sending the pure input to the fully mixed state. Reuses decohereReducedN_outerProduct (the channel on a pure density) + degenerateWitness_decohere_half (15a, the qubit dephasing computation).

theorem CSD.Empirical.CSDBridge.ChannelCapacity.dephasing_plus_output_isHermitian : (Einselection.decohereReducedN (LF2.outerProduct Einselection.degenerateWitness)).IsHermitian

The dephased coherent output Φ_deph(|+⟩⟨+|) = ½I is Hermitian.

theorem CSD.Empirical.CSDBridge.ChannelCapacity.dephasing_plus_output_entropy : QuantumInfo.vonNeumannEntropy dephasing_plus_output_isHermitian = Real.log 2

The dephased coherent output has entropy log 2. S(Φ_deph(|+⟩⟨+|)) = S(½I) = log 2: the maximally mixed qubit's maximal entropy.

theorem CSD.Empirical.CSDBridge.ChannelCapacity.dephasing_destroys_coherence : QuantumInfo.vonNeumannEntropy ⋯ = 0 ∧ QuantumInfo.vonNeumannEntropy dephasing_plus_output_isHermitian = Real.log 2 ∧ QuantumInfo.vonNeumannEntropy ⋯ < QuantumInfo.vonNeumannEntropy dephasing_plus_output_isHermitian

THE decoherence witness: coherence destroyed, entropy jumps 0 → log 2. The pure coherent input |+⟩⟨+| (entropy 0) is sent by the dephasing channel to the maximally mixed ½I (entropy log 2): the strict entropy increase S(|+⟩⟨+|) = 0 < log 2 = S(Φ_deph(|+⟩⟨+|)). The channel cannot preserve the superposition: quantum coherence is destroyed. Connects to 15a (decohere_not_diagonal_in_rotated_basis, the off-diagonal-killing) and the LF6-B.2 purity drop.

Capstone

theorem CSD.Empirical.CSDBridge.ChannelCapacity.dephasing_classical_vs_quantum : (∀ (i : Fin 2), Einselection.decohereReducedN (LF2.outerProduct (EuclideanSpace.single i 1)) = LF2.outerProduct (EuclideanSpace.single i 1)) ∧ Einselection.decohereReducedN (LF2.outerProduct Einselection.degenerateWitness) = ↑(1 / 2) • 1 ∧ QuantumInfo.vonNeumannEntropy ⋯ = 0 ∧ QuantumInfo.vonNeumannEntropy dephasing_plus_output_isHermitian = Real.log 2 ∧ holevoChi2 ⋯ ⋯ classical_avg_isHermitian = Real.log 2

Build 15e capstone: classical information survives, quantum coherence destroyed. For the completely-dephasing (de-isolation) channel Φ_deph = decohereReducedN:

1. classical-yes — the computational-basis states are FIXED POINTS, Φ_deph(|i⟩⟨i|) = |i⟩⟨i| for every i (dephasing_fixes_basis_state);
2. quantum-no — the coherent |+⟩⟨+| is mapped to the maximally mixed ½I (dephasing_plus_eq_half_one);
3. the coherent input is pure, S(|+⟩⟨+|) = 0 (plus_entropy_zero);
4. its dephased output is maximally mixed, S(½I) = log 2 (dephasing_plus_output_entropy): the entropy jump 0 → log 2;
5. the single-letter Holevo χ of the classical basis ensemble is a full bit, χ = log 2 (holevo_classical_eq_log_two).

The contrast is single-shot Holevo / coherent-information, NOT the regularized capacity. The CSD reading: the de-isolation channel preserves the classical (pointer-basis) Σ-volume partition but collapses the coherent off-diagonal Σ-structure; the ontic Σ-volume capacity (throughput of Φ ≠ id) is D1-gated to the entangled tier (LF6). Foundational-triple-only.