Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

No pure steering bit in minimal dimension

Open
QAlgorithms.Papers.Independent.Intakethird100.P36.no_pure_steering_bit

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

prove2quantum

Consider normalized no-signaling assemblages with a qubit Bob system and two binary inputs and outputs. Call an assemblage pure if every conditional density block has a unit-vector representative, with arbitrary normalized outcome probabilities; its Bob marginal need not be pure. Then

∄ Ψ pure such that∀Σ,Ψ⟶Σ\nexists\,\Psi\ \text{pure such that}\quad \forall\Sigma,\quad \Psi\longrightarrow\Sigma∄Ψ pure such that∀Σ,Ψ⟶Σ

where Σ\SigmaΣ ranges over all normalized assemblages with the same minimal dimensions and each arrow denotes an exact single-copy stochastic Bob-to-Alice 1W-LOCC conversion with strictly positive, input-independent success probability. The source may be nonorthogonal. This rules out a universal pure unit of steering in the minimal dimension, while making no assertion about mixed sources.

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 : ℕ}

/-- Theorem 5, PDF p.7; Appendix F, pp.14–16. No pure source is universal for
normalized targets of the same minimal dimension. The source need not be
orthogonal; no claim about a mixed universal source is made. -/
theorem no_pure_steering_bit :
    ¬ ∃ rho : AssemblageBlocks 2 2 2, IsNormalized rho ∧ IsPureAssemblage rho ∧
      ∀ sigma : AssemblageBlocks 2 2 2, IsNormalized sigma → SteeringConverts rho sigma := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P36

end
Source
The resource theory of steering, arXiv:1409.5804v3, PDF p. 7, Theorem 5
Read-back

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

There does not exist a family ρ=(ρa∣x)a,x<2\rho=(\rho_{a|x})_{a,x<2}ρ=(ρa∣x​)a,x<2​ of complex 2×22\times22×2 matrices with all of the following properties: every block is 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; there exist, for each xxx, nonnegative numbers px,ap_{x,a}px,a​ summing to one and vectors va,x∈C2v_{a,x}\in\mathbb C^2va,x​∈C2 satisfying ∑i∣va,x,i∣2=1\sum_i|v_{a,x,i}|^2=1∑i​∣va,x,i​∣2=1 for every a,xa,xa,x, including those with px,a=0p_{x,a}=0px,a​=0, such that ρa∣x=px,ava,xva,x†\rho_{a|x}=p_{x,a}v_{a,x}v_{a,x}^\daggerρa∣x​=px,a​va,x​va,x†​; and ρ\rhoρ converts to every normalized family σ=(σaf∣xf)af,xf<2\sigma=(\sigma_{a_f|x_f})_{a_f,x_f<2}σ=(σaf​∣xf​​)af​,xf​<2​. Here normalized for σ\sigmaσ means the same positivity, equality of the two outcome sums, and unit total mass just specified for ρ\rhoρ, without any purity requirement. Conversion means that there exist a natural number mmm, matrices Kw∈C2×2K_w\in\mathbb C^{2\times2}Kw​∈C2×2 with I−∑w<mKw†KwI-\sum_{w<m}K_w^\dagger K_wI−∑w<m​Kw†​Kw​ positive semidefinite, nonnegative numbers iw,xf,xi_{w,x_f,x}iw,xf​,x​ with ∑xiw,xf,x=1\sum_xi_{w,x_f,x}=1∑x​iw,xf​,x​=1, nonnegative numbers ow,af,a,x,xfo_{w,a_f,a,x,x_f}ow,af​,a,x,xf​​ with ∑afow,af,a,x,xf=1\sum_{a_f}o_{w,a_f,a,x,x_f}=1∑af​​ow,af​,a,x,xf​​=1, and a real ppp with 0<p≤10<p\le10<p≤1, such that, for every af,xfa_f,x_faf​,xf​, ∑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​​. These choices may depend on σ\sigmaσ; the protocol need not be complete, and the unit vectors specifying purity need not be mutually orthogonal.

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