Exact minimal lengths for constant-excitation quantum codes: eight qubits for stabilizer codes, twelve and fourteen for CSS

The reduction: constant excitation is exactly C1 subset V_y, and the shift may be sorted to 1ʷ 0ⁿ⁻ʷ

The pruned depth-first enumeration of subspaces of V_y is complete, so a true from the search refutes every code

Headline: no [[10,1,d>=3]] and no [[11,1,d>=3]] constant-excitation CSS code exists; with n <= 9 re-derived, n = 12 is the exact threshold

Validation: the source's [[12,1,3]] code reproduced from its printed stabilizers, with distance exactly 3

Negative controls: too strong, too weak, corruption, and the source's [[4,1,2]] code reproduced ket for ket

The k-transport: CodeK n y k with k ≥ 1 implies CodeK n y 1, so no [[n,k,d>=3]] CE CSS code with any k >= 1 exists for n <= 11 (no_codeKₗeₑleven); CodeK n y 1 = Code n y

The k >= 2 reduction: three surviving functionals (CodeK.toPair), complement + sorting of the shift (Pair.reduce) halving every sweep

Soundness of the k >= 2 sweep: dfs2ₛound, the MK-to-list-world equalities, bitsOfₓor, noₚairₒfₛweeps, CodeK.toTwo

Headline: no [[n,k,d>=3]] CE CSS code with k >= 2 exists for n <= 13; with the verified [[14,3,3]], n = 14 is the exact threshold for multiple logical qubits — the source's "smallest via Theorem 3" qualification drops for k > 1 as it did for k = 1

Validation: the source's [[14,3,3]] code reproduced from its printed stabilizers (codeFourteen), basis pinned to the printed Z-generators, distance exactly 3 with d_X = 4, 7-CE

Controls: searchY2 14 127 = false from the witness through soundness (no sweep run); hasD2 accepts the 14-node; the [[12,1,3]] node separates k = 1 from k >= 2 (10 survivors, no 2-dim subspace); shrinking C₂ to claim k = 4 dies at a weight-1 error; d_Z non-vacuity; k >= 2 sweep consistent with k = 1 theorems on n <= 11

Scope, verified, and an erratum: both published eight-qubit distance-3 CE codes are non-CSS as the family's n ≤ 9 theorem requires; PVK's own (C₁, C₂, y) satisfies every structural field of Code 8 y and fails only d_X (= 2); the Error Correction Zoo entry /c/qubit₈₁₃ mis-states PVK's |1̄⟩, so this family's 2026-08-28 family.json note on PVK is withdrawn

The stabilizer layer and its reduction: packed Paulis with the symplectic form; constant excitation is exactly Z^(tensor n) in S together with pi(S) subset V_y; the shift may be sorted and complemented; the canonical-basis search is complete (stab_dfsₛound, noₛtabₒfₛearchAll)

Validation: Plenio-Vedral-Knight's and En-Jui Chang's [[8,1,3]] constant-excitation codes reproduced in Lean from their printed equations – isotropic of order 128, Z^(tensor 8) in the stabilizer, pi(S) subset V₁5, distance exactly 3, and NOT CSS; PVK's printed codewords are 4-CE, two-dimensional, and stabilized by the printed Paulis with the printed signs

Erratum, now kernel-bound: the Error Correction Zoo's /c/qubit₈₁₃ writes |1bar> = X^(tensor 8)|0bar>, which differs from PVK Eq. (8) in exactly four amplitudes; the weight-2 Pauli X4X5 carries |0bar> to the zoo's |1bar> exactly, so the zoo's code has distance 2, not the 3 in its own title, and is additive; the same operator does not act on PVK's own pair. Also: the seventh generator printed in arXiv:2503.05249v1 Appendix A anticommutes with two of the other six

Controls for the stabilizer half: the node test accepts PVK's span (the checker can say yes); searchY 8 15 = false derived from the witness with no sweep run; Steane's [[7,1,3]] has k = 1 and d >= 3 at exactly n = 7 but no shift makes it constant-excitation

Headline: no [[n, k >= 1, d >= 3]] constant-excitation STABILIZER code exists for n <= 7, with any shift; with Plenio-Vedral-Knight's verified [[8,1,3]], eight qubits is the exact minimum – the first proof of a minimality PVK asserted in 1996 from an undescribed computer search after withdrawing an unsound argument, and the first result of any kind for the non-CSS case