Exact conditional contraction for Pauli channels and depolarization in every dimension

Dev D. Goyal

Exact conditional contraction for Pauli channels and depolarization in every dimension

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Exact conditional hockey-stick contraction coefficients of Pauli and depolarizing channels
Status: Determined exactly
Result: For every γ ≥ 1 the conditional hockey-stick contraction coefficient is 1 − 8ab/(a+b) for a Pauli channel with smallest weights a ≤ b, and s[1+(d²−1)s]/[1−(d²−3)s] for depolarization λ = −s, 0 ≤ s ≤ 1/(d²−1), in dimension d.

Abstract

The conditional hockey-stick contraction coefficient is determined exactly for every stochastic Pauli qubit channel and for depolarization throughout its physical parameter interval in every dimension. The formulas include all boundary cases and every hockey-stick parameter γ ≥ 1, with arbitrary finite quantum references.

Details

Year: 2026
Discipline: Mathematical physics
Area: Quantum information
Subject: Quantum information
Result type: Standalone theorem and reproducible proof package
Formal proof: Standalone Lean package
Family: quantum-exact-contraction
Keywords: contraction coefficients, hockey-stick divergence, Pauli channels, depolarizing channel, strong data processing, quantum channels

Statement and scope

Formal scope. The exact conditional hockey-stick contraction coefficients are formalized for actual finite-reference density states, every stochastic Pauli qubit channel, the full physical signed depolarizing family in every dimension d ≥ 2, and every γ ≥ 1. Channel constructors, unrestricted upper bounds and matching supremum witnesses are included. Unital-qubit normal-form existence is cited; erasure-simulation and ensemble-guessing consequences retain conventional proofs.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 516 KB
PDF on GitHub: papers/physics/quantum-exact-contraction/quantum_exact_contraction.pdf
LaTeX source: papers/physics/quantum-exact-contraction/quantum_exact_contraction.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/physics/quantum-exact-contraction/ 57 Lean files

Lakefile

papers/physics/quantum-exact-contraction/lakefile.lean

Toolchain

leanprover/lean4:v4.19.0

Library roots

AuditExactContraction.lean

Reproduce

The commands below are quoted from papers/physics/quantum-exact-contraction/README.md, which gives their context and working directory.

Reproduction

lake exe cache get
python3 verify.py

Reproduction

python3 verify.py --lean /path/to/lean --mathlib /path/to/mathlib

README: papers/physics/quantum-exact-contraction/README.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior work. The Omega Institute's public repository records a claimed general proof that the conditional hockey-stick coefficient does not depend on γ ≥ 1, committed on 16 October 2026 (issue #17637). The exact Pauli and depolarizing values here are not in that record. Priority and novelty record.

Source. Prior results and source-comparison limits are stated in the manuscript. Historical priority is not certified.

Questions and answers

What is the conditional contraction coefficient of a Pauli channel?

If a ≤ b are the two smallest Pauli probabilities, the conditional hockey-stick contraction coefficient equals 1 − 8ab/(a+b) for every γ ≥ 1, with value 1 when a = b = 0, over arbitrary finite quantum references. The extension to all unital qubit channels uses the cited Choi–Li normal form, which is not part of the Lean project.

What is the value for the depolarizing channel?

For D_λ in dimension d ≥ 2 it is λ when 0 ≤ λ ≤ 1 and s[1+(d²−1)s]/[1−(d²−3)s] when λ = −s with 0 ≤ s ≤ 1/(d²−1), for every γ ≥ 1. The conditional framework and positive-Doeblin upper bound are due to Hirche, George, Nuradha and Wilde; historical priority is not certified.

Is the result formally verified?

The exact coefficients are formalized in Lean 4 for actual finite-reference density states, every stochastic Pauli qubit channel and the full signed depolarizing family in every dimension d ≥ 2, including matching supremum witnesses. Erasure-simulation and ensemble-guessing consequences keep conventional proofs, and the paper is an unrefereed preprint.

Was the γ-independence known before?

Yes, in general: the Omega Institute's public repository records a claimed proof, committed on 16 October 2026 (issue #17637), that the conditional hockey-stick coefficient of every finite channel equals its trace-distance value for all γ ≥ 1. The exact Pauli and depolarizing values here are not in that record.

Cite

Citation file papers/physics/quantum-exact-contraction/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@unpublished{goyal2026exactcontraction,
  author = {Goyal, Dev D.},
  title = {Exact conditional contraction for Pauli channels and depolarization in every dimension},
  year = {2026},
  note = {Unpublished preprint. Fully autonomous agentic research. Historical priority remains provisional.},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/physics/quantum-exact-contraction}
}