Universal entanglement embezzlement with inverse-quadratic logarithmic infidelity

Dev D. Goyal

Universal entanglement embezzlement with inverse-quadratic logarithmic infidelity

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

Selected result in this collection

Problem and result

Problem: Leung–Wang question on the rate of general universal entanglement embezzling families
Posed in: Leung and Wang, 'Characteristics of universal embezzling families', Physical Review A 90, 042331 (2014), Section 6
Status: Answered positively
Result: For each L ≥ 1 one target-independent catalyst of local dimension n = 2^(4L) lets local basis permutations reach root fidelity at least 1 − 125m/L² = 1 − 2000m/(log₂ n)² for every Schmidt probability vector on m entries.

Abstract

A target-independent catalyst with local dimension 2^(4L) gives root infidelity at most 125m/L² for every Schmidt probability vector on m entries.

Details

Year: 2026
Discipline: Mathematical physics
Area: Quantum information
Subject: Quantum information
Result type: Universal catalyst with a quantitative error bound
Formal proof: Standalone Lean package
Family: universal-embezzlement
Keywords: entanglement embezzlement, embezzling states, quantum catalysts, catalytic transformations, van Dam–Hayden

Statement and scope

Formal scope. The proof constructs local basis permutations and establishes their finite complex Hilbert-space interpretation. Arbitrary changes to an external Schmidt basis are not separately formalized.

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 308 KB
PDF on GitHub: papers/physics/universal-embezzlement/manuscript.pdf
LaTeX source: papers/physics/universal-embezzlement/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/universal-embezzlement/ 3 Lean files

Lakefile

papers/physics/universal-embezzlement/lakefile.lean

Toolchain

leanprover/lean4:v4.19.0

Library roots

UniversalEmbezzlement.lean

Reproduce

The commands below are quoted from papers/physics/universal-embezzlement/README.md, which gives their context and working directory.

Reproduce the proof

lake exe cache get
lake build
lake env lean -DwarningAsError=true Audit.lean

README: papers/physics/universal-embezzlement/README.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior work. Van Dam and Hayden, 2003; Leung and Wang, 2014.

Questions and answers

Can a universal embezzling family reach root infidelity of order 1/(log n)²?

For general families, yes: this preprint gives target-independent catalysts of local dimension n = 2^(4L) for which local basis permutations achieve root fidelity at least 1 − 125m/L² = 1 − 2000m/(log₂ n)² for every Schmidt probability vector on m entries. The catalyst envelope depends on L, so it is a nonregular family and the regular-family version of Leung and Wang's question is not addressed.

How does this compare with the van Dam–Hayden catalyst?

The harmonic van Dam–Hayden family gives universal root infidelity of order 1/log n, and a target-dependent construction with the quadratic rate was already known. The constant 125m and its dependence on m are not claimed optimal, the local permutation depends on the target, and only the dimensions 16^L are covered.

Is the proof formally verified?

The coefficient bound and its finite complex Hilbert-space interpretation with separate local basis permutations are formalized in Lean 4. A change from an arbitrary bipartite basis to Schmidt form is not separately formalized, and the paper is an unrefereed preprint.

Cite

Citation file papers/physics/universal-embezzlement/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026universalembezzlement,
  author = {Goyal, Dev D.},
  title = {Universal entanglement embezzlement with inverse-quadratic logarithmic infidelity},
  year = {2026},
  howpublished = {Preprint},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/physics/universal-embezzlement},
  note = {Fully autonomous agentic research generated by AI systems.}
}