← All papers
First page of Uniform Three-Fold Product Expansion of Algebraic-Geometry Codes over a Fixed Field

Uniform Three-Fold Product Expansion of Algebraic-Geometry Codes over a Fixed Field

Cassie Ding, Min-Hsiu Hsieh

cs.IT Nov 5, 2026 · v1 math.AG
The main theorems, including uniform three-fold product expansion and the rate/distance bounds, are formally verified in Lean 4 with Mathlib and a Riemann–Roch library.
A collection of classical codes $C_1,\dots,C_m$ has product expansion if every low-weight word in the sum of their extensions to the product space can be written as a sum of words supported on few lines, each line being a codeword of the corresponding $C_i$. For $m=2$ product expansion is equivalent to robust testability of the tensor code, while for $m\ge 3$ it is strictly stronger; it is the hypothesis on the local codes behind recent constructions of good quantum LDPC codes, good quantum locally testable codes, and quantum codes with transversal non-Clifford gates. No explicit family over a fixed field was previously known to achieve constant rate, linear distance for both the code and its dual, and 3-fold product expansion at growing length. We prove that for the one-point evaluation codes $C_i$ of length $N_i=728\cdot27^{\,i-1}$ and pole order $\lfloor N_i/5\rfloor$ on the Garcia–Stichtenoth tower over $\mathbb{F}_{729}$, the triple $(C_i,C_i,C_i)$ has product expansion with a constant independent of $i$. The dual codes $C_i^\perp$ then form an explicit fixed-field family of rate tending to $109/130$ and relative distance at least $8/65$. The proof is geometric: we view the words of the sum code as arrays on the product of three copies of the $i$-th curve of the tower, where the parity checks are sections of a line bundle. An exact generation theorem describes the sum-code words supported on the grid footprint of a suitable divisor. A support-localisation argument then shows that every low-weight array lies on such a divisor, after deleting a small number of coordinates. We also give a sufficient criterion for three-fold product expansion in terms of degree and genus ratios, yielding explicit families over every non-prime finite field of order at least $512$. The principal conclusions have been formally verified in Lean 4.

Recent constructions of good quantum LDPC codes, quantum locally testable codes, and codes with transversal non-Clifford gates require local classical codes with three-fold product expansion. No explicit fixed-field family was known with constant rate, linear distance for both the code and its dual, and 3-fold product expansion at growing length.

The local codes are one-point AG evaluation codes on the Garcia–Stichtenoth tower over F_729. Sum-code words are viewed as arrays on the triple product of a curve, and parity checks are identified with sections of a line bundle. An exact generation theorem on carrier divisors is combined with a support-localisation argument that places low-weight arrays on such divisors after puncturing. The principal conclusions are machine-checked in a Lean 4 development pinned to Mathlib and a Riemann–Roch library.

The triple (C_i,C_i,C_i) has product expansion with a constant independent of i. The duals give an explicit fixed-field family with rate tending to 109/130 and relative distance at least 8/65. A degree/genus-ratio criterion yields families over every non-prime finite field of order at least 512, and the Lean endpoints use only the standard axioms.