Symmetric coherent-information baseline in three depolarizing conventions

Definition

DepolarizingCoherentInformationBaseline

by lisamegawatts · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

coherent-informationdefinitionsdepolarizing-channelquantum-information

Define the scalar closed-form one-copy symmetric coherent-information baseline in nats using total Pauli error q, and derive the corresponding functions of per-Pauli error r and mixing probability p. The source paper states the same baseline in bits; this definition uses the positive Real.log 2 rescaling required by Mathlib’s natural-log entropy. The Lean definitions are total functions on ℝ; physical parameter ranges are part of the interpretation, and no equality with coherent information derived from a formal quantum-channel model is claimed here.

Definition code

import Mathlib.Analysis.SpecialFunctions.BinaryEntropy

namespace DepolarizingCoherentInformation

noncomputable def symmetricIcTotalPauli (q : ℝ) : ℝ :=
  Real.log 2 - Real.qaryEntropy 4 q

noncomputable def symmetricIcPerPauli (r : ℝ) : ℝ :=
  symmetricIcTotalPauli (3 * r)

noncomputable def symmetricIcMixing (p : ℝ) : ℝ :=
  symmetricIcTotalPauli (3 * p / 4)

end DepolarizingCoherentInformation

Source

Artus Krohn-Grimberghe, arXiv:2608.15870v2, §§2–3 (channel conventions and maximally mixed one-copy coherent-information formula); Mathlib Real.qaryEntropy.

Read-back

What the Lean code literally says, in plain math · codex-gpt-5

The code defines three total real-valued functions on all real inputs. Writing $H_4(x)=x\log 3-x\log x-(1-x)\log(1-x)$ for the real $4$ -ary entropy used here, it specifies, for every $q,r,p\in\mathbb{R}$ , that $I_{\mathrm{total}}(q)=\log 2-H_4(q)$ , $I_{\mathrm{per}}(r)=I_{\mathrm{total}}(3r)$ , and $I_{\mathrm{mixing}}(p)=I_{\mathrm{total}}(3p/4)$ . There are no hypotheses or domain restrictions, so these definitions also apply when their arguments, including $3r$ and $3p/4$ , lie outside $[0,1]$ ; the logarithm is the total real logarithm, with $\log 0=0$ and $\log x=\log|x|$ for negative $x$ .

View graph