Researcher-in-the-Loop Evolutionary Discovery of Entanglement-Assisted Quantum Code Families

# Researcher-in-the-loopEvolutionary Discovery ofentanglement-assisted quantum code families
Source: [https://arxiv.org/html/2610.41183](https://arxiv.org/html/2610.41183)
## Researcher\-in\-the\-loop Evolutionary Discovery of entanglement\-assisted quantum code families

Jae\-Hyun BaekAffiliation:Department of Artificial Intelligence, Sogang University, Seoul, KoreaAffiliation:Institute for Mathematical and Data Sciences, Sogang University, Seoul, KoreaByung\-Sun WonJon\-Lark Kim††thanks:Corresponding author:jlkim@sogang\.ac\.krAffiliation:Institute for Mathematical and Data Sciences, Sogang University, Seoul, KoreaAffiliation:Department of Mathematics, Sogang University, Seoul, Korea

###### Abstract

LLM\-guided program evolution can produce mathematical constructions, but validity, generality, and reproducibility require distinct evidence\. We develop a researcher\-in\-the\-loop discovery pipeline that combines program evolution, exact evaluation, mathematical generalization, certified nonexistence checks, and formal proof checking\. We apply it to entanglement\-assisted quantum error\-correcting codes \(EAQECCs\)\. Starting from tasks that did not specify a family formula, evolved programs produced finite qubit constructions whose structure researchers generalized to the family\[\[n,1,n−1;n−q−1\]\]q\[\[n,1,n\-1;n\-q\-1\]\]\_\{q\}for prime powersq≥3q\\geq 3atn≥2​q\+1n\\geq 2q\+1and forq=2q=2at oddn≥5n\\geq 5\. Lean checks the algebraic certificate underlying this family\. Together with entanglement lifting, the family closes 54 gaps in archived EAQECC tables\. The released evidence includes 115 verified code records, ten nonexistence results with checked DRAT proofs, family implementations, and preserved search programs for exact checks and seeded replay\. In a controlled cohort of eight paired generation blocks, validation\-selected iterative programs achieve success in 46\.1% and 31\.6% of held\-out executions at unseen lengthsn=13,15n=13,15, compared with 19\.5% and 3\.1% for independently generated programs\. In this setting, program evolution and researcher analysis turn finite computational discoveries into a proved family with independently checkable evidence\.

## 1Introduction

LLM\-guided program search has produced mathematical constructions and algorithms\([Romera\-Paredes et al\., 2024](https://arxiv.org/html/2610.41183#bib.bib18);[Novikov et al\., 2025](https://arxiv.org/html/2610.41183#bib.bib15)\)\. Their outputs can also support general mathematical results through researcher analysis\. This raises three questions:*whether evolved programs produce valid codes, whether their structure can be generalized and proved to work beyond the searched cases, and whether the resulting constructions and preserved searches can be independently reproduced*\. Addressing these questions requires records of the initial task, computational discoveries and subsequent mathematical analysis\.

We study this process for entanglement\-assisted quantum error\-correcting codes \(EAQECCs\)\. Early AlphaEvolve searches produced finite qubit codes whose structure led us to an infinite qubit family\. Further mathematical generalization gives the prime\-power construction and proof in Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)\. The initial instructions suggested directions such as cyclic shifts, but did not provide this family formula\. Later instructions explicitly incorporated the discovered qubit family \(Appendix[B\.3](https://arxiv.org/html/2610.41183#A2.SS3)\), allowing it to guide further searches\.

Our reproducibility contribution concerns these mathematical constructions and their computational evidence\. The[artifact](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)supplies code matrices, family implementations, proofs, task specifications and preserved search programs\. Readers can recompute code parameters, construct and verify family instances, inspect the proof and replay preserved searches\. Figure[1](https://arxiv.org/html/2610.41183#S3.F1)summarizes how researcher analysis and program evolution interact\. Section[3\.4](https://arxiv.org/html/2610.41183#S3.SS4)specifies which operations are reproducible\. A final Lean stage checks the algebraic construction underlying Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)\(Appendix[D](https://arxiv.org/html/2610.41183#A4)\); model generation remains stochastic\.

Several improvements concern constructions published in 2020 and 2022 that remained listed in the EAQECC tables accessed on 17 July 2026\([Grassl et al\., 2020](https://arxiv.org/html/2610.41183#bib.bib8);[Luo et al\., 2022](https://arxiv.org/html/2610.41183#bib.bib13)\)\. Our constructions and certified exclusions close nine previously tabulated qubit distance gaps \(Table[2](https://arxiv.org/html/2610.41183#S4.T2)\)\. The prior constructions predate our table access by approximately four to six years\. Their dates document available constructions rather than a complete history of improvement attempts\.

Our contributions are:

- •A researcher\-in\-the\-loop discovery pipeline\.We connect LLM\-guided program evolution with researcher proposals, mathematical generalization and formal proof checking for EAQECC discovery\. Preserved programs, code matrices and formal certificates support reconstruction and independent verification of the resulting constructions \(Sections[3](https://arxiv.org/html/2610.41183#S3)and[3\.4](https://arxiv.org/html/2610.41183#S3.SS4)\)\.
- •General constructions from evolved program outputs\.Finite qubit constructions led to the general family of Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1), whose algebraic construction is checked in Lean\. The family and entanglement lifting close 54 listed gaps, while checked nonexistence certificates establish selected optimality and minimum\-entanglement results \(Section[4](https://arxiv.org/html/2610.41183#S4)\)\.
- •Program development and generalization\.We compare independent and iterative generation under shared research guidance\. Eight new generation blocks yield longer\-code success of 46\.1% and 31\.6% for iterative programs, versus 19\.5% and 3\.1% for independent proposals atn=13,15n=13,15\. Preserved lineages identify useful objective and search\-policy changes \(Section[5](https://arxiv.org/html/2610.41183#S5)\)\.

## 2Background and related work

### 2\.1Entanglement\-assisted quantum error\-correcting codes

Quantum error correction protects quantum information sent through noisy communication links\. Early stabilizer constructions imposed algebraic compatibility constraints that limited which classical codes could be reused\.[Brun et al\. \(2006\)](https://arxiv.org/html/2610.41183#bib.bib2)showed that entanglement shared in advance between sender and receiver relaxes these constraints, enabling a broader class of quantum codes\. This is the motivation for entanglement\-assisted quantum error\-correcting codes \(EAQECCs\)\.

A code with parameters\[\[n,k,d;c\]\]q\[\[n,k,d;c\]\]\_\{q\}encodeskklogical qudits intonntransmittedqq\-level systems usingccshared maximally entangled qudit pairs\. Each pair containslog2⁡q\\log\_\{2\}qebits, equal to one for qubits \(q=2q=2\)\([Grassl et al\., 2022](https://arxiv.org/html/2610.41183#bib.bib9)\)\. The receiver’s halves are assumed noiseless and are not counted innn\.

The distancedddetermines the code’s guaranteed error protection\. With ideal decoding, it corrects arbitrary errors on up to⌊\(d−1\)/2⌋\\lfloor\(d\-1\)/2\\rfloortransmitted qudits, or up tod−1d\-1*erasures*, where the lost qudits’ locations are known\([Brun et al\., 2006](https://arxiv.org/html/2610.41183#bib.bib2);[Grassl et al\., 2022](https://arxiv.org/html/2610.41183#bib.bib9)\)\. Increasingddat fixed\(q,n,k,c\)\(q,n,k,c\)strengthens protection without increasing the transmission or entanglement budget\. For example, our\[\[12,1,11;8\]\]2\[\[12,1,11;8\]\]\_\{2\}code raises the listed distance from 9 to 11, increasing the guaranteed correction of arbitrary errors from four to five transmitted qubits with the same resources \(Table[2](https://arxiv.org/html/2610.41183#S4.T2)\)\. A verified code thus provides an encoding specification for a quantum link with given resource and error\-protection requirements\. Reducingccat fixed\(n,k,d\)\(n,k,d\)instead lowers the entanglement needed before transmission\([Luo et al\., 2022](https://arxiv.org/html/2610.41183#bib.bib13)\)\.

### 2\.2Code discovery as program search

We search linear stabilizer EAQECCs represented by generator matrices over𝔽q\\mathbb\{F\}\_\{q\}\. The LLM revises a search program that proposes matrices; an exact evaluator computes their\(k,c,d\)\(k,c,d\)\. At fixed\(q,n,k,c\)\(q,n,k,c\), reference tables give a constructed lower distance bounddℓd\_\{\\ell\}and an upper bounddud\_\{u\}\([Grassl, 2026](https://arxiv.org/html/2610.41183#bib.bib7);[Luo et al\., 2022](https://arxiv.org/html/2610.41183#bib.bib13)\)\. Findingd\>dℓd\>d\_\{\\ell\}improves the lower bound, while reachingdud\_\{u\}closes the gap\. We also construct codes at unlisted cells and minimize entanglement, denotedcmins​\(n,k,d\)c^\{\\mathrm\{s\}\}\_\{\\min\}\(n,k,d\)within our stabilizer class\. Applicable bounds filter impossible targets\([Grassl et al\., 2022](https://arxiv.org/html/2610.41183#bib.bib9)\); Appendix[A](https://arxiv.org/html/2610.41183#A1)gives the representation, notation and comparison rules\.

FunSearchevolves programs that construct mathematical objects or make algorithmic decisions, using an evaluator to select useful revisions\. It produced larger cap\-set constructions and improved online bin\-packing heuristics\([Romera\-Paredes et al\., 2024](https://arxiv.org/html/2610.41183#bib.bib18)\); its executable outputs let researchers inspect and develop the underlying mathematical ideas\.AlphaEvolveextends this approach to matrix\-multiplication algorithms, data\-center scheduling, hardware\-circuit simplification and model\-training kernels\([Novikov et al\., 2025](https://arxiv.org/html/2610.41183#bib.bib15);[Georgiev et al\., 2025](https://arxiv.org/html/2610.41183#bib.bib5)\)\. Related frameworks includeOpenEvolve,CodeEvolve,ShinkaEvolveandTurboEvolve, which implement or extend evaluator\-guided program evolution with population management and proposal\-selection strategies\([Sharma, 2025](https://arxiv.org/html/2610.41183#bib.bib19);[Assumpção et al\., 2026](https://arxiv.org/html/2610.41183#bib.bib1);[Lange et al\., 2025](https://arxiv.org/html/2610.41183#bib.bib11);[Yang et al\., 2026](https://arxiv.org/html/2610.41183#bib.bib25)\)\. We useAlphaEvolveas the evolution engine for EAQECC discovery, supplying target parameters, an exact evaluator and researcher\-directed construction ideas\.

Quantum\-code discovery also uses genetic algorithms to evolve stabilizer representations\([Webster & Browne, 2024](https://arxiv.org/html/2610.41183#bib.bib22)\), and reinforcement learning to optimize codes and encoders\([Poulsen Nautrup et al\., 2019](https://arxiv.org/html/2610.41183#bib.bib17);[Su et al\., 2025](https://arxiv.org/html/2610.41183#bib.bib21);[Mauron et al\., 2023](https://arxiv.org/html/2610.41183#bib.bib14);[Olle et al\., 2024](https://arxiv.org/html/2610.41183#bib.bib16)\)\. More directly,[Cruz\-Benito et al\. \(2026\)](https://arxiv.org/html/2610.41183#bib.bib4)evolve Python generators for bivariate bicycle codes, verify candidates, and derive structural results\. Our contribution concerns EAQECC distance–entanglement targets: exact finite\-field evaluation supports finite constructions, a prime\-power family with a Lean\-checked algebraic certificate, and certified nonexistence results\. The controlled study compares independent proposals with iterative program feedback under a shared researcher proposal\.

## 3The researcher\-in\-the\-loop discovery pipeline

Our discovery pipeline combines human\-in\-the\-loop \(HITL\) research with LLM\-guided program evolution and exact verification\. Researchers propose construction ideas, inspect verified instances and revise the task between campaigns\. Figure[1](https://arxiv.org/html/2610.41183#S3.F1)connects these interventions to the automated search and evaluation loop\. Constructed codes establish lower distance bounds; SAT refutations with checked certificates lower upper bounds\. Independent verification and archived evidence support both routes\. Researchers generalize the discovered constructions and develop proofs, then pass the formalized statements and proofs to the Lean checking stage\.

Researcherin the loopPropose and revise ideasbetween campaignsGeneralize and provefrom discovered codes![Refer to caption](https://arxiv.org/html/2610.41183v1/assets/lean_logo.png)Machine\-check proofs01 TARGET02 EVOLVE03 VERIFY04 DISCOVERnndℓ​–​dud\_\{\\ell\}\\;\\text\{\-\-\}\\;d\_\{u\}775​–​65\\;\\text\{\-\-\}\\;6997​–​87\\;\\text\{\-\-\}\\;811119​–​109\\;\\text\{\-\-\}\\;10Reference tablesKnown boundsLLM evolvesa programGeneratorsExact evaluatorfeedback![Refer to caption](https://arxiv.org/html/2610.41183v1/assets/python_logo.png)![Refer to caption](https://arxiv.org/html/2610.41183v1/assets/magma_logo.png)Recomputek,c,dk,c,dSAT \+ DRAT proof checkCertify nonexistencedℓ↑d\_\{\\ell\}\\uparrowdu↓d\_\{u\}\\downarrowTighten code bounds\[\[11,1,10;8\]\]2\[\[11,1,10;8\]\]\_\{2\}11510codesexclusionsnonexistence targetstask specificationinspect codes

Figure 1:The researcher\-in\-the\-loop discovery pipeline\.### 3\.1Target selection

We compare our constructions with the bounds listed in the EAQECC tables \(codetables\.de\), accessed on 17 July 2026\. These reference bounds define listed\-gap and absent\-cell targets, filtered using the EA\-Plotkin and applicable Singleton bounds\. EA\-Plotkin also tightens 398 upper bounds in the reference qubit table\. Appendix[A\.3](https://arxiv.org/html/2610.41183#A1.SS3)gives the table records and filters\. The artifact preserves these comparison data and uses them by default\. A second copy, retrieved on 10 September 2026, contains identical intervals at all 11,640 qubit and qutrit entries\.

### 3\.2LLM\-guided program evolution

The qubit discovery campaigns use AlphaEvolve\([Novikov et al\., 2025](https://arxiv.org/html/2610.41183#bib.bib15)\)through Google Cloud Vertex AI\. We provide a seed program, task specification and exact evaluator; AlphaEvolve generates revisions and archives their source and outcomes\. An LLM modifies a designated block of the seed\. Within each candidate program, an exact parameter oracle evaluates intermediate matrices; the program uses these results to choose targets, accept local moves and restart search\. Algorithm[1](https://arxiv.org/html/2610.41183#alg1), for example, minimizes a cost combining signature mismatch and the number of logical operators below the target distance\.

After the program returns up to 16 matrices, the external evaluator recomputes their parameters and assigns the best proposal score to the program\. Its reward favors a valid signature, fewer low\-weight logical operators and newly achieved targets\. This reward guides the next program revision; the inner cost guides matrix search within one execution\. Independent code checking follows in Section[3\.3](https://arxiv.org/html/2610.41183#S3.SS3)\.

Each candidate runs in its own subprocess with a fixed 240 s budget and a specified seed for its random\-number generator\. Failures receive a low score, and the campaign continues\. The same interface supports fixed\-program replay \(Section[3\.4](https://arxiv.org/html/2610.41183#S3.SS4)\)\. The four campaign logs record401401completed candidate searches, corresponding to26\.726\.7h of allocated search budget \(Appendix[B\.1](https://arxiv.org/html/2610.41183#A2.SS1)\)\.

The initial task specification did not contain the family proved in Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)\. We started with an annealing seed and instructions suggesting cyclic shifts among other construction directions\. Evolved programs produced finite qubit codes; analysis of their structure led researchers to a general qubit family and its proof\. The later task specifications included that family and requested further constructions, while the best program was reused as a new seed\. These records distinguish the initial discovery stage from subsequent search using the mathematical result \(Appendix[B\.3](https://arxiv.org/html/2610.41183#A2.SS3)\)\. The current prime\-power theorem extends the qubit construction through further researcher\-led generalization and proof\.

### 3\.3Independent verification and nonexistence checking

The Magma export supplies only a basis of the symplectic dualL=S⟂L=S^\{\\perp\}, whereSSis the stabilizer space\. Magma independently recomputes the dual, radical and\(k,c,d\)\(k,c,d\)\(Appendix[A\.1](https://arxiv.org/html/2610.41183#A1.SS1)\)\. All 148 objects—115 core codes atq=2,3,4,5q=2,3,4,5and 33 family instances—were re\-verified with zero mismatches under Magma V2\.28\-20\. Separate𝔽2\\mathbb\{F\}\_\{2\}linear\-algebra checks verify the two solver\-refined qubit codes; all code records can also be checked in Python using the[artifact](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)\. Lean checks the algebraic certificate underlying Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)\. A separate Comparator run checks the submitted proof against the exact formal goal and permitted axioms \(Appendix[D](https://arxiv.org/html/2610.41183#A4)\)\.

To test existence of an\[\[n,k,d;c\]\]q\[\[n,k,d;c\]\]\_\{q\}code, we encode the smaller subspaceL=S⟂L=S^\{\\perp\}in symplectic normal form\. Constraints enforce the target signature directly, so every satisfying assignment specifies an EAQECC\. Distance constraints dominate the encoding\.

For an unsatisfiable encoding, the SAT solver produces a DRAT proof, a certificate of unsatisfiability checked independently by DRAT\-trim\([Wetzler et al\., 2014](https://arxiv.org/html/2610.41183#bib.bib23)\)\. Together with the encoding’s completeness, this establishes the corresponding code nonexistence result\. The qutrit encoding uses a coordinate\-normalization lemma to preserve completeness\. Appendix[B\.2](https://arxiv.org/html/2610.41183#A2.SS2)gives the proof scope and encoding, and Section[4\.3](https://arxiv.org/html/2610.41183#S4.SS3)reports the certified results\.

### 3\.4Reproducibility

Readers can reconstruct two outputs: code constructions and preserved program executions\. Supplied matrices support exact\(k,c,d\)\(k,c,d\)checks; family implementations generate instances, and Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)proves the construction for all admissible parameters\. Task specifications and discovery logs document the progression from finite qubit codes to the researcher\-derived family \(Appendix[B\.1](https://arxiv.org/html/2610.41183#A2.SS1)\)\. Source replay concerns retained programs, including later programs that use this family\. It replaces wall time with a virtual clock tied to evaluator calls and preserves the recorded random\-number seeds and stopping conditions\. Three programs with four seeds each reproduce all twelve stored proposal lists, with agreement between one and four workers\. The[artifact](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)provides these inputs, independent parameter checks and reference\-bound audits\.

## 4Results

Algorithm[1](https://arxiv.org/html/2610.41183#alg1)presents a later, high\-scoring AlphaEvolve program whose seed already incorporated the discovered qubit family\. It illustrates continued search after that generalization\. Figure[2](https://arxiv.org/html/2610.41183#S4.F2)and the shading show changes to target selection, reuse of stored proposals, construction choices and generator\-row mutations\. The earlier discoveries that motivated the theorem are recorded separately \(Appendix[B\.1](https://arxiv.org/html/2610.41183#A2.SS1)\)\. Section[5](https://arxiv.org/html/2610.41183#S5)evaluates iterative feedback using newly generated programs, including Algorithm[2](https://arxiv.org/html/2610.41183#alg2)in Appendix[C\.5](https://arxiv.org/html/2610.41183#A3.SS5)\.

Algorithm 1Search program evolved by AlphaEvolve\.1:targets

𝒯\\mathcal\{T\}, time allowance

BB
2:

Φ\(r,t\)=5000\|r\.c−ct\|\+1000\|r\.k−kt\|\+r\.offending\\Phi\(r,t\)=5000\|r\.c\-c\_\{t\}\|\+1000\|r\.k\-k\_\{t\}\|\+r\.\\mathrm\{offending\}
3:

b​e​s​t←\{\}best\\leftarrow\\\{\\\};bt←0b\_\{t\}\\leftarrow 0for allt∈𝒯t\\in\\mathcal\{T\}

4:whiletime remainsdo

5:

πt∝nt−1\.5​\(1\+10​bt\)\\pi\_\{t\}\\propto\\hbox\{\\pagecolor\{achieve\!13\}$n\_\{t\}^\{\-1\.5\}\(1\+10b\_\{t\}\)$\}; sample

t∼πt\\sim\\pi⊳\\trianglerightUse recorded progress to change target selection\.

6:

n←ntn\\leftarrow n\_\{t\};

s←nt−kt\+cts\\leftarrow n\_\{t\}\-k\_\{t\}\+c\_\{t\};

u∼Uniform\[0,1\)u\\sim\\mathrm\{Uniform\}\[0,1\)
7:ifu<0\.2u<0\.2,t∈b​e​s​tt\\in bestandb​e​s​t​\[t\]\.o\>0best\[t\]\.o\>0then

8:

𝐆←copy\(best\[t\]\.𝐆\)\\mathbf\{G\}\\leftarrow\\hbox\{\\pagecolor\{achieve\!13\}$\\operatorname\{copy\}\(best\[t\]\.\\mathbf\{G\}\)$\}⊳\\trianglerightResume from this target’s stored best proposal\.

9:else

10:

𝐆←Construct​\(t,u\)\\mathbf\{G\}\\leftarrow\\hbox\{\\pagecolor\{achieve\!13\}$\\textsc\{Construct\}\(t,u\)$\}⊳\\trianglerightExpand construction choices\.

11:endif

12:if

𝐆\\mathbf\{G\}is undefined or

rank⁡𝐆≠s\\operatorname\{rank\}\\mathbf\{G\}\\neq sthen

13:

𝐆←RandomStabilizer​\(n,s\)\\mathbf\{G\}\\leftarrow\\textsc\{RandomStabilizer\}\(n,s\)
14:endif

15:

o←Φ⁡\(Evaluate​\(n,𝐆,dt\),t\)o\\leftarrow\\Phi\(\\textsc\{Evaluate\}\(n,\\mathbf\{G\},d\_\{t\}\),t\);

KeepBest​\(b​e​s​t,t,𝐆,o\)\\textsc\{KeepBest\}\(best,t,\\mathbf\{G\},o\)
16:if

o=0o=0then continue

17:

τ←30\\tau\\leftarrow 30;

f←0f\\leftarrow 0
18:while

f<1500f<1500andtime remainsdo

19:

τ←max⁡\(0\.1,0\.995​τ\)\\tau\\leftarrow\\max\(0\.1,0\.995\\tau\)
20:

𝐆′←MixedMove​\(𝐆\)\\mathbf\{G\}^\{\\prime\}\\leftarrow\\hbox\{\\pagecolor\{achieve\!13\}$\\textsc\{MixedMove\}\(\\mathbf\{G\}\)$\}⊳\\trianglerightAdd cyclic rotation of a whole generator row\.

21:if

rank⁡𝐆′≠s\\operatorname\{rank\}\\mathbf\{G\}^\{\\prime\}\\neq sthen

f←f\+1f\\leftarrow f\+1;continue

22:

o′←Φ⁡\(Evaluate​\(n,𝐆′,dt\),t\)o^\{\\prime\}\\leftarrow\\Phi\(\\textsc\{Evaluate\}\(n,\\mathbf\{G\}^\{\\prime\},d\_\{t\}\),t\);

Δ←o′−o\\Delta\\leftarrow o^\{\\prime\}\-o
23:Set

\(𝐆,o\)←\(𝐆′,o′\)\(\\mathbf\{G\},o\)\\leftarrow\(\\mathbf\{G\}^\{\\prime\},o^\{\\prime\}\)with probability

min\{1,exp\(−Δ/τ\)\}\\min\\\{1,\\exp\(\-\\Delta/\\tau\)\\\}
24:

f←0f\\leftarrow 0on an accepted strict improvement, otherwise

f←f\+1f\\leftarrow f\+1
25:

KeepBest​\(b​e​s​t,t,𝐆,o\)\\textsc\{KeepBest\}\(best,t,\\mathbf\{G\},o\);if

o=0o=0then break

26:endwhile

27:bt←ProgressBonus​\(b​e​s​t,t,bt\)b\_\{t\}\\leftarrow\\textsc\{ProgressBonus\}\(best,t,b\_\{t\}\)

28:endwhile

29:returnup to 16 stored proposals with the smallest objective values

Shading: principal changes from the campaign seed; routine definitions are in Appendix[B\.1](https://arxiv.org/html/2610.41183#A2.SS1)\.

Campaign seedEvolved program \(Algorithm[1](https://arxiv.org/html/2610.41183#alg1)\)Target selectionπt∝nt−2\\pi\_\{t\}\\propto n\_\{t\}^\{\-2\}fixed length\-based weightsπt∝nt−1\.5​\(1\+10​bt\)\\pi\_\{t\}\\propto n\_\{t\}^\{\-1\.5\}\(1\+10b\_\{t\}\)stored costnear\-miss bonusbtb\_\{t\}Search initializationfresh candidaterepairnew initialization on each attemptsavedb​e​s​t​\[t\]best\[t\]resume repairupdateb​e​s​t​\[t\]best\[t\]conditional reuse on a later attemptGenerator mutationX\\mathrm\{X\}I\\mathrm\{I\}Z\\mathrm\{Z\}Y\\mathrm\{Y\}I\\mathrm\{I\}X\\mathrm\{X\}X\\mathrm\{X\}I\\mathrm\{I\}Z\\mathrm\{Z\}Y\\mathrm\{Y\}Z\\mathrm\{Z\}X\\mathrm\{X\}local Pauli update \(example\)X\\mathrm\{X\}I\\mathrm\{I\}Z\\mathrm\{Z\}Y\\mathrm\{Y\}I\\mathrm\{I\}X\\mathrm\{X\}I\\mathrm\{I\}X\\mathrm\{X\}X\\mathrm\{X\}I\\mathrm\{I\}Z\\mathrm\{Z\}Y\\mathrm\{Y\}rotate one rowby whole qubitsrow rotation added to the existing moves

Figure 2:Program changes in Algorithm[1](https://arxiv.org/html/2610.41183#alg1)\(schematic\)\.### 4\.1Distance improvements

For listed cells, the tables give the July 2026 distance interval within the previous code parameters and our verified distance in Oursdd\(2026\)\. Bold entries attain the applicable archived, EA\-Plotkin or certified upper bound \(Section[4\.3](https://arxiv.org/html/2610.41183#S4.SS3)\)\. References identify previous lower\-bound constructions and their dates\. Forq=4,5q=4,5, where no comparable dated entry is archived, full constructed parameters appear in a separate*New constructions*block\. No historical interval is assigned where no comparison entry exists\.

Table 1:Qubit EAQECCs \(q=2q=2\)\.†\\daggerConstructed by the evolved program at unseen code lengths\.

Table 2:Qudit EAQECCs \(q=3,4,5q=3,4,5\)\.PreviousOursddReferences\[\[n,k,dℓ​–​du;c\]\]q\[\[n,k,d\_\{\\ell\}\\text\{\-\-\}d\_\{u\};c\]\]\_\{q\}\(2026\)\[\[9,1,7​–​8;4\]\]3\[\[9,1,7\\text\{\-\-\}8;4\]\]\_\{3\}𝟖\\mathbf\{8\}[Luo et al\. \(2022\)](https://arxiv.org/html/2610.41183#bib.bib13)\[\[10,1,8​–​9;5\]\]3\[\[10,1,8\\text\{\-\-\}9;5\]\]\_\{3\}𝟗\\mathbf\{9\}[Luo et al\. \(2022\)](https://arxiv.org/html/2610.41183#bib.bib13)\[\[11,1,9​–​10;7\]\]3\[\[11,1,9\\text\{\-\-\}10;7\]\]\_\{3\}𝟏𝟎\\mathbf\{10\}[Luo et al\. \(2022\)](https://arxiv.org/html/2610.41183#bib.bib13)\[\[13,1,10​–​12;8\]\]3\[\[13,1,10\\text\{\-\-\}12;8\]\]\_\{3\}𝟏𝟐\\mathbf\{12\}[Luo et al\. \(2022\)](https://arxiv.org/html/2610.41183#bib.bib13)*New construction*OursddReferences\[\[10,1,9;4\]\]4\[\[10,1,9;4\]\]\_\{4\}99Ours\[\[12,1,11;6\]\]4\[\[12,1,11;6\]\]\_\{4\}1111Ours\[\[14,1,13;8\]\]4\[\[14,1,13;8\]\]\_\{4\}1313Ours\[\[12,1,11;5\]\]5\[\[12,1,11;5\]\]\_\{5\}1111Ours\[\[14,1,13;7\]\]5\[\[14,1,13;7\]\]\_\{5\}1313Ours

The five Table[2](https://arxiv.org/html/2610.41183#S4.T2)rows withk=1k=1andc=n−3c=n\-3are covered by Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1); the other four retained generator matrices were constructed by normal\-form SAT\. The daggeredn=13,15n=13,15rows also have constructions from the evolved program at lengths withheld from training and selection \(Section[5\.2](https://arxiv.org/html/2610.41183#S5.SS2)\)\. These reconstructions are covered by the family theorem and are not counted again among its 54 gap closures\.

Our codes and the upper bounds close all nine listed qubit gaps in Table[2](https://arxiv.org/html/2610.41183#S4.T2)\. Four cells improve the previous lower bound by two:\(n,k,c\)=\(10,1,6\)\(n,k,c\)=\(10,1,6\),\(12,1,8\)\(12,1,8\),\(12,2,9\)\(12,2,9\)and\(13,1,8\)\(13,1,8\)\. For the last two cells, the EA\-Plotkin bound and a checked DRAT refutation, respectively, give final distance intervals\[9,9\]\[9,9\]and\[11,11\]\[11,11\]\(Section[4\.3](https://arxiv.org/html/2610.41183#S4.SS3)\)\. Table[2](https://arxiv.org/html/2610.41183#S4.T2)shows four qutrit gap closures, including\[\[13,1,12;8\]\]3\[\[13,1,12;8\]\]\_\{3\}, which raises the listed distance from 10 to 12 at fixed length and entanglement\.

The previous\[\[7,1,5;4\]\]2\[\[7,1,5;4\]\]\_\{2\}construction follows from the pure\[\[11,1,5\]\]2\[\[11,1,5\]\]\_\{2\}code of[Calderbank et al\. \(1997\)](https://arxiv.org/html/2610.41183#bib.bib3)and the length\-reduction rule of[Grassl et al\. \(2020\)](https://arxiv.org/html/2610.41183#bib.bib8); we date this EAQECC construction by the 2020 rule\. The other eight qubit baselines and the four displayed qutrit baselines follow from the 2022 version of[Luo et al\. \(2022\)](https://arxiv.org/html/2610.41183#bib.bib13)\. Appendix[A\.4](https://arxiv.org/html/2610.41183#A1.SS4)records the source codes and propagation rules for each cell\.

The 65 core qubit code records cover 61 distinct\(n,k,c\)\(n,k,c\)cells: eight listed and 53 absent cells\. The 27 qutrit codes comprise 15 improvements to listed entries, 11 constructions at absent cells and one code whose distance is already listed\. Multiple codes at one cell are not counted as separate table entries\. Four of these listed core cells overlap the family results in Section[4\.2](https://arxiv.org/html/2610.41183#S4.SS2)\. The additionaln=15n=15code record is kept in the controlled\-study archive, separately from these core\-file counts\.

### 4\.2Code families and reduced entanglement

Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)is the mathematical generalization of the construction identified through the evolved qubit codes\. It gives\[\[n,1,n−1;n−q−1\]\]q\[\[n,1,n\-1;n\-q\-1\]\]\_\{q\}forq≥3q\\geq 3,n≥2​q\+1n\\geq 2q\+1, and forq=2q=2at oddn≥5n\\geq 5\. The proof in Appendix[A\.2](https://arxiv.org/html/2610.41183#A1.SS2)establishes the entire family; the implementations verify finite instances atq=2,3,4,5q=2,3,4,5\. Entanglement lifting increasesccby one at fixed\(n,k\)\(n,k\)without reducing distance whenc<n−kc<n\-k\(Lemma[1](https://arxiv.org/html/2610.41183#Thmlemma1)\)\. The qubit family closes 29 listed gaps\. Forq=3q=3, lifting fromc=n−4c=n\-4to the table’sc=n−3c=n\-3closes 25 more, for 54 in total\. This family addresses finite\-length distance–entanglement tradeoffs: at fixedqq, its ratek/n=1/nk/n=1/nvanishes andc/nc/ntends to one\. The broader archive includes 29 binary codes withk\>1k\>1, up tok=6k=6\.

Additional constructions attaind=n−1d=n\-1atc=n−q−2c=n\-q\-2\. The displayedq=4,5q=4,5examples include\[\[10,1,9;4\]\]4\[\[10,1,9;4\]\]\_\{4\}and\[\[12,1,11;5\]\]5\[\[12,1,11;5\]\]\_\{5\}, requiring four and five shared pairs, respectively\. These constructions establish achievable entanglement costs; smaller costs atq=4,5q=4,5have not been excluded\. Complementary finite\-field annealing searches produce 13 archived codes atq=4q=4and 10 atq=5q=5\(Appendix[B\.1](https://arxiv.org/html/2610.41183#A2.SS1)\)\. Table[2](https://arxiv.org/html/2610.41183#S4.T2)selects those using the least entanglement reached at the displayed lengths\.

5510101616nn005510101515ccq=2q=25510101616nn005510101515ccq=3q=35510101616nn005510101515ccq=4q=45510101616nn005510101515ccq=5q=5

Code exists:c=n−q−1c=n\-q\-1Code exists:c<n−q−1c<n\-q\-1Code exists:c\>n−q−1c\>n\-q\-1Nonexistence certified, including implications at smallerccNo code found; nonexistence unprovedReferencec=n−3c=n\-3; not a general boundUnmarked gray cell: no result asserted in this figure\.

Figure 3:Linear stabilizer EAQECCs atk=1k=1, target distancen−1n\-1\.Figure[3](https://arxiv.org/html/2610.41183#S4.F3)concerns linear stabilizer EAQECCs withk=1k=1and target distancen−1n\-1\. Teal at\(q,n,c\)\(q,n,c\)denotes a construction with distance at leastn−1n\-1\. The white tick, solid fill and pale fill distinguishc=n−q−1c=n\-q\-1, smallerccand largercc, respectively; these are positions relative to the family line, not claims of minimum entanglement\. Pale cells correspond to explicit constructions or entanglement lifting\. Red cells are excluded by released, checked certificates or by their implications at smallerccthrough entanglement lifting\. A dotted outline records an unsuccessful search, not nonexistence\. Unmarked gray cells assert neither construction nor exclusion\. The dashedc=n−3c=n\-3line is obtained by substitutingk=1k=1andd=n−1d=n\-1into the historical Brun–Devetak–Hsieh expression2​\(d−1\)≤n−k\+c2\(d\-1\)\\leq n\-k\+cat equality\. It is a comparison line, not a general bound in this regime \(Appendix[A\.3](https://arxiv.org/html/2610.41183#A1.SS3)\)\.

### 4\.3Upper bounds and optimality

Solver refinement settles the two remaining qubit gaps from Table[2](https://arxiv.org/html/2610.41183#S4.T2)\. Normal\-form SAT finds\[\[12,2,9;9\]\]2\[\[12,2,9;9\]\]\_\{2\}, improving upon an intermediated=8d=8construction from our earlier search\. EA\-Plotkin givesd≤⌊144/15⌋=9d\\leq\\lfloor 144/15\\rfloor=9, so the new code is distance\-optimal\. At\(n,k,c\)=\(13,1,8\)\(n,k,c\)=\(13,1,8\), a DRAT\-certified refutation excludesd≥12d\\geq 12; our existingd=11d=11code is therefore optimal\. Both codes are checked by separate binary linear\-algebra code, and DRAT\-trim replays the nonexistence certificate\. We attribute these two closures to solver refinement\.

Matching nonexistence results also establish minimum entanglement at selected lengths\. For qubits atk=1k=1,d=n−1d=n\-1, the minimum isn−3n\-3atn=7,9,11n=7,9,11andn−4n\-4atn=6,8,10n=6,8,10\. This finite\-length parity pattern combines distinct constructions with certified exclusions; Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)’s binary branch covers odd lengths\. For qutrits, the certified exclusion of\[\[10,1,9;4\]\]3\[\[10,1,9;4\]\]\_\{3\}and a code atc=5c=5givecmins​\(10,1,9\)=5c^\{\\mathrm\{s\}\}\_\{\\min\}\(10,1,9\)=5\. Two further exclusions,\[\[5,2,4;3\]\]2\[\[5,2,4;3\]\]\_\{2\}and\[\[6,2,5;4\]\]2\[\[6,2,5;4\]\]\_\{2\}, were also checked by exhaustive enumeration\. All ten exclusions have checked DRAT proofs \(Appendix[B\.2](https://arxiv.org/html/2610.41183#A2.SS2)\)\.

Applying the EA\-Plotkin bound of[Guo & Li \(2013\)](https://arxiv.org/html/2610.41183#bib.bib10)additionally lowers 398 listed qubit upper bounds\. The auditor recomputes these corrections against the reference table data\. These corrections follow from a known inequality and are reported as a separate source of upper bounds\.

## 5Ablation Study

We test whether iterative feedback helps develop a researcher\-proposed change into an effective search program\. Both policies receive the same initial code and research guidance; their difference is how they reuse previous programs and execution feedback\.

### 5\.1Program generation

The shared proposal is to maintain and mutate a basis ofL=S⟂L=S^\{\\perp\}, converting it toSSfor exact evaluation\. For\[\[9,1,8;6\]\]2\[\[9,1,8;6\]\]\_\{2\}and\[\[11,1,10;8\]\]2\[\[11,1,10;8\]\]\_\{2\}, this replaces a basis of 14 or 18 generators with four vectors\. Symplectic complementation preserves the feasible code set but changes the variables and local mutations\. A preliminary calibration compares the initialSS\-side program with a workingLL\-side control and fixes a budget at which the change can produce measurable success\. Neither the control’s source nor generator matrices are supplied to the model\.

*Independent proposals*always receive the initial program and its fixed training measurements\.*Iterative evolution*receives the best\-so\-far program and the most recent attempt, including rejected attempts, with training feedback for both\. The model can revise the representation, objective, mutation operators and restart policy\. A proposal is a whole program revision; an evaluator call checks one candidate matrix produced by that program\. Both use Gemini 3\.5 Flash and identical tool access\. There is no controller initialization: every success must be produced by the submitted program\.

An initial four\-block study was followed by a prospective eight\-block replication using new generation and execution seeds\. Each policy is allocated seven proposals per block\. The replication receives 111 of 112 planned responses; one iterative pool has six proposals\. All eight blocks are retained under a rule fixed before validation and testing\. Training uses two seeds and 10,000 exact evaluations per target\. Four new validation seeds select among the three training\-best distinct programs; 32 further seeds evaluate each selection\. Only training feedback enters generation\. The original and new cohorts are reported separately \(Appendix[C](https://arxiv.org/html/2610.41183#A3)\)\.

\(a\) Program generationn=9,11n=9,110255075100Success rate \(%\)Exact evaluations05k10k43\.6%58\.0%\(b\) Generalization to longer codesn=13,15n=13,150255075100Success rate \(%\)Exact evaluations015k30k11\.3%38\.9%Initial programClassical L\-side controlIndependent proposalsIterative evolution

Figure 4:Prospective replication under shared research guidance\.In the new cohort, success atn=9,11n=9,11is 72\.7% and 43\.4% for iterative evolution, versus 60\.2% and 27\.0% for independent proposals\. The prespecified primary endpoint is the paired block difference in mean normalized success\-curve area: 0\.359 versus 0\.260, a gain of 0\.099\. Five of eight block differences are positive; a descriptive two\-sided sign\-flip test givesp=0\.328p=0\.328\. Generation blocks, rather than execution seeds, are the units for policy inference\. Restricting to the seven fully received paired blocks gives a gain of 0\.150\.

Figure[4](https://arxiv.org/html/2610.41183#S5.F4)aggregates both lengths within each panel\. Each policy contributes eight selected programs and 32 runs per length; each fixed control contributes 32 runs per length\. Across the two generation lengths, iterative selections solve 297/512 executions, versus 223/512 for independent selections\. Every saved successful code passes an independent parameter check\. Appendix[C\.3](https://arxiv.org/html/2610.41183#A3.SS3)reports the earlier cohort and its fresh\-seed repeat separately; the artifact also preserves model\-use accounting for both policies\.

### 5\.2Generalization to longer codes

The selected programs are applied without further modification to\[\[13,1,12;10\]\]2\[\[13,1,12;10\]\]\_\{2\}and\[\[15,1,14;12\]\]2\[\[15,1,14;12\]\]\_\{2\}at 30,000 calls\. These lengths are withheld from generation and selection; their outcomes are secondary endpoints\. In the new eight\-block cohort, iterative success is 118/256 \(46\.1%\) and 81/256 \(31\.6%\), versus 50/256 \(19\.5%\) and 8/256 \(3\.1%\) for independent proposals\. Two iterative selections achieve 32/32 atn=13n=13and at least 28/32 atn=15n=15\(Appendix[C\.4](https://arxiv.org/html/2610.41183#A3.SS4)\)\. Their mean normalized curve areas are 0\.309 and 0\.193, compared with 0\.099 and 0\.012 for independent proposals\.

A preserved lineage from the original cohort gives a source\-level diagnosis of one useful edit\. Adding a penalty for distance below the target—the only functional search change in that step—raisesn=13n=13success from 13/32 to 29/32 andn=15n=15success from 3/32 to 28/32\. The validation\-selected child \(Algorithm[2](https://arxiv.org/html/2610.41183#alg2)\) then bundles changes to objective weights, moves and restart behavior; we therefore use the earlier step for edit\-level attribution and report the complete lineage in Appendix[C\.5](https://arxiv.org/html/2610.41183#A3.SS5)\. All resulting codes pass independent linear\-algebra checks\. Table[2](https://arxiv.org/html/2610.41183#S4.T2)includes the longer\-code parameters alongside their prior intervals\.

## 6Limitations and conclusion

The controlled evidence is scoped to one model, one researcher proposal and binary targets\. The eight generation blocks are the independent units for policy inference; repeated executions measure frozen\-program variability\. The policies receive equal proposal allocations but use different token totals\. Exact distance verification enumerates symplectic duals, so its cost grows exponentially with their dimension\. The distance guarantees assume ideal decoding and noiseless receiver\-side halves; circuit costs and hardware\-level error rates are not evaluated\. For these controlled studies, the artifact preserves all generated sources, requests and selection records and supports fixed\-program replay; stochastic model sampling is documented rather than expected to return byte\-identical programs\.

The central mathematical result developed from code constructions produced by evolved programs\. Researchers analyzed their structure, derived a qubit family, and extended and proved the prime\-power construction of Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)\. Later prompts reused the qubit family, showing how a result obtained through program search can guide further research\. The family and entanglement lifting close 54 listed gaps\. Normal\-form SAT completes two final qubit closures, ten checked DRAT refutations certify selected upper bounds and minimum entanglement costs, and EA\-Plotkin tightens 398 listed upper bounds\.

Supplied matrices, family implementations and independent verifiers support reconstruction and checks of finite instances; preserved programs support seeded replay\. The proof covers every admissible parameter\. Independent Magma verification reports zero mismatches across 148 objects, and Lean checks the algebraic certificate underlying the researcher\-derived theorem\. The prospective eight\-block cohort identifies useful program revisions and higher held\-out longer\-code success among iterative selections under shared research guidance\. Applying the workflow to another problem still requires its own representation, evaluator and mathematical analysis\.

### AI use statement

We used Gemini models through AlphaEvolve and a local controller to propose and revise search programs under researcher guidance and exact evaluation feedback \(Sections[3](https://arxiv.org/html/2610.41183#S3)and[5](https://arxiv.org/html/2610.41183#S5)\)\. LLM\-based assistants, including Codex, supported implementation, mathematical reasoning and manuscript preparation\. Generated codes were independently checked; Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)’s algebraic construction was verified in Lean\. The authors reviewed AI\-assisted outputs and take responsibility for the paper’s claims, proofs, code and reported results\.

### Ethics statement

This work studies algebraic code constructions and search programs; it does not involve experiments on human participants or use participant\-level or personal datasets\. Its potential benefit is to improve methods for quantum error correction and communication, while the reported idealized parameters do not establish hardware\-level reliability or operational security\. Research\-integrity considerations are addressed through dated sources, explicit provenance, independent verification, and separation of new parameter claims from retrospective reconstruction\. Unsuccessful searches are distinguished from proved nonexistence\. The controlled\-study records preserve failed and excluded attempts, unavailable responses and protocol amendments, and the released records omit account credentials and machine\-local configuration\. Researcher and AI contributions are disclosed, external sources are cited, and the artifact retains software licensing information\. Compute allowances and model usage are documented in Appendices[B\.1](https://arxiv.org/html/2610.41183#A2.SS1)and[C](https://arxiv.org/html/2610.41183#A3)\.

### Reproducibility statement

The artifact supports reconstruction and independent checking of the mathematical outputs: generator matrices specify the finite codes, implementations generate family instances, and Appendix[A\.2](https://arxiv.org/html/2610.41183#A1.SS2)provides the general construction and proof of Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)\. The initial and later task specifications in Appendix[B\.3](https://arxiv.org/html/2610.41183#A2.SS3)document the transition from initial search directions to reuse of the researcher\-derived qubit family\. Preserved programs can be replayed with fixed seeds and evaluation budgets as described in Section[3\.4](https://arxiv.org/html/2610.41183#S3.SS4)and the[artifact](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)\. Appendix[C](https://arxiv.org/html/2610.41183#A3)and the accompanying study records supply generation requests, selections and held\-out outcomes for the separate controlled comparison\. Computational checks verify finite cases; general validity rests on the proof\. Appendix[D](https://arxiv.org/html/2610.41183#A4)gives the exact formal goal and proof structure for Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)\. The artifact includes the Lean sources, pinned dependencies and separate kernel and Comparator verification records\. Fresh LLM sampling is not part of this replay\. External solver and Magma checks are reported separately from completed Python checks\. The artifact is released under the MIT license and is available at[https://github\.com/LeGenAI/llm\_guided\_EAQECC\_search/tree/arxiv\-v1](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)\.

### Acknowledgments

We thank the maintainers of the tables of best\-known codes\([Grassl, 2026](https://arxiv.org/html/2610.41183#bib.bib7)\)\. J\.\-L\. Kim was supported in part by the BK21 FOUR \(Fostering Outstanding Universities for Research\) funded by the Ministry of Education \(MOE, Korea\), National Research Foundation of Korea \(NRF\) under Grant No\. 4120240415042, Basic Science Research Program through the National Research Foundation of Korea \(NRF\) funded by the Ministry of Science and ICT under Grant No\. RS\-2025\-24534992 and Global \- Learning & Academic research institution for Master’s⋅\\cdotPhD students, and Postdocs \(LAMP\) Program of the National Research Foundation of Korea \(NRF\) grant funded by the Ministry of Education \(No\. RS\-2024\-00441954\)\.

## References

- Assumpção et al\. \(2026\)Henrique Assumpção, Diego Ferreira, Leandro Campos, and Fabricio Murai\.CodeEvolve: an open source evolutionary coding agent for algorithmic discovery and optimization\.*arXiv preprint arXiv:2510\.14150*, 2026\.
- Brun et al\. \(2006\)Todd Brun, Igor Devetak, and Min\-Hsiu Hsieh\.Correcting quantum errors with entanglement\.*Science*, 314\(5798\):436–439, 2006\.doi:10\.1126/science\.1131563\.
- Calderbank et al\. \(1997\)A\. R\. Calderbank, E\. M\. Rains, P\. W\. Shor, and N\. J\. A\. Sloane\.Quantum error correction via codes over GF\(4\)\.arXiv:quant\-ph/9608006v5, 1997\.URL[https://arxiv\.org/abs/quant\-ph/9608006v5](https://arxiv.org/abs/quant-ph/9608006v5)\.Version dated 10 September 1997\.
- Cruz\-Benito et al\. \(2026\)Juan Cruz\-Benito, Andrew W\. Cross, David Kremer, and Ismael Faro\.Evolutionary discovery of bivariate bicycle codes with LLM\-guided search\.arXiv:2606\.02418, 2026\.URL[https://arxiv\.org/abs/2606\.02418](https://arxiv.org/abs/2606.02418)\.
- Georgiev et al\. \(2025\)Bogdan Georgiev, Javier Gómez\-Serrano, Terence Tao, and Adam Zsolt Wagner\.Mathematical exploration and discovery at scale\.*arXiv preprint arXiv:2511\.02864*, 2025\.
- Grassl \(2021\)Markus Grassl\.Entanglement\-assisted quantum communication beating the quantum Singleton bound\.*Physical Review A*, 103:L020601, 2021\.doi:10\.1103/PhysRevA\.103\.L020601\.
- Grassl \(2026\)Markus Grassl\.Bounds on the parameters of various types of codes\.\([http://www\.codetables\.de](http://www.codetables.de/)\), 2026\.Accessed on 17 July 2026; table data preserved in the accompanying artifact\.
- Grassl et al\. \(2020\)Markus Grassl, Felix Huber, and Andreas Winter\.Entropic proofs of Singleton bounds for quantum error\-correcting codes\.arXiv:2010\.07902v1, 2020\.URL[https://arxiv\.org/abs/2010\.07902v1](https://arxiv.org/abs/2010.07902v1)\.First public version, 15 October 2020; Theorem 7\.
- Grassl et al\. \(2022\)Markus Grassl, Felix Huber, and Andreas Winter\.Entropic proofs of Singleton bounds for quantum error\-correcting codes\.*IEEE Transactions on Information Theory*, 68\(6\):3942–3950, 2022\.doi:10\.1109/TIT\.2022\.3149291\.
- Guo & Li \(2013\)Luobin Guo and Ruihu Li\.Linear Plotkin bound for entanglement\-assisted quantum codes\.*Physical Review A*, 87:032309, 2013\.doi:10\.1103/PhysRevA\.87\.032309\.
- Lange et al\. \(2025\)Robert Tjarko Lange, Yuki Imajuku, and Edoardo Cetin\.ShinkaEvolve: Towards open\-ended and sample\-efficient program evolution\.*arXiv preprint arXiv:2509\.19349*, 2025\.
- Lean Project \(2026\)Lean Project\.Comparator\.[https://github\.com/leanprover/comparator](https://github.com/leanprover/comparator), 2026\.Revision a4f696825c583ed8a5b4060d9a0faa5b882d365b\.
- Luo et al\. \(2022\)Gaojun Luo, Martianus Frederic Ezerman, Markus Grassl, and San Ling\.How much entanglement does a quantum code need?*arXiv preprint arXiv:2207\.05647*, 2022\.URL[https://arxiv\.org/abs/2207\.05647v1](https://arxiv.org/abs/2207.05647v1)\.First public version, 12 July 2022; Table I and Section IV\.
- Mauron et al\. \(2023\)Caroline Mauron, Terry Farrelly, and Thomas M\. Stace\.Optimization of tensor network codes with reinforcement learning\.*arXiv preprint arXiv:2305\.11470*, 2023\.
- Novikov et al\. \(2025\)Alexander Novikov, Ngân Vũ, Marvin Eisenberger, Emilien Dupont, Po\-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J\. R\. Ruiz, Abbas Mehrabian, M\. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Balog\.AlphaEvolve: A coding agent for scientific and algorithmic discovery\.*arXiv preprint arXiv:2506\.13131*, 2025\.
- Olle et al\. \(2024\)Jan Olle, Remmy Zen, Matteo Puviani, and Florian Marquardt\.Simultaneous discovery of quantum error correction codes and encoders with a noise\-aware reinforcement learning agent\.*npj Quantum Information*, 10:126, 2024\.
- Poulsen Nautrup et al\. \(2019\)Hendrik Poulsen Nautrup, Nicolas Delfosse, Vedran Dunjko, Hans J\. Briegel, and Nicolai Friis\.Optimizing quantum error correction codes with reinforcement learning\.*Quantum*, 3:215, 2019\.doi:10\.22331/q\-2019\-12\-16\-215\.
- Romera\-Paredes et al\. \(2024\)Bernardino Romera\-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M\. Pawan Kumar, Emilien Dupont, Francisco J\. R\. Ruiz, Jordan S\. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi\.Mathematical discoveries from program search with large language models\.*Nature*, 625:468–475, 2024\.doi:10\.1038/s41586\-023\-06924\-6\.
- Sharma \(2025\)Asankhaya Sharma\.OpenEvolve: an open\-source evolutionary coding agent\.[https://github\.com/algorithmicsuperintelligence/openevolve](https://github.com/algorithmicsuperintelligence/openevolve), 2025\.
- Shin et al\. \(2011\)Jeonghwan Shin, Jun Heo, and Todd A\. Brun\.Entanglement\-assisted codeword stabilized quantum codes\.*Physical Review A*, 84:062321, 2011\.doi:10\.1103/PhysRevA\.84\.062321\.
- Su et al\. \(2025\)Vincent Paul Su, ChunJun Cao, Hong\-Ye Hu, Yariv Yanay, Charles Tahan, and Brian Swingle\.Discovery of optimal quantum error correcting codes via reinforcement learning\.*Physical Review Applied*, 23:034048, 2025\.doi:10\.1103/PhysRevApplied\.23\.034048\.
- Webster & Browne \(2024\)Mark Webster and Dan Browne\.Engineering quantum error correction codes using evolutionary algorithms\.*arXiv preprint arXiv:2409\.13017*, 2024\.URL[https://arxiv\.org/abs/2409\.13017](https://arxiv.org/abs/2409.13017)\.
- Wetzler et al\. \(2014\)Nathan Wetzler, Marijn J\. H\. Heule, and Warren A\. Hunt\.DRAT\-trim: Efficient checking and trimming using expressive clausal proofs\.In*Theory and Applications of Satisfiability Testing \(SAT\)*, volume 8561 of*LNCS*, pp\. 422–429, 2014\.
- Wilde & Brun \(2008\)Mark M\. Wilde and Todd A\. Brun\.Optimal entanglement formulas for entanglement\-assisted quantum coding\.*Physical Review A*, 77:064302, 2008\.doi:10\.1103/PhysRevA\.77\.064302\.
- Yang et al\. \(2026\)Yang Yang, Zining Zhong, Jindong Li, Jiemin Wu, Kaishen Yuan, Wenshuo Chen, Menglin Yang, and Yutao Yue\.TurboEvolve: Towards fast and robust LLM\-driven program evolution\.*arXiv preprint arXiv:2604\.18607*, 2026\.

## Appendix AThe domain, the tables, and the targets

### A\.1Codes as subspaces of𝔽q2​n\\mathbb\{F\}\_\{q\}^\{2n\}

For prime\-powerqq, our search uses𝔽q\\mathbb\{F\}\_\{q\}\-linear stabilizer EAQECCs\. Stabilizer generators are products of Pauli operators defining error\-detection constraints\. Entanglement assistance permits noncommuting generators on the transmitted qudits by completing them with operators on the receiver’s halves into commuting constraints\. Their commutation relations determine the entanglement cost\([Brun et al\., 2006](https://arxiv.org/html/2610.41183#bib.bib2);[Wilde & Brun, 2008](https://arxiv.org/html/2610.41183#bib.bib24)\)\. Nonadditive EAQECCs form a different search space\([Shin et al\., 2011](https://arxiv.org/html/2610.41183#bib.bib20)\)\.

We write vectors in bold, scalar coordinates and coefficients in italic, and subspaces with italic capitals such asS,L,RS,L,R\. Modulo phase, a Pauli operator is represented by𝒖=\(x1,z1,…,xn,zn\)∈𝔽q2​n\\boldsymbol\{u\}=\(x\_\{1\},z\_\{1\},\\ldots,x\_\{n\},z\_\{n\}\)\\in\\mathbb\{F\}\_\{q\}^\{2n\}\. For qubits, the pairs\(0,0\)\(0,0\),\(1,0\)\(1,0\),\(0,1\)\(0,1\)and\(1,1\)\(1,1\)representI,X,Z,YI,X,Z,Y, respectively\. The symplectic product with𝒗=\(x1′,z1′,…,xn′,zn′\)\\boldsymbol\{v\}=\(x^\{\\prime\}\_\{1\},z^\{\\prime\}\_\{1\},\\ldots,x^\{\\prime\}\_\{n\},z^\{\\prime\}\_\{n\}\)is

⟨𝒖,𝒗⟩=∑i\(xi​zi′−zi​xi′\),\\langle\\boldsymbol\{u\},\\boldsymbol\{v\}\\rangle=\\sum\_\{i\}\(x\_\{i\}z\_\{i\}^\{\\prime\}\-z\_\{i\}x\_\{i\}^\{\\prime\}\),and the symplectic weightwts⁡\(𝒖\)\\operatorname\{wt\_\{s\}\}\(\\boldsymbol\{u\}\)counts positions with\(xi,zi\)≠\(0,0\)\(x\_\{i\},z\_\{i\}\)\\neq\(0,0\)\. For qubits, zero symplectic product means that the Pauli operators commute\.

LetSSbe the generator span and sets=dimSs=\\dim S\. Its symplectic dualS⟂S^\{\\perp\}consists of vectors orthogonal toSS\. For any subspaceU≤𝔽q2​nU\\leq\\mathbb\{F\}\_\{q\}^\{2n\}, define its radical byrad⁡\(U\):=U∩U⟂\\operatorname\{rad\}\(U\):=U\\cap U^\{\\perp\}\. ThusSiso=rad⁡\(S\)S\_\{\\mathrm\{iso\}\}=\\operatorname\{rad\}\(S\)contains stabilizer operations with trivial logical action\. Vectors inS⟂∖SisoS^\{\\perp\}\\setminus S\_\{\\mathrm\{iso\}\}represent undetectable errors with nontrivial logical action\. The code parameters are

c=s−dimSiso2,k=n−s\+c,d=min⁡\{wts⁡\(𝒗\):𝒗∈S⟂∖Siso\}\.c=\\frac\{s\-\\dim S\_\{\\mathrm\{iso\}\}\}\{2\},\\qquad k=n\-s\+c,\\qquad d=\\min\\\{\\operatorname\{wt\_\{s\}\}\(\\boldsymbol\{v\}\):\\boldsymbol\{v\}\\in S^\{\\perp\}\\setminus S\_\{\\mathrm\{iso\}\}\\\}\.Finite\-field linear algebra gives the dual and radical\. Withr=dimL=n\+k−cr=\\dim L=n\+k\-c, the dual hasqrq^\{r\}vectors, of whichqr−qn−k−cq^\{r\}\-q^\{n\-k\-c\}are non\-radical; their minimum weight givesdd\. For Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1),r=q\+2r=q\+2is independent of length at fixedqq\. At every binary ablation length,r=4r=4: 16 dual vectors and 12 non\-radical vectors\. The controlled evaluator computes the radical from the Gram kernel, avoiding enumeration ofSS\. The archived discovery helper instead enumerates bothSSandLL, totaling2s\+2r2^\{s\}\+2^\{r\}vectors before filtering\. Thus implementation and subspace dimensions determine cost, independently of the search representation\. Parameters are recomputed from generators, not search\-program reports\.

To propagate constructions and exclusions across entanglement costs, we use the following form of the standard rule in[Luo et al\. \(2022, Section IV, rule \(4\)\)](https://arxiv.org/html/2610.41183#bib.bib13)\. We include its symplectic argument for completeness\.

###### Lemma 1\.

An𝔽q\\mathbb\{F\}\_\{q\}\-linear stabilizer EAQECC with parameters\[\[n,k,d;c\]\]q\[\[n,k,d;c\]\]\_\{q\},k≥1k\\geq 1andc<n−kc<n\-k, gives an𝔽q\\mathbb\{F\}\_\{q\}\-linear stabilizer EAQECC with parameters\[\[n,k,d′;c\+1\]\]q\[\[n,k,d^\{\\prime\};c\+1\]\]\_\{q\}andd′≥dd^\{\\prime\}\\geq d\.

###### Sketch of proof\.

SetL=S⟂L=S^\{\\perp\}andR=rad⁡\(L\)R=\\operatorname\{rad\}\(L\), withdimR=j=n−k−c\>0\\dim R=j=n\-k\-c\>0\. ChooseL=U⊕RL=U\\oplus R\. The form onUUis nondegenerate, since a vector ofUUorthogonal toUUalso lies inRR, hence inU∩R=\{0\}U\\cap R=\\\{0\\\}; hencedimU=2​k\\dim U=2k\. For a codimension\-one subspaceR′≤RR^\{\\prime\}\\leq R, putL′=U⊕R′L^\{\\prime\}=U\\oplus R^\{\\prime\}andS′=\(L′\)⟂S^\{\\prime\}=\(L^\{\\prime\}\)^\{\\perp\}\. Thenrad⁡\(L′\)=R′\\operatorname\{rad\}\(L^\{\\prime\}\)=R^\{\\prime\}and

L′∖R′⊆L∖R,dimS′=s\+1,dimR′=j−1\.L^\{\\prime\}\\setminus R^\{\\prime\}\\subseteq L\\setminus R,\\qquad\\dim S^\{\\prime\}=s\+1,\\qquad\\dim R^\{\\prime\}=j\-1\.The inclusion givesd′≥dd^\{\\prime\}\\geq d, while the parameter formulas givec′=\(\(s\+1\)−\(j−1\)\)/2=c\+1c^\{\\prime\}=\(\(s\+1\)\-\(j\-1\)\)/2=c\+1andk′=n−\(s\+1\)\+c′=kk^\{\\prime\}=n\-\(s\+1\)\+c^\{\\prime\}=k\. The ambient space is unchanged, so the length remainsnn\. ∎

Repeating the operation gives distance at leastddfor everyc′∈\{c,…,n−k\}c^\{\\prime\}\\in\\\{c,\\ldots,n\-k\\\}\. Conversely, nonexistence at costccand distance at leastddexcludes every smaller cost at the same\(n,k\)\(n,k\): any such code could be lifted to costcc\. This justifies the upward construction propagation and downward exclusion propagation in Figure[3](https://arxiv.org/html/2610.41183#S4.F3)\. For the qutrit family, one step reduces the radical dimension from three to two and raisesc=n−4c=n\-4ton−3n\-3\. The 25 open reference cells haven=12,…,36n=12,\\ldots,36, all within Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)’s range; their listed upper boundn−1n\-1makes each lifted lower bound exact\.

### A\.2The closed form, and why it works

Early evolved constructions\[\[9,1,8;6\]\]2\[\[9,1,8;6\]\]\_\{2\}and\[\[11,1,10;8\]\]2\[\[11,1,10;8\]\]\_\{2\}\(Appendix[B\.1](https://arxiv.org/html/2610.41183#A2.SS1)\) motivated the odd\-length qubit family recorded in later tasks\. The construction below generalizes it to prime powers\. Its algebraic properties have also been independently rechecked with the Lean kernel; Appendix[D](https://arxiv.org/html/2610.41183#A4)gives the formal goal, proof and correspondence with this construction\.

Fix a prime powerq=peq=p^\{e\}, a lengthn≥2​q\+1n\\geq 2q\+1, and an enumerationu1,…,uqu\_\{1\},\\dots,u\_\{q\}of𝔽q\\mathbb\{F\}\_\{q\}\. On qudits1,…,2​q1,\\dots,2qtakeqqdisjoint pairs and let𝝆i\\boldsymbol\{\\rho\}\_\{i\}beZZ\-type on pairiiwithzz\-values\(1,−1\)\(1,\-1\)\. Juxtaposition and powers denote concatenation of coordinate pairs;\(0,1\)0\(0,1\)^\{0\}is empty, so the tail atn=2​q\+1n=2q\+1contains only\(0,λ\)\(0,\\lambda\)\. Put

𝒂=\(1,0\)n,𝒃=\(u1,1\)\(u1,z2\)\|⋯\|\(uq,1\)\(uq,z2\)\|\(0,1\)n−2​q−1\(0,λ\),\\boldsymbol\{a\}=\(1,0\)^\{n\},\\qquad\\boldsymbol\{b\}=\(u\_\{1\},1\)\(u\_\{1\},z\_\{2\}\)\\,\\big\|\\cdots\\big\|\\,\(u\_\{q\},1\)\(u\_\{q\},z\_\{2\}\)\\,\\big\|\\,\(0,1\)^\{n\-2q\-1\}\(0,\\lambda\),withz2=1z\_\{2\}=1for oddppandz2=0z\_\{2\}=0forp=2p=2, andL=span⁡\{𝒂,𝒃,𝝆1,…,𝝆q\}L=\\operatorname\{span\}\\\{\\boldsymbol\{a\},\\boldsymbol\{b\},\\boldsymbol\{\\rho\}\_\{1\},\\dots,\\boldsymbol\{\\rho\}\_\{q\}\\\}\.

###### Theorem 1\.

Letqqbe a prime power\. Forq≥3q\\geq 3withn≥2​q\+1n\\geq 2q\+1, orq=2q=2with oddn≥5n\\geq 5, one can chooseλ∈𝔽q×\\lambda\\in\\mathbb\{F\}\_\{q\}^\{\\times\}so thatLLis the normalizer side of an\[\[n,1,n−1;n−q−1\]\]q\[\[n,1,n\-1;n\-q\-1\]\]\_\{q\}EAQECC\. Forq≥3q\\geq 3, its entanglement costccisq−2q\-2shared pairs below the threshold in the BDH expression; forq=2q=2, it meets that threshold\.

###### Proof\.

The two vectors𝒂,𝒃∈𝔽q2​n\\boldsymbol\{a\},\\boldsymbol\{b\}\\in\\mathbb\{F\}\_\{q\}^\{2n\}and theqqradical candidates𝝆1,…,𝝆q\\boldsymbol\{\\rho\}\_\{1\},\\ldots,\\boldsymbol\{\\rho\}\_\{q\}are defined above\. WriteR0=span⁡\{𝝆1,…,𝝆q\}R\_\{0\}=\\operatorname\{span\}\\\{\\boldsymbol\{\\rho\}\_\{1\},\\ldots,\\boldsymbol\{\\rho\}\_\{q\}\\\}\. Each𝝆i\\boldsymbol\{\\rho\}\_\{i\}has two nonzeroZZcomponents on a distinct pair of qudits, so theseqqvectors are linearly independent\. Moreover,𝒂\\boldsymbol\{a\}and𝒃\\boldsymbol\{b\}have equalXXcomponents within each pair\. Their symplectic products with𝝆i\\boldsymbol\{\\rho\}\_\{i\}therefore vanish\. The radical candidates are mutually orthogonal, since they are allZZ\-type\.

The symplectic product of the two vectors is the sum of theZZcomponents of𝒃\\boldsymbol\{b\}:

δ:=⟨𝒂,𝒃⟩=q⁡\(1\+z2\)\+\(n−2​q−1\)​1𝔽q\+λ=\(n−1\)​1𝔽q\+λ\.\\delta:=\\langle\\boldsymbol\{a\},\\boldsymbol\{b\}\\rangle=q\(1\+z\_\{2\}\)\+\(n\-2q\-1\)\\,1\_\{\\mathbb\{F\}\_\{q\}\}\+\\lambda=\(n\-1\)\\,1\_\{\\mathbb\{F\}\_\{q\}\}\+\\lambda\.Here integers are interpreted in𝔽q\\mathbb\{F\}\_\{q\}, andq​1𝔽q=0q\\,1\_\{\\mathbb\{F\}\_\{q\}\}=0because its characteristic dividesqq\. Ifq≥3q\\geq 3, at most one of theq−1≥2q\-1\\geq 2nonzero choices ofλ\\lambdamakesδ=0\\delta=0; choose any other nonzero value\. Ifq=2q=2andnnis odd, the only choiceλ=1\\lambda=1givesδ=1\\delta=1\. For even binarynn, it givesδ=0\\delta=0: this particular construction loses its nondegenerate pair\. Thusδ≠0\\delta\\neq 0in every case covered by the theorem\.

To establish independence of the full generating set, supposeα​𝒂\+β​𝒃\+∑iti​𝝆i=𝟎\\alpha\\boldsymbol\{a\}\+\\beta\\boldsymbol\{b\}\+\\sum\_\{i\}t\_\{i\}\\boldsymbol\{\\rho\}\_\{i\}=\\boldsymbol\{0\}\. Sincen≥2​q\+1n\\geq 2q\+1, the final qudit is outside the support of every𝝆i\\boldsymbol\{\\rho\}\_\{i\}\. Its two components are\(α,λ​β\)\(\\alpha,\\lambda\\beta\), soα=β=0\\alpha=\\beta=0\. Independence of the radical candidates then impliesti=0t\_\{i\}=0for everyii\. ConsequentlydimL=q\+2\\dim L=q\+2\. The restriction of the symplectic form toLL, in this basis, has one nondegenerate2×22\\times 2block\(0δ−δ0\)\\left\(\\begin\{smallmatrix\}0&\\delta\\\\ \-\\delta&0\\end\{smallmatrix\}\\right\)and aq×qq\\times qzero block\. Hence its rank is two andrad⁡\(L\)=R0\\operatorname\{rad\}\(L\)=R\_\{0\}\.

Every vector outside this radical has the unique form

𝒘=α​𝒂\+β​𝒃\+∑i=1qti​𝝆i,\(α,β\)≠\(0,0\)\.\\boldsymbol\{w\}=\\alpha\\boldsymbol\{a\}\+\\beta\\boldsymbol\{b\}\+\\sum\_\{i=1\}^\{q\}t\_\{i\}\\boldsymbol\{\\rho\}\_\{i\},\\qquad\(\\alpha,\\beta\)\\neq\(0,0\)\.Alln−2​qn\-2qtail qudits are nonzero: their components are\(α,β\)\(\\alpha,\\beta\), except for the final\(α,λ​β\)\(\\alpha,\\lambda\\beta\)\. On pairii, the two coordinate pairs are

\(α\+β​ui,β\+ti\),\(α\+β​ui,β​z2−ti\)\.\(\\alpha\+\\beta u\_\{i\},\\,\\beta\+t\_\{i\}\),\\qquad\(\\alpha\+\\beta u\_\{i\},\\,\\beta z\_\{2\}\-t\_\{i\}\)\.Ifβ=0\\beta=0, thenα≠0\\alpha\\neq 0and allnnqudits are nonzero\. Ifβ≠0\\beta\\neq 0, exactly one indexiisatisfiesui=−α/βu\_\{i\}=\-\\alpha/\\beta, sinceu1,…,uqu\_\{1\},\\ldots,u\_\{q\}enumerate allqqelements of the finite field𝔽q\\mathbb\{F\}\_\{q\}, and−α/β∈𝔽q\-\\alpha/\\beta\\in\\mathbb\{F\}\_\{q\}\. Every other pair has two nonzeroXXcomponents\. On the exceptional pair, bothZZcomponents could vanish only ifti=−β=β​z2t\_\{i\}=\-\\beta=\\beta z\_\{2\}\. This is impossible because1\+z2≠01\+z\_\{2\}\\neq 0: it equals22in odd characteristic and11in characteristic two\. At most one qudit can therefore be zero, givingwts⁡\(𝒘\)≥n−1\\operatorname\{wt\_\{s\}\}\(\\boldsymbol\{w\}\)\\geq n\-1\.

This lower bound is attained\. Fix any indexii, chooseβ=1\\beta=1,α=−ui\\alpha=\-u\_\{i\},ti=−1t\_\{i\}=\-1, andth=0t\_\{h\}=0forh≠ih\\neq i\. The first qudit of pairiiis zero and its second has nonzeroZZcomponent1\+z21\+z\_\{2\}\. All other pairs have nonzeroXXcomponents, and the tail remains nonzero\. This vector lies outsideR0R\_\{0\}and has weight exactlyn−1n\-1\.

Finally, setS=L⟂S=L^\{\\perp\}\. Nondegeneracy of the ambient symplectic form givesS⟂=LS^\{\\perp\}=LanddimS=2​n−q−2\\dim S=2n\-q\-2\. AlsoS∩S⟂=L⟂∩L=R0S\\cap S^\{\\perp\}=L^\{\\perp\}\\cap L=R\_\{0\}, whose dimension isqq\. The parameter formulas in Appendix[A\.1](https://arxiv.org/html/2610.41183#A1.SS1)now give

c=2​n−q−2−q2=n−q−1,k=n−\(2​n−q−2\)\+c=1,d=n−1\.c=\\frac\{2n\-q\-2\-q\}\{2\}=n\-q\-1,\\qquad k=n\-\(2n\-q\-2\)\+c=1,\\qquad d=n\-1\.For these parameters,2​\(d−1\)−\(n−k\+c\)=\(2​n−4\)−\(2​n−q−2\)=q−22\(d\-1\)\-\(n\-k\+c\)=\(2n\-4\)\-\(2n\-q\-2\)=q\-2\. Thus the BDH threshold exceedsccbyq−2q\-2shared pairs forq≥3q\\geq 3and met with equality forq=2q=2, as stated\. ∎

The auditor instantiates this construction and verifies every member exactly forq∈\{2,3,4,5\}q\\in\\\{2,3,4,5\\\}and2​q\+1≤n≤2​q\+82q\+1\\leq n\\leq 2q\+8\(claimfamilies\); the theorem covers every prime power\.

### A\.3Reference bounds and target selection

The reference tables record, for each parameter cell\(q,n,k,c\)\(q,n,k,c\), the listed lower and upper distance bounds and their construction sources\. Our comparison uses the bounds accessed on 17 July 2026\. The reference qubit table contains 563 entries whose distance bounds differ by one\. The artifact preserves these table data and a second copy retrieved on 10 September 2026; both cover qubit codes withn≤64n\\leq 64and qutrit codes withn≤36n\\leq 36\. The reproduction command uses the July reference data unless another retrieval date is explicitly selected\. Schema checks reject malformed records before classifying improvements or previously unlisted cells\.

An entry with distance interval\[dℓ,du\]\[d\_\{\\ell\},d\_\{u\}\]closes when construction and nonexistence bounds meet\. For\(q,n,k,c\)=\(2,7,1,4\)\(q,n,k,c\)=\(2,7,1,4\), a verified\[\[7,1,6;4\]\]2\[\[7,1,6;4\]\]\_\{2\}code closes the listed5≤d≤65\\leq d\\leq 6gap\. Cells absent from the reference tables are called*record targets*in the archive; absence alone does not establish novelty relative to all published constructions\.

The familiar BDH Singleton expression2​\(d−1\)≤n−k\+c2\(d\-1\)\\leq n\-k\+cis not a general bound in the large\-distance regime\([Grassl, 2021](https://arxiv.org/html/2610.41183#bib.bib6)\)\. Our principal family hasd=n−1d=n\-1, so we use the applicable generalized Singleton bounds of[Grassl et al\. \(2022\)](https://arxiv.org/html/2610.41183#bib.bib9)\. The\[\[12,1,11;5\]\]5\[\[12,1,11;5\]\]\_\{5\}code, for example, uses four fewer pairs than substitution into the BDH expression would suggest; it does not contradict a valid upper bound\.

For qubit \(q=2q=2\) linear stabilizer EAQECCs withk≥1k\\geq 1, the EA\-Plotkin bound\([Guo & Li, 2013](https://arxiv.org/html/2610.41183#bib.bib10)\)givesd≤⌊3⋅4k−1​n/\(4k−1\)⌋d\\leq\\lfloor 3\\cdot 4^\{k\-1\}n/\(4^\{k\}\-1\)\\rfloor\. It lowers 398 upper bounds in the reference*qubit*table\. The qubit target list retains cells not excluded by this inequality, the applicable Singleton bounds, or our certified refutations\.

### A\.4Sources and dates of previous bounds

The dates in Tables[2](https://arxiv.org/html/2610.41183#S4.T2)and[2](https://arxiv.org/html/2610.41183#S4.T2)refer to verified versions of public sources, not necessarily to the first discovery of each EAQECC parameter set\. The reference qubit table fixes which lower and upper bounds we compare against\. For\(7,1,4\)\(7,1,4\), the underlying pure\[\[11,1,5\]\]2\[\[11,1,5\]\]\_\{2\}code is recorded by[Calderbank et al\. \(1997\)](https://arxiv.org/html/2610.41183#bib.bib3); applying Theorem 7 of[Grassl et al\. \(2020\)](https://arxiv.org/html/2610.41183#bib.bib8)withℓ=4\\ell=4establishes the EAQECC lower bound by 15 October 2020\. The elapsed time to 17 July 2026 is 5\.8 years when rounded to one decimal\.

The other eight qubit rows use the July 12, 2022 version of[Luo et al\. \(2022\)](https://arxiv.org/html/2610.41183#bib.bib13)\. For oddn∈\{9,11,13,15\}n\\in\\\{9,11,13,15\\\}, Table I contains\[\[n−1,0,n−1;n−3\]\]2\[\[n\-1,0,n\-1;n\-3\]\]\_\{2\}\. Quantum shortening gives\[\[n−2,1,n−2;n−3\]\]2\[\[n\-2,1,n\-2;n\-3\]\]\_\{2\}, and two length extensions yield the previous\[\[n,1,n−2;n−3\]\]2\[\[n,1,n\-2;n\-3\]\]\_\{2\}bound\. The two even\-length rows arise similarly:

\]2\\displaystyle\]\_\{2\}⟶\[\[7,1,7;6\]\]2⟶\[\[10,1,7;6\]\]2,\\displaystyle\\longrightarrow\[\[7,1,7;6\]\]\_\{2\}\\longrightarrow\[\[10,1,7;6\]\]\_\{2\},\[\[10,0,10;8\]\]2\\displaystyle\[\[10,0,10;8\]\]\_\{2\}⟶\[\[9,1,9;8\]\]2⟶\[\[12,1,9;8\]\]2\.\\displaystyle\\longrightarrow\[\[9,1,9;8\]\]\_\{2\}\\longrightarrow\[\[12,1,9;8\]\]\_\{2\}\.A fourth length extension of\[\[9,1,9;8\]\]2\[\[9,1,9;8\]\]\_\{2\}also gives the previous\[\[13,1,9;8\]\]2\[\[13,1,9;8\]\]\_\{2\}bound\. For thek=2k=2row, the source’s\[\[17,0,12;9\]\]2\[\[17,0,12;9\]\]\_\{2\}code gives

\[\[17,0,12;9\]\]2⟶\[\[13,4,8;9\]\]2⟶\[\[13,2,8;9\]\]2⟶\[\[12,2,7;9\]\]2\[\[17,0,12;9\]\]\_\{2\}\\longrightarrow\[\[13,4,8;9\]\]\_\{2\}\\longrightarrow\[\[13,2,8;9\]\]\_\{2\}\\longrightarrow\[\[12,2,7;9\]\]\_\{2\}by four quantum shortenings, taking a subcode, and puncturing\. The rules and source codes are both present in the 2022 version, giving 4\.0 years between publication and our table access date\. These derivations match the provenance strings in the archived EAQECC table\. They establish that the baselines were available by the stated dates and still listed in 2026; they do not establish a complete chronology of intervening work\.

For the displayed qutrit rows, Table II of the same 2022 source contains\[\[10,0,8;4\]\]3\[\[10,0,8;4\]\]\_\{3\},\[\[10,0,9;6\]\]3\[\[10,0,9;6\]\]\_\{3\}, and\[\[13,1,10;8\]\]3\[\[13,1,10;8\]\]\_\{3\}\. Quantum shortening of\[\[10,0,8;4\]\]3\[\[10,0,8;4\]\]\_\{3\}gives\[\[9,1,7;4\]\]3\[\[9,1,7;4\]\]\_\{3\}\. Separately, increasing the dimension of the same\[\[10,0,8;4\]\]3\[\[10,0,8;4\]\]\_\{3\}source code using one additional shared pair gives\[\[10,1,8;5\]\]3\[\[10,1,8;5\]\]\_\{3\}\([Luo et al\., 2022](https://arxiv.org/html/2610.41183#bib.bib13), Section IV, rule \(6\)\)\. Applying this dimension\-increase rule to\[\[10,0,9;6\]\]3\[\[10,0,9;6\]\]\_\{3\}and then extending its length yields\[\[11,1,9;7\]\]3\[\[11,1,9;7\]\]\_\{3\}\. The fourth baseline is the listed\[\[13,1,10;8\]\]3\[\[13,1,10;8\]\]\_\{3\}code itself\. Theq=4,5q=4,5rows have no prior entry in the archived tables and are not included in these historical comparisons\.

## Appendix BThe discovery pipeline in detail

### B\.1Campaign configuration and verification

Across the four discovery campaigns, Google Cloud Vertex AI’s AlphaEvolve service sampledgemini\-3\.5\-flashandgemini\-3\.1\-pro\-previewequally, with four generation and four evaluation workers\. The four campaigns requested120120,120120,8080and8080programs; worker logs record120120,121121,8080and8080completed searches \(401 total\)\. Service counters are121121,122122,8181and8181, each including an initial program with a supplied score\. Completed searches determine the nominal allowance:401×240401\\times 240s, or26\.7326\.73h\. Archived records report1\.871\.87M input and3\.743\.74M output tokens\. Campaigns 1–2 share one task specification and campaigns 3–4 another \(Appendix[B\.3](https://arxiv.org/html/2610.41183#A2.SS3)\)\.

Campaign 1 records 120 completed searches\. The first new\[\[9,1,8;6\]\]2\[\[9,1,8;6\]\]\_\{2\}and\[\[11,1,10;8\]\]2\[\[11,1,10;8\]\]\_\{2\}codes precede completions 4 and 119, respectively: 0\.267 h and 7\.933 h of allocated search budget at 240 s per completed search\. The logs do not provide elapsed discovery times\. A later task records\[\[7,1,6;4\]\]2\[\[7,1,6;4\]\]\_\{2\}as an earlier construction without a first\-hit budget\. The\[\[13,1,12;10\]\]2\[\[13,1,12;10\]\]\_\{2\}record instead cites the closed\-form theorem as its source\. Initial and later tasks document the transition from finite constructions to the researcher\-derived family\. Algorithm[1](https://arxiv.org/html/2610.41183#alg1)is a later retained program; the logs do not identify a surviving source for every early discovery\. Section[5](https://arxiv.org/html/2610.41183#S5)uses separately generated, preserved programs and its own protocol\.

For the complementary finite\-field searches atq=4,5q=4,5, simulated annealing searchesL=span⁡\{𝝆1,…,𝝆j,𝒂,𝒃\}L=\\operatorname\{span\}\\\{\\boldsymbol\{\\rho\}\_\{1\},\\ldots,\\boldsymbol\{\\rho\}\_\{j\},\\boldsymbol\{a\},\\boldsymbol\{b\}\\\}withj=n−1−cj=n\-1\-cfixed, disjointZZ\-pair rows, each with entries\(1,1\)\(1,1\)\. Moves resample up to three entries of𝒂\\boldsymbol\{a\}or𝒃\\boldsymbol\{b\}\. The objective counts non\-radical span vectors below distancen−1n\-1by exact enumeration and Gram tests\. Full\-rank and⟨𝒂,𝒃⟩s≠0\\langle\\boldsymbol\{a\},\\boldsymbol\{b\}\\rangle\_\{s\}\\neq 0checks prune proposals; Metropolis acceptance, cooling and restarts guide search\. Before saving, a separate parameter calculation checks\(k,c,d\)=\(1,c,n−1\)\(k,c,d\)=\(1,c,n\-1\)\. All 23 archived matrices have this form and pass the independent Magma check\. The[artifact](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)supplies the routines and code\-to\-record mappings\.

The independent Magma check receives generators only and re\-derives every quantity we report\. Symplectic weight is obtained by embedding\(xi,zi\)↦xi\+ω​zi\(x\_\{i\},z\_\{i\}\)\\mapsto x\_\{i\}\+\\omega z\_\{i\}intoGF⁡\(q2\)\\mathrm\{GF\}\(q^\{2\}\), choosingω∉𝔽q\\omega\\notin\\mathbb\{F\}\_\{q\}\. Then\{1,ω\}\\\{1,\\omega\\\}is an𝔽q\\mathbb\{F\}\_\{q\}\-basis, so the image is zero exactly when\(xi,zi\)=\(0,0\)\(x\_\{i\},z\_\{i\}\)=\(0,0\)\. Magma’s ownWeight\(\)therefore counts nonzero coordinate pairs from the supplied generators\.

Algorithm[1](https://arxiv.org/html/2610.41183#alg1)summarizes the archived evolved construction program; its preserved source is available in the[artifact](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)\. The generator matrix𝐆\\mathbf\{G\}spansSS, andb​e​s​t​\[t\]best\[t\]stores the lowest\-cost proposal seen for targettt\. The objective remains5000\|r\.c−ct\|\+1000\|r\.k−kt\|\+r\.offending5000\|r\.c\-c\_\{t\}\|\+1000\|r\.k\-k\_\{t\}\|\+r\.\\mathrm\{offending\}, with cost10910^\{9\}for an evaluator error\. Herer\.offendingr\.\\mathrm\{offending\}counts𝒗∈S⟂∖Siso\\boldsymbol\{v\}\\in S^\{\\perp\}\\setminus S\_\{\\mathrm\{iso\}\}withwts⁡\(𝒗\)<dt\\operatorname\{wt\_\{s\}\}\(\\boldsymbol\{v\}\)<d\_\{t\}; it is an integer count\. After return, the external evaluator instead maximizes1000−offending1000\-\\mathrm\{offending\}for matching\(k,c\)\(k,c\), adding10610^\{6\}for a newly achieved archive target\. A signature mismatch scores−5000\|r\.c−ct\|−1000\-5000\|r\.c\-c\_\{t\}\|\-1000; the best proposal sets the program score\. Both calls use the exact parameter routine; Magma supplies the separate implementation check\. The campaign seed used fixed target weightsnt−2n\_\{t\}^\{\-2\}\. The evolved program uses normalized weights proportional tont−1\.5​\(1\+10​bt\)n\_\{t\}^\{\-1\.5\}\(1\+10b\_\{t\}\), initially withbt=0b\_\{t\}=0\. After a repair attempt,ProgressBonususes the stored best costot⋆o\_\{t\}^\{\\star\}:

bt←\{\(1\+ot⋆\)−1,0<ot⋆<100,0,ot⋆=0,bt,otherwise\.b\_\{t\}\\leftarrow\\begin\{cases\}\(1\+o\_\{t\}^\{\\star\}\)^\{\-1\},&0<o\_\{t\}^\{\\star\}<100,\\\\ 0,&o\_\{t\}^\{\\star\}=0,\\\\ b\_\{t\},&\\text\{otherwise\}\.\\end\{cases\}If no proposal was recorded, takeot⋆=109o\_\{t\}^\{\\star\}=10^\{9\}\. A proposal with zero cost at its initial evaluation takes the earliercontinuebranch and skips this bonus update, exactly as in the source\.

For a new attempt, the program samples one scalaruuand tests branches in order\. Ifu<0\.2u<0\.2and a stored positive\-cost proposal exists, it resumes from that matrix\. Otherwise,Constructuses a cyclic construction whenu<0\.4u<0\.4ands≤2​ns\\leq 2n, a divisor\-stride construction whenu<0\.6u<0\.6ands≤2​ns\\leq 2n, or a block construction whenu<0\.8u<0\.8\. If none applies, or the resulting rank is notss, it uses a random stabilizer\. The construction branches and their validity checks remain subject to the same exact evaluator as the seed\.

The cyclic branches use one or two nonzero base vectors\. Rowiitakes baseimodmi\\bmod mand rotates it by2​h​⌊i/m⌋mod2​n2h\\lfloor i/m\\rfloor\\bmod 2nbits, wheremmis the number of bases\. The ordinary cyclic branch setsh=1h=1; the added branch samples a positive proper divisor ofnn\. The block branch extends the allowed dual dimension from 8 to 12 and block sizes from\{2,4,6\}\\\{2,4,6\\\}to\{2,4,6,8\}\\\{2,4,6,8\\\}\.

During repair,MixedMovesamplesv∈\[0,1\)v\\in\[0,1\): ifv<0\.2v<0\.2ands≥2s\\geq 2, XOR two distinct rows; otherwise, ifv<0\.4v<0\.4, rotate one row by1,…,n−11,\\ldots,n\-1qubits uniformly; otherwise, apply a weight\-1–3 Pauli perturbation to one row\. The rotation changes one generator, not all coordinates of the code\. Rank\-deficient proposals incrementffwithout evaluation\. The inherited Metropolis loop cools by0\.9950\.995to0\.10\.1and restarts after 1,500 attempts without an accepted strict improvement\. It retains each target’s best accepted proposal and returns at most 16\. Figure[2](https://arxiv.org/html/2610.41183#S4.F2)shows source changes, not their individual performance effects\.

### B\.2The refutation encoding

EncodeL=S⟂L=S^\{\\perp\}usingj=n−k−cj=n\-k\-cradical generators𝝆1,…,𝝆j\\boldsymbol\{\\rho\}\_\{1\},\\ldots,\\boldsymbol\{\\rho\}\_\{j\}andkkhyperbolic pairs\(𝒖i,𝒗i\)\(\\boldsymbol\{u\}\_\{i\},\\boldsymbol\{v\}\_\{i\}\)\. Gram constraints enforce rank2​k2kand pair independence\. For qubits, all22​k\+j−2j2^\{2k\+j\}\-2^\{j\}non\-radical combinations must have weight at leastdd\. Gray\-code chaining changes one generator contribution at a time; Sinz counters enforce weight\. Whenj≥1j\\geq 1, local symplectic maps and coordinate permutations make𝝆1\\boldsymbol\{\\rho\}\_\{1\}a nonzeroZZ\-prefix\. For its bits\(xi,zi\)\(x\_\{i\},z\_\{i\}\), the CNF setsxi=0x\_\{i\}=0,z1=1z\_\{1\}=1and adds\(zi∨¬zi\+1\)\(z\_\{i\}\\lor\\neg z\_\{i\+1\}\)fori<ni<n\. These clauses allow every nonempty prefix in one CNF, without fixing its weight or making the other radical rowsZZ\-only\.

For qutrits, each field element is one\-hot encoded\. The radical basis is in reduced row echelon form, and modular state chains impose its Gram constraints\. Fork=1k=1, it suffices to test the four projective logical representatives𝒖,𝒗,𝒖\+𝒗,𝒖\+2​𝒗\\boldsymbol\{u\},\\boldsymbol\{v\},\\boldsymbol\{u\}\+\\boldsymbol\{v\},\\boldsymbol\{u\}\+2\\boldsymbol\{v\}, each shifted by every radical vector\. Their nonzero scalar multiples have the same weights\. Atd=n−1d=n\-1, pairwise clauses prevent a representative from vanishing at two coordinates\. The following lemma permits an additional normalization\.

###### Lemma 2\(Coordinate normalization\)\.

LetL≤𝔽q2​nL\\leq\\mathbb\{F\}\_\{q\}^\{2n\}have radicalRRwithdimL=dimR\+2\\dim L=\\dim R\+2anddimR\>2\\dim R\>2\. If every vector inL∖RL\\setminus Rhas symplectic weight at leastn−1n\-1, then local symplectic transformations can makeRRentirelyZZ\-type\.

###### Sketch of proof\.

By definition,R=rad⁡\(L\)=L∩L⟂R=\\operatorname\{rad\}\(L\)=L\\cap L^\{\\perp\}\. Letπi:𝔽q2​n→𝔽q2\\pi\_\{i\}:\\mathbb\{F\}\_\{q\}^\{2n\}\\to\\mathbb\{F\}\_\{q\}^\{2\}beπi​\(𝒗\)=\(xi,zi\)\\pi\_\{i\}\(\\boldsymbol\{v\}\)=\(x\_\{i\},z\_\{i\}\), andπi​h=\(πi,πh\):𝔽q2​n→𝔽q4\\pi\_\{ih\}=\(\\pi\_\{i\},\\pi\_\{h\}\):\\mathbb\{F\}\_\{q\}^\{2n\}\\to\\mathbb\{F\}\_\{q\}^\{4\}fori≠hi\\neq h\. WritingKi​h=ker⁡\(πi​h\|L\)K\_\{ih\}=\\ker\(\\pi\_\{ih\}\|\_\{L\}\), the distance hypothesis gives

Ki​h⊆\{𝒗∈L:wts⁡\(𝒗\)≤n−2\}⊆R,Ki​h=ker⁡\(πi​h\|R\)\.K\_\{ih\}\\subseteq\\\{\\boldsymbol\{v\}\\in L:\\operatorname\{wt\_\{s\}\}\(\\boldsymbol\{v\}\)\\leq n\-2\\\}\\subseteq R,\\qquad K\_\{ih\}=\\ker\(\\pi\_\{ih\}\|\_\{R\}\)\.Rank–nullity therefore yields

dimπi​h​\(L\)−dimπi​h​\(R\)=dimL−dimR=2,dimπi​h​\(R\)≤2\.\\dim\\pi\_\{ih\}\(L\)\-\\dim\\pi\_\{ih\}\(R\)=\\dim L\-\\dim R=2,\\qquad\\dim\\pi\_\{ih\}\(R\)\\leq 2\.Supposedimπi​\(R\)=2\\dim\\pi\_\{i\}\(R\)=2\. For everyh≠ih\\neq i,2=dimπi​\(R\)≤dimπi​h​\(R\)≤22=\\dim\\pi\_\{i\}\(R\)\\leq\\dim\\pi\_\{ih\}\(R\)\\leq 2\. Hence the inclusionker⁡\(πi​h\|R\)⊆ker⁡\(πi\|R\)\\ker\(\\pi\_\{ih\}\|\_\{R\}\)\\subseteq\\ker\(\\pi\_\{i\}\|\_\{R\}\)is an equality, since both kernels have dimensiondimR−2\\dim R\-2\. Consequently

ker⁡\(πi\|R\)=⋂h≠iker⁡\(πi​h\|R\)=\{𝟎\},\\ker\(\\pi\_\{i\}\|\_\{R\}\)=\\bigcap\_\{h\\neq i\}\\ker\(\\pi\_\{ih\}\|\_\{R\}\)=\\\{\\boldsymbol\{0\}\\\},which impliesdimR=dimπi​\(R\)=2\\dim R=\\dim\\pi\_\{i\}\(R\)=2, a contradiction\. ThusdimPi≤1\\dim P\_\{i\}\\leq 1for everyPi:=πi​\(R\)P\_\{i\}:=\\pi\_\{i\}\(R\)\.

IfPi=\{𝟎\}P\_\{i\}=\\\{\\boldsymbol\{0\}\\\}, takeMi=I2M\_\{i\}=I\_\{2\}\. Otherwise writePi=span⁡\{𝒘i\}P\_\{i\}=\\operatorname\{span\}\\\{\\boldsymbol\{w\}\_\{i\}\\\}with𝒘i=\(ai,bi\)𝖳≠𝟎\\boldsymbol\{w\}\_\{i\}=\(a\_\{i\},b\_\{i\}\)^\{\\mathsf\{T\}\}\\neq\\boldsymbol\{0\}, and set

Mi=\{\(bi−aiai−10\),ai≠0,\(bi00bi−1\),ai=0\.M\_\{i\}=\\begin\{cases\}\\begin\{pmatrix\}b\_\{i\}&\-a\_\{i\}\\\\ a\_\{i\}^\{\-1\}&0\\end\{pmatrix\},&a\_\{i\}\\neq 0,\\\\\[3\.0pt\] \\begin\{pmatrix\}b\_\{i\}&0\\\\ 0&b\_\{i\}^\{\-1\}\\end\{pmatrix\},&a\_\{i\}=0\.\\end\{cases\}In both casesdetMi=1\\det M\_\{i\}=1andMi​𝒘i=\(0,1\)𝖳M\_\{i\}\\boldsymbol\{w\}\_\{i\}=\(0,1\)^\{\\mathsf\{T\}\}\. ForJ=\(01−10\)J=\\left\(\\begin\{smallmatrix\}0&1\\\\ \-1&0\\end\{smallmatrix\}\\right\),Mi𝖳​J​Mi=JM\_\{i\}^\{\\mathsf\{T\}\}JM\_\{i\}=J\. ThereforeT=diag⁡\(M1,…,Mn\)T=\\operatorname\{diag\}\(M\_\{1\},\\ldots,M\_\{n\}\)is symplectic and

T\(R\)⊆\{\(0,z1,…,0,zn\):zi∈𝔽q\},wts\(T𝒗\)=wts\(𝒗\)\(𝒗∈𝔽q2​n\)\.T\(R\)\\subseteq\\\{\(0,z\_\{1\},\\ldots,0,z\_\{n\}\):z\_\{i\}\\in\\mathbb\{F\}\_\{q\}\\\},\\qquad\\operatorname\{wt\_\{s\}\}\(T\\boldsymbol\{v\}\)=\\operatorname\{wt\_\{s\}\}\(\\boldsymbol\{v\}\)\\quad\(\\boldsymbol\{v\}\\in\\mathbb\{F\}\_\{q\}^\{2n\}\)\.The weight identity follows because everyMiM\_\{i\}is invertible\. ThusTTgives the required local normalization\. ∎

The lemma also applies to binary targets withk=1k=1,d≥n−1d\\geq n\-1andj\>2j\>2\. Adding all radical\-XXzero constraints to the seven binary exclusions gives seven further UNSAT instances with checked DRAT proofs\. A feasible\[\[6,1,5;2\]\]2\[\[6,1,5;2\]\]\_\{2\}control remains SAT and its decoded generators pass independent parameter checks\. The artifact preserves these normalized certificates alongside the original ones\.

For\[\[10,1,9;4\]\]3\[\[10,1,9;4\]\]\_\{3\},j=5j=5\. Row reduction preserves the zeroXXcomponents, so the normalized encoding retains every possible code\. Addingj​n=50jn=50unit clauses gives33,03333\{,\}033variables and476,271476\{,\}271clauses\. The lemma establishes completeness; DRAT certifies unsatisfiability\. As a positive control, the same normalized encoder is SAT when fixed to the archived\[\[10,1,9;5\]\]3\[\[10,1,9;5\]\]\_\{3\}code\. The[artifact](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)supplies the CNF, proof, normalization metadata and checks of the added clauses\.

For certificate verification, the original CNFs are summarized in Table[3](https://arxiv.org/html/2610.41183#A2.T3)\. Solver time measures a fresh UNSAT decision; for\[\[10,1,9;5\]\]2\[\[10,1,9;5\]\]\_\{2\}, it also includes proof generation\. The check time uses DRAT\-trim\. Peak is the larger solver/checker resident set\. Concurrent workloads preclude isolated timing comparisons\. Execution conditions and logs are in the[artifact](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)\.

Table 3:Original SAT refutation resources\.
### B\.3Researcher proposals and task specifications

These structured summaries separate researcher input from the task given to the model\. Shaded rows mark researcher proposals or findings\. Full specifications are preserved verbatim in the[artifact](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)\. The controlled study is separate from the discovery campaigns\.

Discovery campaigns 1–2Initial search

Researcher proposalExplore cyclic qubit shifts, constructive warm starts,GF⁡\(4\)\\mathrm\{GF\}\(4\)\-additive constructions and coupled generator moves\. Reuse structure between targets sharing\(n,c\)\(n,c\)\.

Task to the modelConstruct binary EAQECCs for 68 open table entries\. Each target\[\[n,k,d;c\]\]2\[\[n,k,d;c\]\]\_\{2\}has listed lower distance boundd−1d\-1and upper bounddd\.

Exact feedbackMatch the requested\(k,c\)\(k,c\)and reach distancedd\. The evaluator checks the symplectic constraints and reports the number of nontrivial logical operators below the target distance\.

Knowledge suppliedStabilizer representation, evaluator access and construction directions\. The family formula derived later was not supplied\.

Source: archived task specifications for campaigns 1 and 2\.

Discovery campaigns 3–4After generalization

Researcher resultThe recorded qubit constructions\[\[7,1,6;4\]\]2\[\[7,1,6;4\]\]\_\{2\},\[\[9,1,8;6\]\]2\[\[9,1,8;6\]\]\_\{2\}and\[\[11,1,10;8\]\]2\[\[11,1,10;8\]\]\_\{2\}were generalized by researchers to the odd\-length family\[\[n,1,n−1;n−3\]\]2\[\[n,1,n\-1;n\-3\]\]\_\{2\}\.

Researcher proposalDevelop further constructions using other shift steps, quasi\-cyclic orbits, multiple radical blocks,GF⁡\(4\)\\mathrm\{GF\}\(4\)\-additive constructions, and extension, shortening or puncturing of the known family\.

Task to the modelSearch 329 qubit parameter targets with5≤n≤135\\leq n\\leq 13, including listed gaps and previously unlisted parameter cells\. The task now explicitly includes the discovered qubit family\.

Exact feedbackUse the same parameter and distance checks\. The specification also permits constructing the smaller dual space and converting it to stabilizer generators for evaluation\.

Source: archived task specifications for campaigns 3 and 4\.

Controlled studyShared proposal for both policies

Researcher proposalMaintain and mutate a basis ofL=S⟂L=S^\{\\perp\}throughout search\. Convert each candidateLLtoSSfor exact evaluation\. For the training targets,LLhas only four basis vectors\.

Task to the modelImplementsearch\(target, max\_evals\)under a separate quota for each target and seed\. Independent proposals and iterative evolution receive the same research suggestion\.

Information withheldNo successful code matrix, family formula or workingLL\-side search program is supplied\. There is no controller\-provided initialization\.

Source: archived controlled\-study task; this is separate from the discovery campaigns\.

The controlled\-study protocol and calibration are specified in Appendix[C\.1](https://arxiv.org/html/2610.41183#A3.SS1)\.

## Appendix CResearch\-guided ablation details

### C\.1Shared research guidance and evaluation calibration

The controlled study uses Gemini 3\.5 Flash through VertexgenerateContent, with a local program\-development controller\. It is distinct from the managed AlphaEvolve discovery campaigns\. The two policies receive identical instructions to maintain and mutateL=S⟂L=S^\{\\perp\}throughout search and convert candidate bases toSSusing binary nullspace and symplectic\-swap helpers\. The initial code is the sameSS\-side annealing callback in both policies\. There is no protected initializer\. Programs may change representations, objectives, mutation operators and restart schedules; the workingLL\-side calibration code, archived codes and family formula are not provided to either policy\.

Before model generation, four calibration seeds compare the initial callback with an interface\-adapted, researcher\-assistedLL\-side control at up to10510^\{5\}evaluator calls\. The controls depend on the call limit only through the remaining allowance, so their first\-hit records give success curves at 1,000, 3,000, 10,000, 30,000 and 100,000 calls\. Atn=9n=9, the rule selects the smallest grid budget with initial success between 0\.1 and 0\.5, control success at least 0\.5 and a difference of at least 0\.25\. A second cell may have zero initial success if the control succeeds in at least half the executions\. The selected budget is 10,000: initial/control success is 1/4 versus 2/4 atn=9n=9, and 0/4 versus 2/4 atn=11n=11\. Calibration is a test of whether the evaluator can reward a useful edit, not a measurement of evolutionary contribution\. Independently verified codes establish feasibility at all training and transfer parameters before generation\.

### C\.2Generation, interruption and selection

Four blocks each plan 12 proposals per policy\. Independent proposals receive the fixed initial source and its fixed training feedback\. Iterative evolution receives the best\-so\-far source and the latest attempt, including rejected attempts, with their training feedback\. Training uses two fixed execution seeds atn=9,11n=9,11\. Each proposal is ranked lexicographically by mean normalized success\-curve area, success fraction and clipped distance ratio; earlier proposals break remaining ties\. For first\-hit callhhunder allowanceBB, the primary utility is

u⁡\(h,B\)=\{1−h/B,if the target is solved by call​B,0,otherwise\.u\(h;B\)=\\begin\{cases\}1\-h/B,&\\text\{if the target is solved by call \}B,\\\\ 0,&\\text\{otherwise\.\}\\end\{cases\}This equals the normalized integral of the success indicator over the available evaluator\-call budget\. The initial program remains eligible for selection\. Proposal counts match; token and execution costs need not\.

The planned 12\-proposal runs received 58 model responses before unavailable responses interrupted generation\. Before any validation or test observations, a completion\-only rule retained the longest fully received prefix shared by every policy and block: seven proposals each, 56 total\. The two additional responses and all request records are preserved separately\. Earlier exploratory studies informed calibration and guidance; their measurements are not pooled into this comparison\.

For the included 28 requests per policy, recorded input/output/reasoning token totals are 50,344/22,891/22,780 for independent proposals and 86,501/26,145/32,128 for iterative evolution\. Mean request latency is 8\.77 s and 11\.93 s, respectively\. The additional source and feedback in iterative prompts therefore incur greater model usage despite equal proposal counts\. Receipt\-level accounting is preserved in the artifact; service latency is separate from search time\.

After generation ends, four new validation seeds at the training parameters select among each policy/block’s three training\-best distinct programs, using the same metric order and then training rank\. The eight selected programs are distinct\. Test uses eight further seeds at each training parameter and 10,000 calls per execution\. The separate length transfer usesn=13,15n=13,15, four seeds and 30,000 calls\. Transfer measurements never enter selection\. All seed lists, requests, source hashes, parent relationships, candidate outcomes and selections are retained inexperiments/hitl\_ablation/\.

### C\.3Complete policy outcomes

Table[4](https://arxiv.org/html/2610.41183#A3.T4)reports the original test cohort and the 32\-seed repeat of the same validation\-selected programs\. Displayed values are rounded; differences use unrounded values\. The new seeds were fixed before execution and did not change any program or selection\. The original paired mean curve\-area difference is\+0\.1188\+0\.1188\(two positive blocks\), versus\+0\.0044\+0\.0044in the repeat \(one positive block\)\. Descriptive two\-sided sign\-flip values over the four block differences are 0\.50 and 1\.00\. These calculations use four generation blocks; execution seeds within one program quantify its run\-to\-run variability\. Excluding the block affected by later unavailable responses gives an original mean difference of\+0\.0819\+0\.0819\. All included proposals precede those responses\.

Table 4:Test outcomes by generation block\.Iterative selections are proposals 2, 1, 3 and 1 in blocks 1–4, respectively \(proposal numbers start at one\)\. Thus two selections are first proposals and two incorporate feedback from earlier generated programs\. The classicalLL\-side control uses the shared proposed representation with the preserved annealing objective, moves and restart policy; its source is unchanged from calibration\.

The repeat covers 32 new seeds at each ofn=9,11,13,15n=9,11,13,15, at 10,000 calls for the first two lengths and 30,000 for the latter two\. It includes all eight selected programs, both fixed controls, and the first two programs in the block\-3 iterative lineage\. Together with 24 executions of the classical control on the original test and longer\-code seeds, this gives 1,560 executions and 545 independently verified successful code records, with no process errors\. All records, program hashes and the frozen protocol are inexperiments/hitl\_followup/\.

Atn=9,11n=9,11, the repeat gives 96/128 and 39/128 successes for independent proposals, versus 81/128 and 34/128 for iterative evolution\. The classical control gives 26/32 and 10/32, and the initial program 1/32 and 0/32\. Figure[5](https://arxiv.org/html/2610.41183#A3.F5)shows the longer\-code curves; the artifact also retains the complete four\-length plot\.

\(a\)n=13,d=12n=13,\\ d=120255075100Success rate \(%\)Exact evaluations010k20k30k\(b\)n=15,d=14n=15,\\ d=140255075100Success rate \(%\)Exact evaluations010k20k30kInitial programClassical L\-side controlIndependent proposalsIterative evolution

Figure 5:Longer\-code replay on fresh execution seeds\.Helper computations remain outside the evaluator\-call count but inside the common resource limits\. Each target/seed runs in a separate sandbox with 120/125 s soft/hard CPU limits, 135 s wall time and 1 GiB resident memory\. Every explicit or returned\-candidate verification consumes the same call quota\. Execution times and model request latencies are recorded separately in the artifact\.

The artifact audit reconstructs the original proposal inputs and parent relationships, checks validation selections and independently verifies saved code records\. The complete inputs and replay commands are available in the[artifact](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)\.

### C\.4Prospective generation replication

The new cohort fixes eight paired blocks and seven proposal slots per policy before generation\. Model, shared task, starting program, representation helpers, ranking and validation selection match the original study\. New model seeds and disjoint training, validation, test and longer\-code execution seeds separate the cohorts\. Each block uses two training seeds, four validation seeds and 32 held\-out seeds per length\. The test budget is 10,000 calls atn=9,11n=9,11; longer\-code performance at 30,000 calls is secondary\.

Of 112 allocated slots, 111 return programs: 56 independent and 55 iterative\. One response in block 8 is unavailable\. Before validation or testing, the recorded rule retained all eight blocks, using received programs without replacing the missing proposal\. Subsequent iterative requests use the most recent received source and feedback\. The seven fully received paired blocks provide a sensitivity analysis\. No program is reselected using test or longer\-code outcomes\.

Table[5](https://arxiv.org/html/2610.41183#A3.T5)reports all blocks; each longer\-length entry has 32 executions per policy and block\. The mean primary curve\-area difference is\+0\.0987\+0\.0987; five differences are positive and the descriptive two\-sided sign\-flip value isp=0\.3281p=0\.3281\. On the seven complete blocks, the mean difference is\+0\.1504\+0\.1504\. These are eight paired generation observations, not 512 independent generation trials\.

BlockIndependentIterativeΔ\\Deltaarean=13n=13n=15n=15Test successes /64Independent / iterative12519\-0\.0633 / 50 / 222530\+0\.0073 / 100 / 532435\-0\.0012 / 151 / 443945\+0\.02117 / 165 / 752664\+0\.5786 / 322 / 3263440\+0\.09515 / 80 / 372562\+0\.4173 / 320 / 288252\-0\.2641 / 00 / 0Total/mean223/512297/512\+0\.099\+0\.09950 / 1188 / 81Table 5:New generation blocks\.All 16 selected sources are distinct\. Source inspection finds sustained search inLL, with exact distance feedback obtained through the common charged evaluator\. Rank checks and basis conversions do not compute distance privately\. One program performs uncharged basis\-row additions that leave the subspace unchanged; other proposals evaluate their candidate subspaces\. Reads of the incumbent before search return no matrix because controller initialization is disabled\. The artifact audit reconstructs all 111 prompts and parent choices, reproduces validation selection, checks evaluation quotas and independently verifies saved codes\.

The received independent requests use 100,632 input, 41,801 output and 58,067 reported reasoning tokens; iterative requests use 165,819, 49,296 and 64,426, respectively\. Equal proposal allocations therefore do not imply equal token costs\. Full transport records and the missing\-response rule are preserved in the artifact\.

For Figure[4](https://arxiv.org/html/2610.41183#S5.F4), the original initial program and classicalLL\-side control are also run on these execution seeds\. This fixed\-control replay was added after the new policy results were available; neither control was modified, tuned or selected using them\. Each control has 32 runs per length, and is separate from the eight paired policy observations\. These runs contextualize the success curves; the prespecified policy endpoint and its analysis remain unchanged\.

### C\.5Preserved program and generalization to longer codes

In the original four\-block cohort, the program selected in block 3 isb02\_evolution\_g02, whose preserved parent isb02\_evolution\_g01; generation indices start at zero\. The parent already searchesLLand penalizes distance shortfall\. The child increases the ebit\-mismatch weight from 5,000 to 10,000 and the offending weight from 1 to 100\. It also mixes row replacement, Pauli perturbations and basis\-row mixing, scales mutation size with length, and restores a saved local best with a capped temperature adjustment after stagnation\. Tinted expressions in Algorithm[2](https://arxiv.org/html/2610.41183#alg2)mark these edits relative to this immediate parent; the inheritedLL\-side representation and distance\-shortfall term are not tinted\. These changes are observed in the preserved source, rather than inferred from performance alone\. The repeat below measures the combined changes in this final step\.

Algorithm 2Evolved search in the symplectic dual\.1:target

\(n,kt,ct,dt\)\(n,k\_\{t\},c\_\{t\},d\_\{t\}\), exact\-evaluation budget

NN
2:

Φ\(R\)=104\|R\.c−ct\|\+100R\.offending\+103Δd\(R\)\\Phi\(R\)=\\hbox\{\\pagecolor\{achieve\!13\}$10^\{4\}$\}\|R\.c\-c\_\{t\}\|\+\\hbox\{\\pagecolor\{achieve\!13\}$100$\}R\.\\mathrm\{offending\}\+10^\{3\}\\Delta\_\{d\}\(R\)⊳\\trianglerightIncrease penalties for entanglement mismatch and low\-weight violations\.

3:

r←n\+kt−ctr\\leftarrow n\+k\_\{t\}\-c\_\{t\}
4:whilebudget remainsdo

5:

L←L\\leftarrowa random independent list of

rrPauli vectors

6:

C←Φ⁡\(Eval​\(L⟂\)\)C\\leftarrow\\Phi\(\\textsc\{Eval\}\(L^\{\\perp\}\)\);\(L∗,C∗\)←\(L,C\)\(L\_\{\*\},C\_\{\*\}\)\\leftarrow\(L,C\)⊳\\trianglerightRetain the best state within each restart\.

7:

τ←50\\tau\\leftarrow\\hbox\{\\pagecolor\{achieve\!13\}$50$\};

f←0f\\leftarrow 0;g←0g\\leftarrow 0

8:while

f<600f<\\hbox\{\\pagecolor\{achieve\!13\}$600$\}andbudget remainsdo

9:

τ←max⁡\(0\.01,0\.995​τ\)\\tau\\leftarrow\\max\(\\hbox\{\\pagecolor\{achieve\!13\}$0\.01$\},0\.995\\tau\)
10:

L′←MixedMove​\(L\)L^\{\\prime\}\\leftarrow\\hbox\{\\pagecolor\{achieve\!13\}$\\textsc\{MixedMove\}\(L\)$\}⊳\\trianglerightAdd row mixing and allow larger Pauli changes at longer lengths\.

11:if

rank⁡L′≠r\\operatorname\{rank\}\\,L^\{\\prime\}\\neq rthen

f←f\+1f\\leftarrow f\+1;continue

12:

C′←Φ⁡\(Eval​\(\(L′\)⟂\)\)C^\{\\prime\}\\leftarrow\\Phi\(\\textsc\{Eval\}\(\(L^\{\\prime\}\)^\{\\perp\}\)\);

δ←C′−C\\delta\\leftarrow C^\{\\prime\}\-C
13:if

δ≤0\\delta\\leq 0or

U\(0,1\)<exp\(−δ/τ\)U\(0,1\)<\\exp\(\-\\delta/\\tau\)then

14:

\(L,C\)←\(L′,C′\)\(L,C\)\\leftarrow\(L^\{\\prime\},C^\{\\prime\}\)
15:ifC<C∗C<C\_\{\*\}then

16:\(L∗,C∗\)←\(L,C\)\(L\_\{\*\},C\_\{\*\}\)\\leftarrow\(L,C\);g←0g\\leftarrow 0

17:else

18:g←g\+1g\\leftarrow g\+1

19:endif

20:if

δ<0\\delta<0then

f←0f\\leftarrow 0else

f←f\+1f\\leftarrow f\+1
21:else

22:

f←f\+1f\\leftarrow f\+1;g←g\+1g\\leftarrow g\+1

23:endif

24:ifg\>80g\>80then⊳\\trianglerightOn stagnation, return to the best state and adjust the temperature\.

25:\(L,C\)←\(L∗,C∗\)\(L,C\)\\leftarrow\(L\_\{\*\},C\_\{\*\}\);g←0g\\leftarrow 0

26:τ←min⁡\(30,1\.5​τ\)\\tau\\leftarrow\\min\(30,1\.5\\tau\)

27:endif

28:endwhile

29:endwhile

30:returnthe evaluator’s best verified record, if any

Shading: changes from the immediate parent; exact definitions in Appendix[C\.5](https://arxiv.org/html/2610.41183#A3.SS5)\.

The program cost in Algorithm[2](https://arxiv.org/html/2610.41183#alg2)is

Φ\(R\)=104\|R\.c−ct\|\+100R\.offending\+103Δd\(R\),\\Phi\(R\)=10^\{4\}\|R\.c\-c\_\{t\}\|\+100\\,R\.\\mathrm\{offending\}\+10^\{3\}\\Delta\_\{d\}\(R\),whereΔd\(R\)=max\(0,dt−R\.d\)\\Delta\_\{d\}\(R\)=\\max\(0,d\_\{t\}\-R\.d\), ordtd\_\{t\}if distance is unavailable\. If the offending count or entanglement cost is missing, the score is10910^\{9\}\. These definitions match the preserved source\.

In Algorithm[2](https://arxiv.org/html/2610.41183#alg2), a random Pauli perturbation has weight uniformly sampled from1,…,max⁡\(2,⌊n/2⌋\)−11,\\ldots,\\max\(2,\\lfloor n/2\\rfloor\)\-1\.MixedMovechooses a row uniformly: with probability 0\.3 it replaces the row by such a perturbation, with probability 0\.3 it XORs the perturbation into the row, and otherwise it samples a second row\. If that row is different, it XORs the two rows and, with probability 0\.5, adds a Pauli perturbation\. A rank\-deficient proposal incrementsffand skips evaluation\. Otherwise,ffresets only on an accepted improvement over the current cost, and increments on all other moves\. The counterggresets on a new restart\-local best and increments on other evaluated moves\. Atg\>80g\>80, the program restores that best, setsg=0g=0and appliesτ←min⁡\(30,1\.5​τ\)\\tau\\leftarrow\\min\(30,1\.5\\tau\)\. This adjustment can lower a temperature still above 30; it is not always a temperature increase\. The source and its budget behavior remain unchanged\.

The original child achieves 16/16 primary\-test successes and 3/4 at each longer length\. Its successful longer\-code executions use 3,260–9,755 calls atn=13n=13and 7,125–16,756 atn=15n=15\. Table[6](https://arxiv.org/html/2610.41183#A3.T6)reports every preserved lineage stage on the 32 new seeds; the original validation selection is unchanged\. Between the first proposal and parent, the only functional search change is the distance\-shortfall penalty\. Between parent and selected child, several policies change together\. This lineage was chosen for diagnosis after its original performance, so the table describes that program’s development separately from the four\-block policy comparison\.

Table 6:Preserved lineage on fresh execution seeds\.All eight selected programs implement sustainedLL\-side repair\. Each passes candidate matrices to the common evaluator throughout search; none substitutes a private distance test that filters solutions before their first charged evaluation\.

## Appendix DLean verification of Theorem 1

The formal artifact verifies the algebraic construction underlying Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)\. Its shared definitions import Mathlib; the construction proof is a separate module\. The challenge imports only those definitions, and the submitted solution imports the construction proof\. The sources and pinned project are in the[artifact](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)\.

### D\.1Exact goal and mathematical interpretation

Use the field𝔽q\\mathbb\{F\}\_\{q\}and enumerationu1,…,uqu\_\{1\},\\ldots,u\_\{q\}from Appendix[A\.2](https://arxiv.org/html/2610.41183#A1.SS2)\. Lean denotes this field by𝔽\\mathbb\{F\}and its cardinality byFintype\.card𝔽\\mathbb\{F\}, which equalsqq\. The natural numbertailist=n−2​q\>0t=n\-2q\>0; hencen=2​q\+tn=2q\+t\. The disjunction below specifies the sameq≥3q\\geq 3and odd\-length binary cases as Theorem[1](https://arxiv.org/html/2610.41183#Thmtheorem1)\. Within namespaceEAQECCFamily\.Comparator, the submitted declaration is:

theoremtheorem1\_exact\_goal

\{𝔽\\mathbb\{F\}:Typeu\}\[Field𝔽\\mathbb\{F\}\]\[Fintype𝔽\\mathbb\{F\}\]\[DecidableEq𝔽\\mathbb\{F\}\]

\{tail:ℕ\\mathbb\{N\}\}\[NeZerotail\]

\(hcase:3≤\\leqFintype\.card𝔽\\mathbb\{F\}∨\\lor

\(Fintype\.card𝔽\\mathbb\{F\}=2∧\\landOdd\(2\*Fintype\.card𝔽\\mathbb\{F\}\+tail\)\)\):

∃\\existsz2lam:𝔽\\mathbb\{F\},lam≠\\neq0∧\\land1\+z2≠\\neq0∧\\land

Nonempty\(NormalizerSideCertificate𝔽\\mathbb\{F\}tailz2lam\):=by

exacttheorem1\_exacthcase

Lean represents the radical coefficients by the function space

𝒯=\{f:𝔽q→𝔽q\}\.\\mathcal\{T\}=\\\{f:\\mathbb\{F\}\_\{q\}\\to\\mathbb\{F\}\_\{q\}\\\}\.A functionffassigns one scalar to each field element;ffneed not be linear\. Addition and scalar multiplication are pointwise,\(f\+g\)​\(u\)=f⁡\(u\)\+g⁡\(u\)\(f\+g\)\(u\)=f\(u\)\+g\(u\)and\(a​f\)​\(u\)=a​f​\(u\)\(af\)\(u\)=af\(u\)fora∈𝔽qa\\in\\mathbb\{F\}\_\{q\}\. The enumerationu1,…,uqu\_\{1\},\\ldots,u\_\{q\}identifiesffwith the vector𝝉=\(f⁡\(u1\),…,f⁡\(uq\)\)∈𝔽qq\\boldsymbol\{\\tau\}=\(f\(u\_\{1\}\),\\ldots,f\(u\_\{q\}\)\)\\in\\mathbb\{F\}\_\{q\}^\{q\}\. This evaluation map is a linear isomorphism, sodim𝔽q𝒯=q\\dim\_\{\\mathbb\{F\}\_\{q\}\}\\mathcal\{T\}=q\. Thus Lean’sClosedCoefftype is𝒞=𝔽q2⊕𝒯≅𝔽qq\+2\\mathcal\{C\}=\\mathbb\{F\}\_\{q\}^\{2\}\\oplus\\mathcal\{T\}\\cong\\mathbb\{F\}\_\{q\}^\{q\+2\}\. Write𝜼=\(α,β,f\)\\boldsymbol\{\\eta\}=\(\\alpha,\\beta,f\)andτi=f⁡\(ui\)\\tau\_\{i\}=f\(u\_\{i\}\), matching the coefficients of𝒂,𝒃,𝝆i\\boldsymbol\{a\},\\boldsymbol\{b\},\\boldsymbol\{\\rho\}\_\{i\}in Appendix[A\.2](https://arxiv.org/html/2610.41183#A1.SS2)\. Relabeling the paired coordinates byi=1,…,qi=1,\\ldots,q, the linear mapΦ=closedWord\\Phi=\\texttt\{closedWord\}is

Φ​\(𝜼\)\(i,0\)\\displaystyle\\Phi\(\\boldsymbol\{\\eta\}\)\_\{\(i,0\)\}=\(α\+β​ui,β\+τi\),\\displaystyle=\(\\alpha\+\\beta u\_\{i\},\\,\\beta\+\\tau\_\{i\}\),Φ​\(𝜼\)\(i,1\)\\displaystyle\\Phi\(\\boldsymbol\{\\eta\}\)\_\{\(i,1\)\}=\(α\+β​ui,β​z2−τi\),\\displaystyle=\(\\alpha\+\\beta u\_\{i\},\\,\\beta z\_\{2\}\-\\tau\_\{i\}\),Φ​\(𝜼\)tail,j\\displaystyle\\Phi\(\\boldsymbol\{\\eta\}\)\_\{\\mathrm\{tail\},j\}=\(α,βλj\),0≤j<t,\\displaystyle=\(\\alpha,\\,\\beta\\lambda\_\{j\}\),\\qquad 0\\leq j<t,whereλ0=λ\\lambda\_\{0\}=\\lambdaandλj=1\\lambda\_\{j\}=1forj\>0j\>0\. ThusΦ⁡\(𝜼\)=α​𝒂\+β​𝒃\+∑i=1qτi​𝝆i\\Phi\(\\boldsymbol\{\\eta\}\)=\\alpha\\boldsymbol\{a\}\+\\beta\\boldsymbol\{b\}\+\\sum\_\{i=1\}^\{q\}\\tau\_\{i\}\\boldsymbol\{\\rho\}\_\{i\}in the formal coordinate order\. LetL=im⁡ΦL=\\operatorname\{im\}\\Phi,𝒞0=\{\(0,0,f\):f∈𝒯\}\\mathcal\{C\}\_\{0\}=\\\{\(0,0,f\):f\\in\\mathcal\{T\}\\\}, andδ=⟨Φ⁡\(1,0,0𝒯\),Φ⁡\(0,1,0𝒯\)⟩s\\delta=\\langle\\Phi\(1,0,0\_\{\\mathcal\{T\}\}\),\\Phi\(0,1,0\_\{\\mathcal\{T\}\}\)\\rangle\_\{s\}, where0𝒯0\_\{\\mathcal\{T\}\}is the zero function\. The certificate constructed bytheorem1\_exactproves:

1. \(1\)encodeInjectiveanddeltaNonzero:Φ\\Phiis injective andδ≠0\\delta\\neq 0\.
2. \(2\)gramFormulaandradicalIff: for all𝜼=\(α,β,f\)\\boldsymbol\{\\eta\}=\(\\alpha,\\beta,f\)and𝜼′=\(α′,β′,g\)\\boldsymbol\{\\eta\}^\{\\prime\}=\(\\alpha^\{\\prime\},\\beta^\{\\prime\},g\), ⟨Φ⁡\(𝜼\),Φ⁡\(𝜼′\)⟩s=\(α​β′−β​α′\)​δ,Φ⁡\(𝜼\)∈rad⁡\(L\)⇔𝜼∈𝒞0\.\\langle\\Phi\(\\boldsymbol\{\\eta\}\),\\Phi\(\\boldsymbol\{\\eta\}^\{\\prime\}\)\\rangle\_\{s\}=\(\\alpha\\beta^\{\\prime\}\-\\beta\\alpha^\{\\prime\}\)\\delta,\\qquad\\Phi\(\\boldsymbol\{\\eta\}\)\\in\\operatorname\{rad\}\(L\)\\iff\\boldsymbol\{\\eta\}\\in\\mathcal\{C\}\_\{0\}\.
3. \(3\)normalizerFinrankandradicalFinrank:dimL=q\+2\\dim L=q\+2anddim𝒞0=q\\dim\\mathcal\{C\}\_\{0\}=q\.
4. \(4\)distanceLoweranddistanceAttained: ∀𝜼∉𝒞0,wts⁡\(Φ⁡\(𝜼\)\)≥n−1,∃𝜼∉𝒞0,wts⁡\(Φ⁡\(𝜼\)\)=n−1\.\\forall\\boldsymbol\{\\eta\}\\notin\\mathcal\{C\}\_\{0\},\\quad\\operatorname\{wt\_\{s\}\}\(\\Phi\(\\boldsymbol\{\\eta\}\)\)\\geq n\-1,\\qquad\\exists\\boldsymbol\{\\eta\}\\notin\\mathcal\{C\}\_\{0\},\\quad\\operatorname\{wt\_\{s\}\}\(\\Phi\(\\boldsymbol\{\\eta\}\)\)=n\-1\.

Injectivity identifiesΦ⁡\(𝒞0\)\\Phi\(\\mathcal\{C\}\_\{0\}\)with theqq\-dimensional radical ofLL\. TakingS=L⟂S=L^\{\\perp\}givesdimS=2​n−q−2\\dim S=2n\-q\-2\. The standard stabilizer correspondence \(Appendix[A\.1](https://arxiv.org/html/2610.41183#A1.SS1)\) therefore yieldsc=\(dimS−q\)/2=n−q−1c=\(\\dim S\-q\)/2=n\-q\-1,k=n−dimS\+c=1k=n\-\\dim S\+c=1andd=n−1d=n\-1\. These are the code parameters recorded by the certificate; the proof\-bearing fields above certify their underlying symplectic construction\.

For the coordinate convention, Lean’s\(ui,false\)\(u\_\{i\},\\mathrm\{false\}\)and\(ui,true\)\(u\_\{i\},\\mathrm\{true\}\)are our\(i,0\)\(i,0\)and\(i,1\)\(i,1\)\. Its tail putsλ\\lambdafirst; Appendix[A\.2](https://arxiv.org/html/2610.41183#A1.SS2)puts it last\. This permutation preserves the symplectic product and weight\. The proof choosesz2=0z\_\{2\}=0in characteristic two andz2=1z\_\{2\}=1otherwise\.

Figure[6](https://arxiv.org/html/2610.41183#A4.F6)groups the certificate’s mathematical dependencies\. The dashed arrow is the standard stabilizer interpretation used in the paper; it is separate from the Lean\-checked algebraic fields\.

Coordinate mapΦ\\Phiand admissible parametersλ≠0\\lambda\\neq 0,1\+z2≠01\+z\_\{2\}\\neq 0,δ≠0\\delta\\neq 0InjectivitydimL=q\+2\\dim L=q\+2dim𝒞0=q\\dim\\mathcal\{C\}\_\{0\}=qGram formulaRadical identificationrad⁡\(L\)=Φ⁡\(𝒞0\)\\operatorname\{rad\}\(L\)=\\Phi\(\\mathcal\{C\}\_\{0\}\)Weight lower boundwts≥n−1\\operatorname\{wt\_\{s\}\}\\geq n\-1Equality attainedLean algebraic certificateNormalizerSideCertificateStandard stabilizer correspondence\[\[n,1,n−1;n−q−1\]\]q\[\[n,1,n\-1;n\-q\-1\]\]\_\{q\}Figure 6:Dependencies of the algebraic certificate\.
### D\.2Solution and formal verification

The solution above invokestheorem1\_exact\. Its proof body is reproduced verbatim below\. Forq≥3q\\geq 3, it choosesλ\\lambdaoutside two forbidden values\. In the binary branch, odd length permitsλ=1\\lambda=1\. Both branches invoketheorem1\_closed\_form, which assembles the certificate from the injectivity, Gram, radical, dimension and distance lemmas in the same source module\.

letz2:𝔽\\mathbb\{F\}:=if\(2:𝔽\\mathbb\{F\}\)=0then0else1

havehz2:1\+z2≠\\neq0:=by

dsimp\[z2\]

split\_ifswithhtwo

⋅\\cdotsimp

⋅\\cdotsimpa\[one\_add\_one\_eq\_two\]usinghtwo

rcaseshcasewithhlarge\|⟨\\langlehcard,hodd⟩\\rangle

⋅\\cdotobtain⟨\\langlelam,hlam,hδ\\deltabase⟩\\rangle:=exists\_nonzero\_add\_ne\_zerohlarge

\(\(\(2\*Fintype\.card𝔽\\mathbb\{F\}\+tail\-1:ℕ\\mathbb\{N\}\):𝔽\\mathbb\{F\}\)\)

havehδ\\delta:closedDelta\(tail:=tail\)z2lam≠\\neq0:=by

rw\[closedDelta\_eq\_cast\_length\_sub\_one\_add\]

exacthδ\\deltabase

exact⟨\\langlez2,lam,hlam,hz2,theorem1\_closed\_formz2lamhlamhz2hδ\\delta⟩\\rangle

⋅\\cdotletlam:𝔽\\mathbb\{F\}:=1

havehlam:lam≠\\neq0:=one\_ne\_zero

havehδ\\delta:closedDelta\(tail:=tail\)z2lam≠\\neq0:=by

rw\[closedDelta\_eq\_cast\_length\_sub\_one\_add\]

exactbinary\_odd\_delta\_ne\_zerohcardhodd

exact⟨\\langlez2,lam,hlam,hz2,theorem1\_closed\_formz2lamhlamhz2hδ\\delta⟩\\rangle

The proof and submitted solution use onlypropext,Quot\.soundandClassical\.choice\. Comparator confirms that the solution proves the specified goal under this axiom policy, and Lean’s kernel accepts the proof\([Lean Project, 2026](https://arxiv.org/html/2610.41183#bib.bib12)\)\. The[artifact](https://github.com/LeGenAI/llm_guided_EAQECC_search/tree/arxiv-v1)provides the pinned project and reproducible verification records\.