Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Li–Jiang polar-pair optimality: an exact finite-noise refutation

Abstract

A feasible qubit rank-one encoder strictly improves the source polar pair.

Definition 1.1 (First source parameter).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.lambda1 (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Source Eq. 18: d is the logical dimension and p is the noise parameter.

Definition 1.2 (Fourth source parameter).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.lambda4 (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Source Eq. 18; the denominator is d squared.

Definition 1.3 (Fifth source parameter).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.lambda5 (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Source Eq. 18; the claim restricts p to the open interval (0,1).

Definition 1.4 (Second source parameter).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.lambda2 (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Source Eq. 18, with lambda1 and lambda4 as defined above.

Definition 1.5 (Third source parameter).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.lambda3 (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Source Eq. 18, with the factor 2 in the numerator.

Definition 1.6 (Source positive matrix).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourceQ (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Literal Eq. 18, with identity on the code space and maxEntangled(Fin(d)) on the same space. Square roots are the real nonnegative square roots, embedded into the complex matrices.

Definition 1.7 (Right-factor trace Kraus matrices).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourceD (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Eq. 19: D_j = I_L tensor bra(j). Its row a and column (b,k) entry is 1 exactly when a=b and j=k. Thus it removes the right factor.

Definition 1.8 (Source products).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourceB (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Eqs. 19–21: B_ij = Q D_i adjoint D_j. The order of the two indices is retained.

Definition 1.9 (Source orthonormal matrices).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourceE (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Literal Eq. 22, including B_ij adjoint. The ket e_ij is the product-basis vector and psi is maxEntangledVector(Fin(d)).

Definition 1.10 (Actual right partial trace).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.rightTrace (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

The map is partialTraceRight from the existing library. It acts on every complex input matrix and retains the left factor.

Definition 1.11 (Source noise on all matrices).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourceNoise (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Literal all-matrix Eq. 23. The identity in the first term acts on the code space; the identity in the Kronecker term acts on the auxiliary factor. Neither input nor output is normalized by its trace.

Definition 1.12 (Source polar column matrix).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourceC (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Supplement Eq. S60: chi is an auxiliary vector, and sourceC is Q times the column map I tensor ket(chi).

Definition 1.13 (Source polar encoder).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourcePolar (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Eq. S60. CFCsqrt denotes CFC.sqrt and ofMatrixInverse denotes CStarMatrix.ofMatrix.symm. The square root is the ordered positive CFC square root of the actual Gram matrix, transported through that equivalence; the inverse is the matrix inverse.

Definition 1.14 (Matrix action of a completely positive map).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.matrixAction (✓ std3).

Source. Repository-derived.

Acknowledgement. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

The carrier is CompletelyPositiveMap on the finite CStarMatrix algebras, so complete positivity means positivity at every amplification. FiniteIndex abbreviates an arbitrary finite index type with Fintype and DecidableEq instances. ofMatrix is CStarMatrix.ofMatrix, and ofMatrixInverse is its inverse CStarMatrix.ofMatrix.symm; they transport input and output matrices across that equivalence.

Definition 1.15 (Trace constraint on every positive input).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.TraceNonincreasing (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Eq. 13 permits trace-nonincreasing encoding and decoding. X ranges over every positive semidefinite matrix, and Re extracts the real part of its trace.

Definition 1.16 (Input-first Choi convention).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.inputFirstChoi (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

MatrixMap denotes PhyslibLeaf.MatrixMap, and choiMatrix denotes its choi_matrix. The source’s input-first convention is obtained by swapping both product indices of that output-first Choi matrix. The reindexing uses Equiv.prodComm(b,a).

Definition 1.17 (Unrenormalized canonical-purification fidelity).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.entanglementFidelity (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

The shared maxEntangledVector(Fin(d)) is the normalized purification of I/d, in logical-factor-first product order, and maxEntangled(Fin(d)) is its rank-one projector. This is the source overlap for tau=I/d: apply the logical channel to the first purification factor and the identity to the reference factor, then take the real overlap. No output trace division is made, including for trace-decreasing competitors.

Definition 1.18 (Full fixed-noise polar-pair dominance assertion).

Formalization. D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.claim (✓ std3).

Citation. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

Li and Jiang, arXiv:2609.00778v1, printed p. 17 after Eq. S64: ‘Exact optimality of this pair at fixed p > 0 remains open.’ The antecedent is the Eq. S60 polar encoder and the actual right partial trace. The claim quantifies over every natural d >= 2, every real 0 < p < 1, every unit complex auxiliary vector chi, and every completely positive trace-nonincreasing encoder C and decoder D with input-first encoder Choi rank at most one. ofKraus denotes PhyslibLeaf.MatrixMap.of_kraus, and comp composes maps in outer-then-inner order. Competitors are arbitrary members of that class, rather than just the isometric witnesses used to refute it.

Theorem 1.19 (A feasible qubit pair strictly improves the source polar pair).

Proof. Machine-checked in Lean as D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.result (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Bikun Li; Liang Jiang (2026). High-Rank Encoding Can Improve Approximate Quantum Error Correction. URL: https://arxiv.org/abs/2609.00778v1.

Commentary.

At d=2, p=9/13 and chi=ket(0), the source polar columns are (3ket(00)-ket(11))/sqrt(10) and ket(10). The competitor columns are (24ket(00)-7ket(11))/25 and ket(10), with the same actual right partial trace decoder. The proof identifies the positive Gram square root and its inverse, gives the actual source noise 24 complete Kraus matrices, and uses the 48 decoder-noise-encoder composite matrices. It bridges canonical-purification fidelity to the Kraus trace sum and proves both witnesses feasible in the full all-amplification CP/TNI class, with input-first encoder Choi rank at most one. The source polar fidelity is 1537/4160 + 7sqrt(10)/80; the competitor fidelity is 336031/520000. Their difference is 7(10279-3250sqrt(10))/260000 > 0, using 10279 squared minus 10 times 3250 squared = 32841. This refutes exact finite-noise dominance. It determines no global rank-one optimum and does not refute the source’s optimal quadratic asymptotic coefficient.

References

  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.TraceNonincreasing
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.claim
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.entanglementFidelity
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.inputFirstChoi
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.lambda1
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.lambda2
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.lambda3
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.lambda4
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.lambda5
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.matrixAction
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.result
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.rightTrace
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourceB
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourceC
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourceD
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourceE
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourceNoise
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourcePolar
  • Truth anchor: D5/S3/Quantum/Recovery/LiJiangPolarPairOptimalityRefutation.sourceQ
  • Dependency: D5/S3/Quantum/Foundation/FiniteKrausRepresentation
  • Dependency: D5/S3/Quantum/Information/PartialTraceMutualInformation
  • Dependency: D5/S3/QuantumBounds/PeritoTsirelson