The Optimal Distance of Fourteen-Qubit Stabilizer Codes Encoding Three Qubits

We prove, with computer assistance, that the optimal minimum distance of abinary stabilizer code on $14$ qubits encoding $3$ logical qubits is $4$.Equivalently, no binary quantum stabilizer code with parameters14,3,5 exists, including degenerate codes. In the binary symplecticmodel, this is equivalent to the nonexistence of an $11$-dimensional isotropicsubspace C⊆₂²⁸ satisfyingmin\(v):v∈ C^ C\≥ 5.The argument separates the two cases determined by the parity of thestabilizer weights. MacWilliams identities and integrality eliminate theall-even case. In the odd case, the shadow enumerator of Rains is combined withtwo averages over the $135$ self-dual extensions of the code: one for theirweight enumerators and one for their shadows. An incidence computation inan eight-dimensional orthogonal geometry of plus type then forces threelow-weight stabilizer profiles. Integrality and a collision count amongweight-three shadow words eliminate these profiles. All parameter-specificcalculations are finite and exact, and reproducible source code accompanies the paper.The nonexistence theorem is additionally formalized and machine-checked inLean~4 over mathlib, with an axiom audit reporting only standard foundationalprinciples.