Bipartite encoder forms in an operation-generated class differ only by permutations and row operations

A. B. Khesin and A. M. Li, Equivalence Classes of Quantum Error-Correcting Codes (2024), arXiv:2406.12083v1, Section 8, Conjecture 8.3 (main.tex, lines 1768–1771):

In an equivalence class with bipartite forms, all bipartite forms in the class can be transformed from one to another using only output permutations, input permutations, and row operations on the input-output adjacency matrix.

The source introduces these forms as graphs with “no edges among output nodes” (main.tex, line 1631). Its Section 7 class construction uses the operations of Conjecture 6.3 (main.tex, lines 1557 and 1582–1584). The operations and their locators are recorded in the literature note.

Issue #26139 fixes the operation-generated reading. A graph has vertex set $\mathrm{Fin}(k)\sqcup\mathrm{Fin}(n)$, with inputs on the left and outputs on the right. A bipartite form has only input–output edges: neither input–input nor output–output edges. Equivalence is Relation.EqvGen Step, generated by local complementation, output permutations, input permutations, binary additions of distinct input rows, and input-edge removal. Local Clifford decorations are absent.

For all natural $k,n$ and all such bipartite forms $G,H$, claim says that operation-generated equivalence implies Relation.ReflTransGen BipartiteStep G H: a finite, possibly empty, sequence of output permutations, input permutations and binary additions of distinct input rows. This is proved. There is no positivity, connectedness, full-rank or normalization hypothesis.

Section 8 seeks simple representatives of encoder equivalence classes containing bipartite forms. The conjecture asks whether comparison of these forms can dispense with local complementation and input-edge removal. Its proposed application is an efficient equivalence test (main.tex, line 1767); the formal statement settles the reduction of allowed operations, without asserting a runtime bound.

Issue #26139 records the bounded literature check:

• The 2024 source states Conjecture 8.3 and suggests an entanglement-based approach (main.tex, lines 1770 and 1778), confirmed in the source TeX.
• The search author reports ten INSPIRE citing records and screening arXiv:2610.18218, 2512.00141, 2509.12355, 2501.17959, 2506.05478, 2606.02542 and 2509.09603, two INSPIRE-only works and a journal article, with no settlement found. The issue reports the conjecture repeated as Conjecture 5.8.3 in Khesin's Quantum Computing from Graphs (2025), arXiv:2501.17959v1.
• The repository check reported no existing dossier or preregistration for Conjecture 8.3; the sibling Conjecture 7.1 has a separate settlement in KhesinLiEquivalenceClasses.

not-found-in-searched-scope.

All matrices below are over $\mathbb F_2$, and $B_G$ is the $k\times n$ input–output adjacency matrix biadjacency G. For an output subset $S$, write $\rho_G(S)$ for entropy of its image in the vertex set: the rank of the adjacency block between that set and its complement.

1. Invariant on arbitrary intermediate graphs. For any graphs $G,H$ on this fixed vertex set with Step G H, step_profile gives an output permutation transporting every output cut rank. In the row-addition case, entropy_row requires distinct inputs $i\ne j$ and applies to every graph and output subset: the cut matrix is right-multiplied by an invertible transvection. Local complementation uses lc_source and the cut-rank invariance lc_eq; input permutations reindex the cut, and input-edge removal changes no entry of an output cut. For any $G,H$ with Relation.EqvGen Step G H, equivalence_profile therefore supplies an output permutation $\sigma$ such that the output relabelling $J$ of $G$ has the same profile as $H$.
2. Bipartite profiles count supported kernel vectors. For a graph $G$ bipartite with respect to the specified input and output sets, and every output subset $S$, bipartite_profile gives $\rho_G(S)=\operatorname{rank}((B_G)_S)$, where $(B_G)_S$ restricts the columns to $S$. For every binary $k\times n$ matrix $B$ and every $S$, supported_kernel_card gives $N_B(S):=|{u:Bu=0,\ \operatorname{supp}(u)\subseteq S}|=2^{|S|-\operatorname{rank}(B_S)}$. Thus equal bipartite profiles give equal supported-kernel counts, including for empty sets and rank-deficient matrices.
3. Recover the row space. For binary matrices $B,C$ of the same $k\times n$ shape, assuming $N_B(S)=N_C(S)$ for every $S$, kernel_recovery proves equality of their kernels. Every binary vector is the indicator $\mathbf1_T$ of its support, so $N_B(S)=\sum_{T\subseteq S}\mathbf1[B\mathbf1_T=0]$; the subset-sum inversion hyperlink_zeta recovers each summand. Given equality of these kernels, kernels_row_spaces proves equality of row spaces by the coordinate pairing and dual annihilators. Given equal row spaces of two binary matrices of this same shape, row_spaces_unit supplies an invertible $k\times k$ matrix $R$ with $C=RB$, without a full-rank hypothesis.
4. Realize the matrix operations. For bipartite $G,H$ on the specified partition, an invertible binary $k\times k$ matrix $R$, and $B_H=RB_G$, realize_row_equivalence gives the required restricted path. Its matrix induction uses invertible diagonal matrices, transvections and products: over $\mathbb F_2$ the diagonal factors are identities, and each nonidentity transvection adds one input row to a distinct input row. add_row_bipartite preserves bipartiteness for any bipartite graph and any input indices, while bipartite_ext identifies two bipartite graphs whose input–output matrices agree. For bipartite $G$ and any output permutation, permute_bipartite makes $J$ bipartite. Applying the preceding steps to $J,H$ and prepending the output permutation gives result : claim.

