Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A quaternary refutation of the length-five extension expectation

Abstract

The quaternary quantum extension property already fails at lengths one and three, so length five is not minimal.

Definition 1.1 (The trace map on the quaternary field).

Formalization. D5/S3/Quantum/Codes/StabilizerExtensionQuaternaryMinimalLength.tr (✓ std3).

Citation. Ali Assem Mahmoud (2026). Minimal Counterexamples of the MacWilliams Extension Theorem for Stabilizer Codes. DOI: 10.48550/arXiv.2607.26214. URL: https://arxiv.org/abs/2607.26214v1.

Commentary.

The carrier K 1 is the four-element field 𝔽₄, and tr x = x + x squared is its trace to the binary subfield. The label alphabet HilbertPhase (K 1) is A₄ = 𝔽₄² in the source’s notation (MzWi_Ext_Th.tex, lines 211–217).

Definition 1.2 (The trace-symplectic pairing).

Formalization. D5/S3/Quantum/Codes/StabilizerExtensionQuaternaryMinimalLength.symp (✓ std3).

Citation. Ali Assem Mahmoud (2026). Minimal Counterexamples of the MacWilliams Extension Theorem for Stabilizer Codes. DOI: 10.48550/arXiv.2607.26214. URL: https://arxiv.org/abs/2607.26214v1.

Commentary.

For two vectors u and v of labels, sum the determinant-like terms u_i.1 v_i.2 − v_i.1 u_i.2 and apply tr. The carrier HilbertPhase (K 1) is the label alphabet 𝔽₄², and the expression is the coordinate form of the trace-symplectic pairing in the source (MzWi_Ext_Th.tex, lines 211–215).

Definition 1.3 (Trace-symplectic self-orthogonality).

Formalization. D5/S3/Quantum/Codes/StabilizerExtensionQuaternaryMinimalLength.selfOrthogonal (✓ std3).

Citation. Ali Assem Mahmoud (2026). Minimal Counterexamples of the MacWilliams Extension Theorem for Stabilizer Codes. DOI: 10.48550/arXiv.2607.26214. URL: https://arxiv.org/abs/2607.26214v1.

Commentary.

An additive subgroup C is self-orthogonal when the trace-symplectic pairing of every two of its elements is zero. This is the self-orthogonality condition imposed on additive stabilizer codes in the source (MzWi_Ext_Th.tex, lines 217 and 237–239).

Definition 1.4 (A monomial extension witness).

Formalization. D5/S3/Quantum/Codes/StabilizerExtensionQuaternaryMinimalLength.qepWitness (✓ std3).

Citation. Ali Assem Mahmoud (2026). Minimal Counterexamples of the MacWilliams Extension Theorem for Stabilizer Codes. DOI: 10.48550/arXiv.2607.26214. URL: https://arxiv.org/abs/2607.26214v1.

Commentary.

A permutation π of the coordinates and a determinant-one two-by-two matrix τ_i at each coordinate witness an extension when f u at coordinate i equals τ_i applied to u at the coordinate π⁻¹(i). The determinant-one condition is the concrete symplectic condition for the quaternary label alphabet, matching the monomial transformation in Definition 2.1 (MzWi_Ext_Th.tex, lines 221–223).

Definition 1.5 (The quaternary quantum extension property).

Formalization. D5/S3/Quantum/Codes/StabilizerExtensionQuaternaryMinimalLength.QEP (✓ std3).

Citation. Ali Assem Mahmoud (2026). Minimal Counterexamples of the MacWilliams Extension Theorem for Stabilizer Codes. DOI: 10.48550/arXiv.2607.26214. URL: https://arxiv.org/abs/2607.26214v1.

Commentary.

QEP n asserts that every pair of self-orthogonal additive subgroups of the label alphabet at length n, together with every additive bijection preserving Hamming weight, has a witness of the preceding monomial form. This is the source’s Definition 2.3 specialized to q = 4 (MzWi_Ext_Th.tex, lines 237–239).

Definition 1.6 (The extension property for coordinate additive automorphisms).

Formalization. D5/S3/Quantum/Codes/StabilizerExtensionQuaternaryMinimalLength.QEPAdd (✓ std3).

Citation. Ali Assem Mahmoud (2026). Minimal Counterexamples of the MacWilliams Extension Theorem for Stabilizer Codes. DOI: 10.48550/arXiv.2607.26214. URL: https://arxiv.org/abs/2607.26214v1.

Commentary.

QEPAdd n has the same hypotheses as QEP n, but permits an arbitrary additive equivalence of the label alphabet at each coordinate in the extension equation. For K 1 = 𝔽₄, this is the full coordinatewise additive-automorphism version described alongside the symplectic group in Definition 2.1 (MzWi_Ext_Th.tex, lines 221–223).

Definition 1.7 (The expected minimal length five).

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

Citation. Ali Assem Mahmoud (2026). Minimal Counterexamples of the MacWilliams Extension Theorem for Stabilizer Codes. DOI: 10.48550/arXiv.2607.26214. URL: https://arxiv.org/abs/2607.26214v1.

Commentary.

The claim is the disjunction of two leastness assertions: either 5 is the least positive length where QEP fails, or 5 is the least positive length where QEPAdd fails. It is the q = 4 instance of the expectation that the minimal counterexample length is q + 1 (MzWi_Ext_Th.tex, lines 427–430).

Theorem 1.8 (Lengths one and three refute the length-five claim).

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

Resolves. Problems/mahmoud-2026-quaternary-extension-minimal-length-refutation (refuted) by D5/S3/Quantum/Codes/StabilizerExtensionQuaternaryMinimalLength.result.

Source. Repository-derived.

Acknowledgement. Ali Assem Mahmoud (2026). Minimal Counterexamples of the MacWilliams Extension Theorem for Stabilizer Codes. DOI: 10.48550/arXiv.2607.26214. URL: https://arxiv.org/abs/2607.26214v1.

Commentary.

Choose an element w of the four-element field with w different from 0 and 1. For length one, use the additive maps (a,b) ↦ (a + b w, 0) and (a,b) ↦ (a,b) from the binary pair space into the one-coordinate label alphabet. Their images are self-orthogonal, the induced additive equivalence preserves Hamming weight, and the only coordinate permutation is the identity. If a determinant-one matrix extended this equivalence, the image of (1,0) would force its lower-left entry to be zero; its action on the source label (w,0), corresponding to the binary parameter (0,1), would then force 1 = 0 times w, a contradiction. Thus QEP 1 fails.

For length three, use the additive maps (a,b) ↦ ((a,b w),(a,b w),(0,0)) and (a,b) ↦ ((a+b,0),(a,0),(b,0)). Their images are self-orthogonal and the induced equivalence preserves Hamming weight. If a coordinatewise additive extension existed, let j be the image of coordinate 2 under its permutation. Every vector in the first image is zero at coordinate 2, so every image under the extension is zero at j. Additive surjectivity would then make every element of the second image zero at j, but explicit elements of that image are nonzero at each of the three coordinates. This contradiction proves QEPAdd 3 fails.

The first leastness assertion in the claim cannot hold because 1 is a positive member of its failure set, and the second cannot hold because 3 is a positive member of its failure set. The two smaller counterexample lengths contradict the asserted least value 5.

References