Clifford+T的距离无关普适性
Distance-Independent Universality of Clifford+T
浏览论文内容
中文总结 AI 辅助
该研究通过四个公理定义射影距离度量，证明Clifford+T门集的普适性定理对满足这些公理的所有距离度量成立，从而实现距离无关的普适性，并在Lean中形式化证明。
中文摘要 AI 辅助
一个著名的定理指出，Clifford+T门集对于量子计算是普适的。该定理将基于酉矩阵上距离度量的近似与全局相位下的相等性相结合。先前的证明针对特定距离度量结合了这两个概念，但未识别出支配它们如何协同工作的性质。哪些性质足以陈述并证明该定理？我们通过四个公理定义射影距离度量来回答这个问题。我们证明了对于满足这些公理的每一个距离度量，普适性定理都成立。因此，我们对定理的表述不依赖于任何特定距离度量的选择。我们展示了希尔伯特-施密特距离已经是一个射影距离度量。我们还开发了一种一般性构造，将一大类距离度量转化为射影距离度量，并将其应用于获得算子范数距离、弗罗贝尼乌斯距离和迹距离的射影版本。最后，我们在Lean中形式化了普适性定理的证明。
英文摘要
A well-known theorem states that the Clifford+T gate set is universal for quantum computing. The theorem combines approximation using a distance measure on unitary matrices with equality up to global phase. Previous proofs combine these two notions for specific distance measures, but do not identify the properties that govern how they work together. Which properties are sufficient to state and prove the theorem? We answer this question by defining projective distance measures using four axioms. We prove that the universality theorem holds for every distance measure satisfying these axioms. Thus, our formulation of the theorem is independent of any particular choice of distance measure. We show that the Hilbert-Schmidt distance is already a projective distance measure. We also develop a general construction that transforms a large class of distance measures into projective distance measures and apply it to obtain projective versions of the operator-norm distance, the Frobenius distance, and the trace distance. Finally, we formalize the proof of the universality theorem in Lean.
发表机构
- University of California, Los Angeles（加州大学洛杉矶分校）
机构由 AI 辅助整理，请以论文原文为准。
