Expand the total-Pauli hashing baseline into binary entropy

Proved

DepolarizingCoherentInformation.totalPauli_expand

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

depolarizing-channelentropyhashing-bound

For every real q, unfold Mathlib’s four-ary entropy identity to express the scalar baseline exactly as Real.log 2 - (Real.binEntropy q + q * Real.log 3). This is an algebraic identity for Mathlib’s totalized entropy functions; no physical-range, positivity, or formal quantum-channel claim is made.

Preamble

import Definitions.Def_DepolarizingCoherentInformationBaseline

Formal statement

namespace DepolarizingCoherentInformation

theorem totalPauli_expand (q : ℝ) :
    symmetricIcTotalPauli q =
      Real.log 2 - (Real.binEntropy q + q * Real.log 3) := by
  sorry

end DepolarizingCoherentInformation

Source

Mathlib Real.qaryEntropy; Artus Krohn-Grimberghe, arXiv:2608.15870v2, §3, Remark (scope).

Read-back

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

For every real number $q$ , with no restriction such as $0 \le q \le 1$ , define $I_{\mathrm{sym}}(q)$ by $I_{\mathrm{sym}}(q) := \log 2-\operatorname{qaryEntropy}_4(q)$ , where $\log$ is the real logarithm; the declaration asserts that

I_{\mathrm{sym}}(q)=\log 2-\bigl(\operatorname{binEntropy}(q)+q\log 3\bigr).

View graph