Every classical channel gives a diagonal S point in T

Open

QAlgorithms.Papers.Independent.Intakethird100.P13.diagonalS_inTetrahedron

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $p(l\mid k)$ be any nonnegative conditional law on four symbols, with $\sum_l p(l\mid k)=1$ separately for each input $k$ . Define $S_{ij}$ by Eq. (38), including its factor $1/4$ and six-delta exponent. For the Bell-correlation tetrahedron $T=\operatorname{conv}\{(1,-1,1),(1,1,-1),(-1,-1,-1),(-1,1,1)\}$ ,

(S_{11},S_{22},S_{33})\in T.

This assertion requires neither a resource state nor a damping parameter. It covers all conditional channels, including laws that are not doubly stochastic.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P13

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P13

attribute [local instance] Classical.propDecidable Classical.decEq

/-- arXiv:1706.05384v2 PDF pp.5,13, Lemma 24: no resource or damping assumption.
Eq.(38)'s normalization, rather than Appendix B's omitted factor, defines S. -/
theorem diagonalS_inTetrahedron (p : Fin 4 → Fin 4 → ℝ) (hp : ClassicalTeleportationLaw p) :
    (fun i : Fin 3 => sCoordinate p i i.succ) ∈ pauliTetrahedron := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P13

end

Source

Simulation of non-Pauli Channels, arXiv:1706.05384v2, PDF p. 13, Lemma 24

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every real array $p=(p_{lk})_{l,k=0}^3$ such that $p_{lk}\ge0$ for every $l,k$ and $\sum_{l=0}^3p_{lk}=1$ for each $k$ , define $\delta_{ab}=1$ when $a=b$ and $0$ otherwise. Then the vector $v\in\mathbb R^3$ with coordinates

v_i=\frac14\sum_{k=0}^3\sum_{l=0}^3 (-1)^{\delta_{k0}+\delta_{i+1,2}+\delta_{i+1,0}+\delta_{k,i+1}+\delta_{i+1,l}+\delta_{0l}} p_{lk}, \qquad i=0,1,2,

belongs to the convex hull of $(1,-1,1)$ , $(1,1,-1)$ , $(-1,-1,-1)$ , and $(-1,1,1)$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph