No pure steering bit in minimal dimension
OpenQAlgorithms.Papers.Independent.Intakethird100.P36.no_pure_steering_bitConsider 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
where 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.
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P36
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
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
There does not exist a family of complex matrices with all of the following properties: every block is positive semidefinite, , and ; there exist, for each , nonnegative numbers summing to one and vectors satisfying for every , including those with , such that ; and converts to every normalized family . Here normalized for means the same positivity, equality of the two outcome sums, and unit total mass just specified for , without any purity requirement. Conversion means that there exist a natural number , matrices with positive semidefinite, nonnegative numbers with , nonnegative numbers with , and a real with , such that, for every , . These choices may depend on ; the protocol need not be complete, and the unit vectors specifying purity need not be mutually orthogonal.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.