Regular contracted S coordinates are valid Pauli points

Proved

QAlgorithms.Papers.Independent.Intakethird100.P13.regularPoint_inTetrahedron

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

prove2quantum

Let $\gamma,s\in[0,1]$ and assume $1-\gamma s>0$ , the domain of the displayed real quotient. Let $T$ be the convex hull of the four Bell-correlation vectors $(1,-1,1),(1,1,-1),(-1,-1,-1),(-1,1,1)$ , and suppose $v=(S_{11},S_{22},S_{33})\in T$ . The point constructed from the positive-translation rescaling satisfies

\left(\sqrt{\frac{1-\gamma}{1-\gamma s}}S_{11},\sqrt{\frac{1-\gamma}{1-\gamma s}}S_{22},\frac{1-\gamma}{1-\gamma s}S_{33}\right)\in T.

Here $s=S_{30}$ in the application. This is a computed point, and no unrelated free Pauli parameters are assumed.

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.12--13, Corollary 23, Eq.(C3), positive S30 case.
The constructed point uses the regular quotient domain of Lemma 20. -/
theorem regularPoint_inTetrahedron (gamma s30 : ℝ) (hg0 : 0 ≤ gamma) (hg1 : gamma ≤ 1)
    (hs0 : 0 ≤ s30) (hs1 : s30 ≤ 1) (hden : 0 < 1-gamma*s30)
    (s : BlochCoordinates) (hs : s ∈ pauliTetrahedron) :
    regularPauliPoint gamma s30 s ∈ pauliTetrahedron := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P13

end

Source

Simulation of non-Pauli Channels, arXiv:1706.05384v2, PDF p. 13, Corollary 23, Eq.(C3)

Read-back

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

For every pair of real numbers $\gamma,s_{30}$ satisfying $0\le\gamma\le1$ , $0\le s_{30}\le1$ , and $1-\gamma s_{30}>0$ , and every vector $s=(s_0,s_1,s_2)\in\mathbb R^3$ in the convex hull of $(1,-1,1)$ , $(1,1,-1)$ , $(-1,-1,-1)$ , and $(-1,1,1)$ , the vector

\left( \sqrt{\frac{1-\gamma}{1-\gamma s_{30}}}\,s_0,\ \sqrt{\frac{1-\gamma}{1-\gamma s_{30}}}\,s_1,\ \frac{1-\gamma}{1-\gamma s_{30}}\,s_2 \right)

belongs to that same convex hull. The endpoints of the stated intervals are included whenever the strict denominator condition holds.

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