摘要
半正定錐的部分轉置像，在一個固定的複合載體上提供了一種已有的、替代性的有序表述。同時輸運錐與過程保持了抽象的等價性，而固定過程表示則可以區分這兩種序。我們研究在給定的有限量子位元載體上迭代一條指定的右參數轉置規則。對於三個標準葉子，其兩種括號方式給出不同的錐，因此不存在任何逐點固定每個乘積算符的線性等同能使它們一致。子集取向標籤給出了一個顯式的修復。相對於另行給定的、張量封閉的標準過程範疇，我們構造箭頭的原始張量、結合子、對稱、非對稱單位映射與擬逆張量子，並通過忠實輸運證明對稱幺半等價。互補子集定義同一個孤立錐，但它們的等同對於原始張量積而言並不是一個同餘。在固定秩處，一個被精確定義的兩提升群胚是一個分裂的中心 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。