Reconcile per-Pauli, total-Pauli, and mixing conventions

Proved

DepolarizingCoherentInformation.convention_equivalence

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

depolarizing-channelparameter-conventionsquantum-information

For every real per-Pauli parameter r, prove that evaluating the per-Pauli baseline at r and the mixing baseline at p = 4r both agree with the total-Pauli baseline at q = 3r. This is the convention bridge needed before importing numerical or interval certificates.

Preamble

import Definitions.Def_DepolarizingCoherentInformationBaseline

Formal statement

namespace DepolarizingCoherentInformation

theorem convention_equivalence (r : ℝ) :
    symmetricIcPerPauli r = symmetricIcTotalPauli (3 * r) ∧
      symmetricIcMixing (4 * r) = symmetricIcTotalPauli (3 * r) := by
  sorry

end DepolarizingCoherentInformation

Source

Artus Krohn-Grimberghe, arXiv:2608.15870v2, §§2–3 (per-Pauli, total-error, and affine/mixing conventions).

Read-back

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

For every real number $r$ , with $T(q):=\log 2-\operatorname{qaryEntropy}(4,q)$ , $P(x):=T(3x)$ , and $M(x):=T\!\left(\frac{3x}{4}\right)$ , where $\log$ is the real logarithm and $\operatorname{qaryEntropy}(4,q)$ is the real $4$ -ary entropy function, the theorem asserts the conjunction $P(r)=T(3r)$ and $M(4r)=T(3r)$ ; fully unfolded, this is $\log 2-\operatorname{qaryEntropy}(4,3r)=\log 2-\operatorname{qaryEntropy}(4,3r)$ together with $\log 2-\operatorname{qaryEntropy}\!\left(4,\frac{3(4r)}{4}\right)=\log 2-\operatorname{qaryEntropy}(4,3r)$ . There are no hypotheses or range restrictions on $r$ , so the assertion includes every real value, including negative values and values for which $r$ , $3r$ , or $4r$ would not ordinarily be interpreted as probabilities.

View graph