Anisotropic contraction preserves the correlation tetrahedron

Proved

QAlgorithms.Papers.Independent.Intakethird100.P13.contraction_preservesTetrahedron

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

prove2quantum

Let $T$ be the convex hull of $(1,-1,1),(1,1,-1),(-1,-1,-1),(-1,1,1)$ . For every $\alpha\in[0,1]$ and $(x,y,z)\in T$ ,

(\sqrt\alpha\,x,\sqrt\alpha\,y,\alpha z)\in T.

This gives a contraction of Pauli correlation points. The square roots apply only to the rescaling parameter, and the source's correlation Y coordinate is retained.

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, Lemma 22; the erroneous C2 weight table
is not used as a premise. -/
theorem contraction_preservesTetrahedron (alpha : ℝ) (h0 : 0 ≤ alpha) (h1 : alpha ≤ 1)
    (q : BlochCoordinates) (hq : q ∈ pauliTetrahedron) :
    contractPoint alpha q ∈ pauliTetrahedron := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P13

end

Source

Simulation of non-Pauli Channels, arXiv:1706.05384v2, PDF p. 12, Lemma 22

Read-back

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

For every real number $\alpha$ with $0\le\alpha\le1$ , including both endpoints, and every vector $q=(q_0,q_1,q_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

(\sqrt{\alpha}\,q_0,\ \sqrt{\alpha}\,q_1,\ \alpha q_2)

belongs to that same convex hull.

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