Infinitely many inequivalent minimal-dimensional steering classes
OpenQAlgorithms.Papers.Independent.Intakethird100.P36.infinitely_many_steering_classesOn a qubit, consider two binary inputs and outputs. For , define , where the input-zero basis is and the input-one basis is . These are normalized, pure orthogonal, steerable assemblages. For distinct parameters in this interval,
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 . Restricting the witness angles selects distinct classes even when all input and output relabelings are allowed.
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 : ℕ}
/-- 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
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
For each real , define a family of matrices by , for , where , , , and . A family is normalized here when all its blocks are positive semidefinite, , and . It is pure orthogonal when there exist probability vectors and vectors with if and zero otherwise, such that . A normalized family has a finite local hidden-state model when, for some natural number , it can be written , where , , each is positive semidefinite with trace one, and each is nonnegative with . Conversion from a normalized family to a normalized family means that there exist a natural number , matrices with positive semidefinite, probability vectors over , probability vectors over , and a real with , such that for every ; completeness of the matrices is not required. The declaration asserts that every with is normalized and pure orthogonal and has no finite local hidden-state model; for any distinct both in that open interval, neither conversion nor conversion exists; and the set of actual matrix families is infinite.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.