Strong minimum-rank multiplicativity from unextendible product constraints

Dev D. Goyal

Strong minimum-rank multiplicativity from unextendible product constraints

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Schmidt number of tensor powers of the Tiles UPB bound entangled state
Status: Determined exactly
Result: If a complex matrix subspace S is annihilated by an unextendible family of product functionals, every nonzero element of S ⊗ T has rank at least 2m(T); for the Tiles bound entangled state ρ, SN(ρ^⊗N) = 2^N for all N ≥ 1.

Abstract

A complex matrix subspace annihilated by an unextendible family of product functionals doubles minimum rank under tensor products: if every nonzero member of T has rank at least r, every nonzero member of S ⊗ T has rank at least 2r, and the minimum rank is exactly doubled when S contains a rank-two matrix. For the Tiles bound entangled state ρ, this gives Schmidt number SN(ρ^⊗N) = 2^N for every N ≥ 1, so N copies cost exactly N ebits to prepare by LOCC with zero error. The two-copy case and nonsharp exponential growth were known.

Details

Year: 2026
Discipline: Mathematical physics
Area: Quantum information
Subject: Quantum information
Result type: Theorem, exact all-copy formula and reproducible proof package
Formal proof: Standalone Lean package
Family: upb-tensor-rank
Keywords: unextendible product bases, UPB, Schmidt number, bound entanglement, Tiles state, PPT entangled states, zero-error entanglement cost, minimum rank

Statement and scope

Formal scope. The rank-doubling theorem with an arbitrary partner, strong minimum-rank multiplicativity, the Tiles support and normalized density operators, and the exact all-copy Schmidt-number equivalence are formalized in 22 Lean modules. The zero-error LOCC cost, the rank-four two-qutrit PPT class and the channel interpretation combine the formal theorem with published results.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 354 KB
PDF on GitHub: papers/physics/upb-tensor-rank/manuscript.pdf
LaTeX source: papers/physics/upb-tensor-rank/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/physics/upb-tensor-rank/

Lean project

papers/physics/upb-tensor-rank/lean/ 23 Lean files

Lakefile

papers/physics/upb-tensor-rank/lean/lakefile.lean

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/physics/upb-tensor-rank/VERIFICATION.md, which gives their context and working directory.

lake exe cache get
python3 verify.py

python3 calculations/exact_matrix_audit.py

README: papers/physics/upb-tensor-rank/README.md
Verification guide: papers/physics/upb-tensor-rank/verification/README.md
Verification record: papers/physics/upb-tensor-rank/VERIFICATION.md
Authorship: papers/physics/upb-tensor-rank/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Source. The Tiles UPB is due to Bennett et al. (1999); Chen, Yang and Tang (2017) proved the two-copy case and Vidal and Cirac (2001) implied nonsharp exponential growth. Related work and limits are stated in the manuscript. Historical priority is not certified.

Questions and answers

What is the Schmidt number of many copies of the Tiles bound entangled state?

For the Tiles UPB projector P and ρ = P/4, the preprint proves SN(ρ^⊗N) = m(range P^⊗N) = 2^N for every N ≥ 1 across the bipartition A₁⋯A_N : B₁⋯B_N. Combined with the published operational meaning of the Schmidt number, N copies cost exactly N ebits to prepare by LOCC with zero error. The general theorem does not claim that minimum rank is multiplicative for arbitrary pairs of subspaces.

Was this known before?

Partly. Chen, Yang and Tang (2017) proved the two-copy case, Vidal and Cirac (2001) implies nonsharp exponential growth, and the Tiles UPB is due to Bennett et al. (1999). The sharp all-copy law and the general theorem with an arbitrary partner are the contribution; no established conjecture asking for this law was found, and originality remains provisional.

Is the proof formally verified?

The rank-doubling theorem with an arbitrary partner, strong minimum-rank multiplicativity and the exact all-copy Schmidt-number formula for the Tiles state are formalized in 22 Lean 4 modules. The zero-error LOCC cost, the rank-four two-qutrit PPT class and the channel interpretation combine the formal theorem with published results that are not formalized.

Cite

Citation file papers/physics/upb-tensor-rank/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026upbtensorrank,
  author = {Goyal, Dev D.},
  title = {Strong Minimum-Rank Multiplicativity from Unextendible Product Constraints},
  year = {2026},
  month = oct,
  note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/physics/upb-tensor-rank}
}