Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Connected encoder classes and powers of three

Abstract

The commuting order-three rotations of the matched input-pivot pairs act freely on each connected class of normalized encoders. Each class therefore has cardinality divisible by 3^k.

Theorem 1.1 (Local complementation as an exclusive-or relation).

Proof. Machine-checked in Lean as D5/S3/Quantum/Codes/KhesinLiEquivalenceClasses.lc_source (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Andrey Boris Khesin, Alexander M. Li (2024). Equivalence Classes of Quantum Error-Correcting Codes. DOI: 10.48550/arXiv.2406.12083. URL: https://arxiv.org/abs/2406.12083v1.

Commentary.

Local complementation toggles the adjacency of two neighbours of v. The exclusive-or relation expresses this toggle; SimpleGraph.fromRel makes it symmetric and removes loops. Thus it gives exactly the same graph as lc.

Definition 1.2 (Adding one input row to another).

Formalization. D5/S3/Quantum/Codes/KhesinLiEquivalenceClasses.addInputRow (✓ std3).

Citation. Andrey Boris Khesin, Alexander M. Li (2024). Equivalence Classes of Quantum Error-Correcting Codes. DOI: 10.48550/arXiv.2406.12083. URL: https://arxiv.org/abs/2406.12083v1.

Commentary.

Conjecture 6.3, p. 17: “4. Performing row operations on the adjacency matrix of input to output edges.” Section 6, p. 18: “Operation 4 consists of adding rows of the adjacency matrix between input and output nodes in modulo 2.” Input vertices are Sum.inl and output vertices are Sum.inr. The row indexed by j is added to row i with Xor; all other edges are retained. SimpleGraph.fromRel removes loops and symmetrizes the displayed relation.

Definition 1.3 (Elementary encoder operations).

Formalization. D5/S3/Quantum/Codes/KhesinLiEquivalenceClasses.Step (✓ std3).

Citation. Andrey Boris Khesin, Alexander M. Li (2024). Equivalence Classes of Quantum Error-Correcting Codes. DOI: 10.48550/arXiv.2406.12083. URL: https://arxiv.org/abs/2406.12083v1.

Commentary.

Conjecture 6.3, p. 17, lists: “1. Local complementing about any vertex of the graph. 2. Permuting the output vertices. 3. Permuting the input vertices. 4. Performing row operations on the adjacency matrix of input to output edges. 5. Removing an input-input edge. 6. Applying local operations on the output edges.” Definition 2.7, p. 6: “By performing a local complementation about vertex v, all edges connecting two vertices in N(v) are toggled.” Step is the inductive relation generated by the five displayed constructors. Operation 6 acts on the removed local Clifford decorations. Permutations act by graph map along Equiv.sumCongr, with each embedding coerced to its underlying function; the row indices in a row operation must be distinct. Sym2.mk forms an unordered pair.

Definition 1.4 (Renormalizing operations).

Formalization. D5/S3/Quantum/Codes/KhesinLiEquivalenceClasses.RenormStep (✓ std3).

Citation. Andrey Boris Khesin, Alexander M. Li (2024). Equivalence Classes of Quantum Error-Correcting Codes. DOI: 10.48550/arXiv.2406.12083. URL: https://arxiv.org/abs/2406.12083v1.

Commentary.

Section 7, p. 19: “To fix this, we first employ operation 5 from Conjecture 6.3 to set all input-input edges to 0.” It continues: “Operation 2 is used to put the pivots back into their fixed positions, so they once again correspond to their input vertices.” RenormStep is the inductive relation generated by operations 2–5; its four constructors are displayed in full.

Definition 1.5 (Normalized labelled encoders).

Formalization. D5/S3/Quantum/Codes/KhesinLiEquivalenceClasses.Normalized (✓ std3).

Citation. Andrey Boris Khesin, Alexander M. Li (2024). Equivalence Classes of Quantum Error-Correcting Codes. DOI: 10.48550/arXiv.2406.12083. URL: https://arxiv.org/abs/2406.12083v1.

Commentary.

Claim 6.4, p. 19: “To find the distinct encoders in an equivalence class of the set of Clifford codes, it is sufficient to find the distinct encoders in the equivalence class satisfying the following constraints:” The list reads: “The input-output adjacency matrix is in RREF.” “The pivot nodes are the lowest-numbered output nodes, and they are ordered to match the order of the input nodes.” “Local Clifford gates on the free output edges are all removed, leaving only output Z nodes with phase 0.” “Diagrams with pivot-pivot edges are not included.” Inputs are Fin(k); outputs are Fin(n). The first k outputs are pivots with the identity input-pivot block. There are no input-input or pivot-pivot edges. The diagram has no local Clifford decorations.

Definition 1.6 (An operation followed by renormalization).

Formalization. D5/S3/Quantum/Codes/KhesinLiEquivalenceClasses.NormalizedStep (✓ std3).

Citation. Andrey Boris Khesin, Alexander M. Li (2024). Equivalence Classes of Quantum Error-Correcting Codes. DOI: 10.48550/arXiv.2406.12083. URL: https://arxiv.org/abs/2406.12083v1.

Commentary.

Section 7, p. 19: “The code takes an integer representation, say n, of an encoder graph, performs one operation from Conjecture 6.3 on the encoder graph, then merges the disjoint sets of n and the integer representing the resulting encoder graph.” The two endpoints are normalized; an intermediate graph Z is reached by Step and then a finite, possibly empty sequence of RenormStep operations. Relation.ReflTransGen represents that sequence.

Definition 1.7 (Number of normalized graphs in a class).

Formalization. D5/S3/Quantum/Codes/KhesinLiEquivalenceClasses.classSize (✓ std3).

Citation. Andrey Boris Khesin, Alexander M. Li (2024). Equivalence Classes of Quantum Error-Correcting Codes. DOI: 10.48550/arXiv.2406.12083. URL: https://arxiv.org/abs/2406.12083v1.

Commentary.

Section 7, p. 19: “The variable edges’ values in the adjacency matrix are made into a single integer using a binary representation.” The source counts distinct labelled normalized adjacency matrices. Nat.card counts the subtype of normalized graphs H in the Relation.EqvGen closure of NormalizedStep from G; it does not quotient graphs by isomorphism.

Definition 1.8 (Khesin–Li Conjecture 7.1).

Formalization. D5/S3/Quantum/Codes/KhesinLiEquivalenceClasses.claim (✓ std3).

Citation. Andrey Boris Khesin, Alexander M. Li (2024). Equivalence Classes of Quantum Error-Correcting Codes. DOI: 10.48550/arXiv.2406.12083. URL: https://arxiv.org/abs/2406.12083v1.

Commentary.

Conjecture 7.1 (arXiv:2406.12083v1, p. 20): “For positive integers n > k, the equivalence classes of [n,k] codes with a single connected component have sizes divisible by 3^k.” Here 0 < k and k < n express the positive integers. The carrier is SimpleGraph(Sum(Fin(k),Fin(n))). Normalized fixes the pivot positions and the three fixed adjacency blocks. Every normalized H in the equivalence class is required to be connected, as in the source’s figures. The cardinality counts labelled normalized graphs.

Theorem 1.9 (Divisibility by 3^k).

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

Resolves. Problems/khesin-li-2024-equivalence-class-sizes (proved) by D5/S3/Quantum/Codes/KhesinLiEquivalenceClasses.result.

Source. Repository-derived.

Acknowledgement. Andrey Boris Khesin, Alexander M. Li (2024). Equivalence Classes of Quantum Error-Correcting Codes. DOI: 10.48550/arXiv.2406.12083. URL: https://arxiv.org/abs/2406.12083v1.

Commentary.

For each input u and its matched pivot p, complement first at u and then at p. On their free-output adjacency rows this sends (b,c) to (c,b xor c), an order-three rotation. Local complementations at different pairs commute because the corresponding vertices are nonadjacent. If both rows vanished, u and p would form an isolated component; connectedness and k < n exclude this. Every nonidentity coordinate rotation therefore moves each class member. The free action of the product of k cyclic groups of order three partitions the class into equal orbits of size 3^k. The orbit decomposition in Mathlib gives the divisibility.

References