The result would not settle the registered reading if the graph partition, equivalence relation or restricted moves differed from the source interpretation. The module explicitly fixes:

• both endpoint graphs bipartite across inputs and outputs, excluding input–input edges as well as output–output edges;
• the equivalence closure of operations 1–5 on decoration-free graphs, allowing intermediate graphs that are not bipartite;
• exactly output permutations, input permutations and additions of distinct input rows modulo two in the conclusion.

This does not identify the operation-generated classes with quantum-code equivalence in Definition 6.2, prove Conjecture 6.3, or assert that every class contains a bipartite form. The source specifies addition modulo two at main.tex, line 1247; its Section 7 normalization removes input–input edges at line 1584.

The canonical source is D5/S3/Quantum/Codes/KhesinLiBipartiteEncoderEquivalence.lean.

• Proof. It proves result : claim.
• Axioms. It uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.

Frozen state: Golden/Frozen/state/D5/S3/Quantum/Codes/KhesinLiBipartiteEncoderEquivalence.lean.json.

Declaration statements:

• result: sha256:5cc103ed3900497f397283a97adffd4ed53e2ecf1df26927a4127f244ce6d9c7;
• claim: sha256:c97b0e3be88cef7fb138a2de049cde1b24d7d16f3037fbf0d01be332056c32f0.

Tier 1 conjecture of a 2024 preprint, preregistered in issue #26139 before any Lean. theorem; resolution proved.

The module is admitted under the open-problem-resolution basis of CLAUDE.md §3.2; the per-declaration proof shapes are listed in the delivery PR. There is no digestion atom.

What the settlement shows

Proved by result: for every natural $k,n$ and every pair of simple graphs $G,H$ on $\mathrm{Fin}(k)\sqcup\mathrm{Fin}(n)$ having only input–output edges, if Relation.EqvGen Step G H, then a finite, possibly empty, sequence of output permutations, input permutations and binary additions of distinct input rows carries $G$ to $H$.

Computed, not formalized: None.

Argued, not formalized.

• Decisive information. For binary $k\times n$ matrices with equal supported-kernel counts on every output subset, the mechanism in kernel_recovery is triangular reconstruction: subtract the contributions of proper subsets from $N_B(S)$ to recover whether $\mathbf1_S$ is in the kernel. This works from the empty set upwards because a binary vector is uniquely specified by its support. A single total rank discards that subset information.
• Endpoint sharpness. Allowing input–input edges would invalidate the conclusion. Take two inputs, no outputs, and compare the graph with its single input edge to the empty graph. Step.removeInputEdge relates them. Every restricted move preserves their input-edge counts: input permutations merely relabel, there are no outputs to permute, and add_row_adjacencies, valid for every graph and any input indices, says row addition keeps all input–input adjacencies. Hence no restricted path joins them.
• Binary boundary. The rank-profile reconstruction does not extend unchanged to larger fields. Over $\mathbb F_3$, the one-row matrices $(1,1)$ and $(1,2)$ have rank zero on the empty column set and rank one on every nonempty column set, but their kernels differ: $(1,-1)$ belongs to the former kernel and not the latter. Thus equal column-rank profiles alone cannot recover the kernel there.
• Effect on the paper and neighbouring questions. The equivalence-testing proposal preceding Conjecture 8.3 gains the asserted reduction of moves for the operation-generated reading. For fixed bipartite endpoints on the same input and output sets, this permits comparison by enumerating output permutations and comparing row spaces: necessity follows from the route; conversely, equal row spaces give an invertible $R$ by row_spaces_unit, and, for the permuted bipartite graph $J$ and bipartite target $H$ with $B_H=RB_J$, realize_row_equivalence gives a restricted path, each of whose moves is a Step. Enumerating permutations gives a finite test; an efficiency bound is unverified. The remainder of Section 8 suggests an entanglement obstruction and representatives for classes without bipartite forms; it states no further theorem. Existence of bipartite representatives for other classes, selection of a unique representative, an efficient test, and the Definition 6.2/Conjecture 6.3 bridge remain open here. The earlier Section 8 propositions are not re-proved by result.

The bounded literature check in #26139 does not establish exhaustive worldwide novelty or priority. The INSPIRE citation count, the screening of its citing works, the reported repetition in arXiv:2501.17959v1, and the issue's repository-wide absence check were not independently reproduced. The source reading here is arXiv:2406.12083v1 main.tex, including the conjecture, operations and Sections 7–8; it is not a reading of the cited follow-up works. The statements under “Argued, not formalized” are not additional formal conclusions of result. Quantum-code equivalence, completeness of the operations, algorithmic complexity, unique canonical representatives and classes lacking bipartite forms are outside this settlement.