Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Infinitely many inequivalent minimal-dimensional steering classes

Open
QAlgorithms.Papers.Independent.Intakethird100.P36.infinitely_many_steering_classes

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

prove2quantum

On a qubit, consider two binary inputs and outputs. For 0<θ<π/40<\theta<\pi/40<θ<π/4, define Ψa∣xθ=12∣ψθ(a,x)⟩⟨ψθ(a,x)∣\Psi^\theta_{a|x}=\tfrac12|\psi^\theta(a,x)\rangle\langle\psi^\theta(a,x)|Ψa∣xθ​=21​∣ψθ(a,x)⟩⟨ψθ(a,x)∣, where the input-zero basis is (∣0⟩,∣1⟩)(|0\rangle,|1\rangle)(∣0⟩,∣1⟩) and the input-one basis is (cos⁡θ∣0⟩+sin⁡θ∣1⟩,−sin⁡θ∣0⟩+cos⁡θ∣1⟩)(\cos\theta|0\rangle+\sin\theta|1\rangle,-\sin\theta|0\rangle+\cos\theta|1\rangle)(cosθ∣0⟩+sinθ∣1⟩,−sinθ∣0⟩+cosθ∣1⟩). These are normalized, pure orthogonal, steerable assemblages. For distinct parameters in this interval,

θ≠η⟹Ψθ⟶̸Ψη  and Ψη⟶̸Ψθ\theta\ne\eta\quad\Longrightarrow\quad \Psi^\theta\not\longrightarrow\Psi^\eta\ \text{ and } \Psi^\eta\not\longrightarrow\Psi^\thetaθ=η⟹Ψθ⟶Ψη  and Ψη⟶Ψθ

under stochastic 1W-LOCC with any strictly positive success probability. The family contains infinitely many distinct assemblages, so there are infinitely many inequivalent classes already at d=r=s=2d=r=s=2d=r=s=2. Restricting the witness angles selects distinct classes even when all input and output relabelings are allowed.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P36
Formal statement
noncomputable section

open scoped BigOperators ENNReal ComplexConjugate ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P36

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

attribute [local instance] Classical.propDecidable

variable {d r s df rf sf m : ℕ}

