← All papers
First page of Bath dimension and initial entropy for closed repeated use of a quantum channel

Bath dimension and initial entropy for closed repeated use of a quantum channel

Seth Douglas

quant-ph Sep 16, 2026 · v1
Ships ancillary Lean files giving a separate, partial machine-checked verification of parts of the quantum channel bath-dimension proofs, with no sorry or extra axioms.
We characterize the bath resources needed to supply repeated uses of a fixed finite-dimensional quantum channel in a closed device. For each horizon $T$, one bath, one initial state and one repeated unitary are fixed before the user. Each output is returned before the next input arrives; no reset, discard, fresh ancilla or uncounted controller is available. Approximation error must vanish against arbitrary adaptive users with quantum memory and references. Writing $r=\lim \log_2(R_T)/T$ for the bath dimension rate and $s=\lim S(ω_T)/T$ for the actual initial entropy rate, we prove that the achievable region is exactly $s\ge 0$, $r+s\ge h$ and $r-s\geκ$. Here $h$ is maximum entropy exchange and $κ$ is a smoothed independent-reference extension cost, with the zero-error limit taken before the supremum over full-rank inputs. Its exact fixed-input form is an affine transform of the zero-leakage quantum privacy funnel. The minimum dimension rate is $(h+κ)/2$. The proof combines entropy converses, a bath-dimension-independent support repair, and a closed adaptive implementation of encoder-only fully quantum Slepian–Wolf recycling. All seeds, clocks, workspace and retained residues are counted. Worked examples include dephasing, pure replacement and a qubit channel with $0<κ<h$. No computability of $κ$ or efficient circuit synthesis is claimed.

The question is what bath resources a closed device needs to implement repeated uses of a fixed finite-dimensional quantum channel. The device has no reset, discard, or fresh ancillas, and it must have vanishing error against adaptive users with quantum memory.

Two quantities are defined: the bath dimension rate r and the initial entropy rate s. Converse bounds are proved via entropy telescoping. Achievability combines a dimension-independent support repair with exactification and an encoder-only fully quantum Slepian–Wolf recycling construction. A partial Lean verification of parts of the argument is supplied as ancillary files, using only standard axioms and no sorry.

The achievable region is exactly s≥0, r+s≥h and r−s≥κ, where h is the maximum entropy exchange and κ is a smoothed extension cost. This gives a minimum dimension rate of (h+κ)/2. Worked examples cover unitary channels, dephasing, pure replacement, and a qubit channel with 0<κ<h.