No nonzero product vector lies in the range of
OpenOAI.DimensionTen.compositeChoi_range_criterionalgebraic-geometryentanglementquantum-informationrange-criterion
For the Choi matrix of the composition of the two explicit maps of the dimension-ten pair, the range of contains no nonzero product vector: whenever with , one of is zero. The source proves this (Proposition 6.1 and Proposition 7.2) from twenty projective directions in at which the pencil map has singular output: each gives a product vector in the kernel of , so a product vector in the range would yield two nonzero homogeneous quadratics in four variables whose zero sets cover all twenty directions, while an exact Galois-theoretic certificate shows every nonzero quadratic vanishes on at most nine of them.
Preamble
import Mathlib import Definitions.Def_DimensionTenPair open Matrix Complex open scoped Matrix ComplexOrder
Formal statement
namespace OAI.DimensionTen
theorem compositeChoi_range_criterion :
∀ (u v : Fin 10 → ℂ) (w : Fin 10 × Fin 10 → ℂ),
choi (phiTwo ∘ phiOne) *ᵥ w = productVector u v → u = 0 ∨ v = 0 := by sorry
end OAI.DimensionTenSource
OpenAI, Entanglement with zero distillable secret key in local dimension ten (September 27, 2026), https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Entanglement-with-zero-distillable-secret-key-in-local-dimension-ten-September-27-2026/paper.pdf, Section 6, Proposition 6.1 (tensor criterion) and Section 7, Proposition 7.2 (twenty rank-loss directions with independent quadratic evaluations), with the arithmetic certificate of Appendix A.