/-- Section VIII, PDF p.7, with the witness family (F5), p.15. Restricting angles
to (0,pi/4) selects infinitely many distinct relabeling orbits. This consequence
uses the overlap multiset invariant, not the defective literal criterion (24). -/
theorem infinitely_many_steering_classes :
    (∀ theta : ℝ, 0 < theta → theta < Real.pi / 4 →
      IsNormalized (angleAssemblage theta) ∧ IsPureOrthogonal (angleAssemblage theta) ∧
      ¬ HasFiniteLHSModel (angleAssemblage theta)) ∧
    (∀ theta eta : ℝ, 0 < theta → theta < Real.pi / 4 →
      0 < eta → eta < Real.pi / 4 → theta ≠ eta →
      ¬ SteeringConverts (angleAssemblage theta) (angleAssemblage eta) ∧
      ¬ SteeringConverts (angleAssemblage eta) (angleAssemblage theta)) ∧
    Set.Infinite (Set.range (fun theta : {t : ℝ // 0 < t ∧ t < Real.pi / 4} =>
      angleAssemblage theta.val)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P36

end
Source
The resource theory of steering, arXiv:1409.5804v3, PDF p. 7, Section VIII; (F5), p.15
Read-back

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

For each real θ\thetaθ, define a family of 2×22\times22×2 matrices by Aa∣xθ=12va,xθ(va,xθ)†A^\theta_{a|x}=\tfrac12v^\theta_{a,x}(v^\theta_{a,x})^\daggerAa∣xθ​=21​va,xθ​(va,xθ​)†, for a,x∈{0,1}a,x\in\{0,1\}a,x∈{0,1}, where v0,0θ=(1,0)v^\theta_{0,0}=(1,0)v0,0θ​=(1,0), v1,0θ=(0,1)v^\theta_{1,0}=(0,1)v1,0θ​=(0,1), v0,1θ=(cos⁡θ,sin⁡θ)v^\theta_{0,1}=(\cos\theta,\sin\theta)v0,1θ​=(cosθ,sinθ), and v1,1θ=(−sin⁡θ,cos⁡θ)v^\theta_{1,1}=(-\sin\theta,\cos\theta)v1,1θ​=(−sinθ,cosθ). A family ρa∣x\rho_{a|x}ρa∣x​ is normalized here when all its blocks are positive semidefinite, ∑aρa∣0=∑aρa∣1\sum_a\rho_{a|0}=\sum_a\rho_{a|1}∑a​ρa∣0​=∑a​ρa∣1​, and Re⁡tr⁡(12∑x,aρa∣x)=1\operatorname{Re}\operatorname{tr}(\tfrac12\sum_{x,a}\rho_{a|x})=1Retr(21​∑x,a​ρa∣x​)=1. It is pure orthogonal when there exist probability vectors (px,a)a<2(p_{x,a})_{a<2}(px,a​)a<2​ and vectors ua,x∈C2u_{a,x}\in\mathbb C^2ua,x​∈C2 with ∑iua,x,i‾ub,x,i=1\sum_i\overline{u_{a,x,i}}u_{b,x,i}=1∑i​ua,x,i​​ub,x,i​=1 if a=ba=ba=b and zero otherwise, such that ρa∣x=px,aua,xua,x†\rho_{a|x}=p_{x,a}u_{a,x}u_{a,x}^\daggerρa∣x​=px,a​ua,x​ua,x†​. A normalized family has a finite local hidden-state model when, for some natural number hhh, it can be written ρa∣x=∑ℓ<hpℓqℓ,x,aξℓ\rho_{a|x}=\sum_{\ell<h}p_\ell q_{\ell,x,a}\xi_\ellρa∣x​=∑ℓ<h​pℓ​qℓ,x,a​ξℓ​, where pℓ≥0p_\ell\ge0pℓ​≥0, ∑ℓpℓ=1\sum_\ell p_\ell=1∑ℓ​pℓ​=1, each ξℓ\xi_\ellξℓ​ is positive semidefinite with trace one, and each qℓ,x,aq_{\ell,x,a}qℓ,x,a​ is nonnegative with ∑aqℓ,x,a=1\sum_aq_{\ell,x,a}=1∑a​qℓ,x,a​=1. Conversion from a normalized family ρ\rhoρ to a normalized family σ\sigmaσ means that there exist a natural number mmm, matrices Kw∈C2×2K_w\in\mathbb C^{2\times2}Kw​∈C2×2 with I−∑wKw†KwI-\sum_wK_w^\dagger K_wI−∑w​Kw†​Kw​ positive semidefinite, probability vectors iw,xf,xi_{w,x_f,x}iw,xf​,x​ over xxx, probability vectors ow,af,a,x,xfo_{w,a_f,a,x,x_f}ow,af​,a,x,xf​​ over afa_faf​, and a real ppp with 0<p≤10<p\le10<p≤1, such that ∑w,x,aiw,xf,xow,af,a,x,xfKwρa∣xKw†=pσaf∣xf\sum_{w,x,a}i_{w,x_f,x}o_{w,a_f,a,x,x_f}K_w\rho_{a|x}K_w^\dagger=p\sigma_{a_f|x_f}∑w,x,a​iw,xf​,x​ow,af​,a,x,xf​​Kw​ρa∣x​Kw†​=pσaf​∣xf​​ for every af,xfa_f,x_faf​,xf​; completeness of the matrices KwK_wKw​ is not required. The declaration asserts that every AθA^\thetaAθ with 0<θ<π/40<\theta<\pi/40<θ<π/4 is normalized and pure orthogonal and has no finite local hidden-state model; for any distinct θ,η\theta,\etaθ,η both in that open interval, neither conversion Aθ→AηA^\theta\to A^\etaAθ→Aη nor conversion Aη→AθA^\eta\to A^\thetaAη→Aθ exists; and the set {Aθ:0<θ<π/4}\{A^\theta:0<\theta<\pi/4\}{Aθ:0<θ<π/4} of actual matrix families is infinite.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me