摘要
半正定锥的部分转置像，在一个固定的复合载体上提供了一种已有的、替代性的有序表述。同时输运锥与过程保持了抽象的等价性，而固定过程表示则可以区分这两种序。我们研究在给定的有限量子比特载体上迭代一条指定的右参数转置规则。对于三个标准叶子，其两种括号方式给出不同的锥，因此不存在任何逐点固定每个乘积算符的线性等同能使它们一致。子集取向标签给出了一个显式的修复。相对于另行给定的、张量封闭的标准过程范畴，我们构造箭头的原始张量、结合子、对称、非对称单位映射与拟逆张量子，并通过忠实输运证明对称幺半等价。互补子集定义同一个孤立锥，但它们的等同对于原始张量积而言并不是一个同余。在固定秩处，一个被精确定义的两提升群胚是一个分裂的中心 Z₂ 扩张；在固定代表元下，其奇提升并不是一个普通的完全正自同态。随后，一个五量子比特例子把匹配的参考输运、一个固定的已定标锚，以及一个基于效应的商区分开来。后者失去的是一个线性子空间，而不只是一个两点转置轨道，并且只在满足标准核不变条件的历史下才被保持。一个被命名的实局部幺正算符连接该锚对，而一个实的受控非门（CNOT）则暴露出扩大的单锚历史类的局限。本文的贡献是对一条有限复合规则及其接口的受控假设分析，而不是一个新的一般融贯性、取向或资源定理，也不是从原初互补性推导量子理论。
部分支撑性陈述与有限见证附有部分的 Lean 4.19.0 形式化。一次记录在案的本地构建与类型／公理审计接受了 117 条定理声明与 57 个定义或缩写。定理 4.5 与 4.6 中完整的对称幺半范畴与等价，以及其他明确列出的稿件链接，仍未被完整形式化。公开的源代码补充材料还包括三份被保留的精确 Python 实现、预期结果、锁定的依赖，以及主张到代码的对照表。打包与源／日志审计并不是又一次 Lean 编译器运行，也不是外部同行评议。
公开的证据选择保留了成功的类型／公理输出以及失败／成功的时间顺序。机器本地的账户路径已从导出的运行摘要中略去，并且有一份失败构建的诊断对其主目录前缀做了明确的规范化。被接受的 Lean 证明源保持不变；私有的评审存档与原始的机器本地回执并不是公开上传文件。
它在本次发布中的位置
开启复合与胞腔分支，把“表述方式的融贯更换”与“被物理容许的过程”区分开来。部分陈述带有 Lean 4.19.0 的部分形式化；定理 4.5–4.6 的完整幺半等价仍未被完整形式化。
下载论文（Zenodo） —— CC-BY-4.0。