High-Rate Quantum Codes with Proven Distance and Low-Weight Measurements

Resumo Técnico: Códigos Quânticos de Alta Taxa com Distância Provada e Medições de Baixo Peso

Enunciado do Problema
O artigo aborda o compromisso fundamental no erro quântico entre três parâmetros críticos: a taxa de codificação (número de qubits lógicos protegidos em relação aos qubits de dados), a distância do código (peso mínimo de um erro lógico indetectável) e o peso da medição (o número de qubits de dados tocados por um único operador medido). Embora os códigos de subsistema ofereçam um mecanismo para substituir medições de estabilizadores pesados por medições de gauge não comutantes mais leves, determinar a distância exata de tais códigos — especificamente a distância "vestida" (dressed), que considera a multiplicação por operadores de gauge) — muitas vezes exige buscas numéricas ou carece de provas rigorosas para famílias gerais. Os autores buscam uma construção que forneça parâmetros explícitos e provados para códigos de alta taxa com medições de baixo peso em grades retangulares.

Metodologia
Os autores estudam uma família de códigos de subsistema quântico, denotados como RLG($q_1, \dots, q_L$), definidos em grades de coordenadas retangulares de dimensão $L$ com comprimentos de lado pares $q_i \ge 4$.

• Construção: O código é definido pela medição de operadores de gauge de "linha de coordenada". Para cada eixo $i$, operadores que atuam como $X$ ou $Z$ ao longo de cada linha paralela a esse eixo estão incluídos no grupo de gauge.
• Estrutura Algébrica: A análise utiliza a descrição simplética binária de operadores de Pauli. O código é do tipo Calderbank–Shor–Steane (CSS), onde o grupo de gauge é gerado por operadores $X$ puros e $Z$ puros. Os autores empregam cálculos de produto tensorial sobre $\mathbb{F}_2$ para determinar os postos dos grupos de gauge e estabilizador.
• Verificação Formal: Uma parte significativa da metodologia envolve a verificação formal usando Lean, um provador de teoremas interativo. Os autores fornecem módulos Lean (ex: RLG.lean, GridLines.lean) que definem a estrutura do código e provam formalmente os limites inferiores de distância via indução no número de eixos. Essa abordagem evita buscas numéricas de distância para o caso geral.
• Otimização: Para um orçamento fixo de qubits de dados (especificamente $N \le 10.000$), os autores realizam uma enumeração finita exata de tuplas retangulares pares para identificar a fronteira de Pareto entre a taxa de codificação e o peso máximo de medição para distâncias específicas ($D=16, 32, 64$).

Principais Contribuições

1. Fórmulas de Parâmetros Exatas: O artigo deriva expressões de forma fechada para o número de qubits de dados ($N$), qubits lógicos protegidos ($K$), qubits de gauge ($g$) e distância vestida ($D$) para qualquer tupla válida de comprimentos de lado:
   • $N = \prod q_i$
   • $K = \prod (q_i - 2)$
   • $D = 2^L$ (onde $L$ é o número de eixos)
   • O peso máximo de medição é $w = \max_i q_i$.
2. Distância Vestida Provada: Ao contrário de muitas análises de códigos de subsistema que dependem de heurísticas ou verificações numéricas, este trabalho fornece uma prova rigorosa de que a distância vestida é exatamente $2^L$. A prova demonstra que qualquer operador lógico não trivial (mesmo após a multiplicação por operadores de gauge) deve ter um tamanho de suporte de pelo menos $2^L$.
3. Distância Bare vs. Dressed: Os autores provam que, para esta família, a distância "bare" (peso mínimo de um operador lógico que comuta com todos os gauges) também é $2^L$, coincidindo com a distância vestida.
4. Análise de Peso de Estabilizador: O artigo estabelece que, embora os operadores de gauge medidos tenham baixo peso ($w$), os estabilizadores não identitários (que são produtos de linhas de gauge) têm um peso mínimo de $2^{L-1} \min_i q_i$. Isso destaca como a liberdade de gauge reduz o peso dos operadores diretamente medidos, mas não elimina as restrições pesadas de estabilizador inerentes à estrutura do código.
5. Resultados de Otimização Finita: Sob um orçamento de 10.000 qubits de dados, os autores identificam as configurações de código otimizadas:
   • Distância 16: Um código com 10.000 qubits de dados protege 4.096 qubits lógicos ($K/N \approx 41\%$) usando medições de peso 10.
   • Distância 32: Um código com 7.776 qubits de dados protege 1.024 qubits lógicos ($K/N \approx 13,2\%$) usando medições de peso 6.
   • Distância 64: Um código com 9.216 qubits de dados protege 256 qubits lógicos ($K/N \approx 2,8\%$) usando medições de peso 6.

Resultados e Alegações
O artigo afirma fornecer um "compromisso completo" entre a taxa de codificação e o peso da medição para esta família específica de códigos nas distâncias 16, 32 e 64. Os resultados mostram que altas taxas são alcançáveis em distâncias moderadas (ex: $D=16$) com pesos de medição relativamente baixos. No entanto, conforme a distância aumenta, a taxa cai significativamente, e o número de eixos ($L$) deve aumentar, o que inerentemente aumenta a distância ($D=2^L$), mas reduz a taxa para um $N$ fixo.

Os autores declaram explicitamente que estes resultados dizem respeito aos parâmetros estáticos da família de códigos. Eles não alegam estabelecer a distância de circuito tolerante a falhas, taxas de erro lógico ou desempenho específico de decodificação sob ruído de nível de circuito. O artigo observa que, embora a construção estenda códigos de "muitos-hipercubos", trata todas as tuplas retangulares pares em uma descrição algébrica unificada, permitindo comprimentos de lado mistos que foram menos explorados anteriormente.

Significância
A significância do trabalho reside na sua capacidade de separar a escolha da distância do problema de otimização finita restante. Ao provar que a distância depende apenas do número de eixos ($L$), enquanto a taxa e o peso de medição dependem dos comprimentos de lado ($q_i$), os autores fornecem um espaço de design claro para selecionar códigos baseados em restrições de hardware (peso de medição) e requisitos lógicos (distância e taxa).

O artigo enfatiza que a "liberdade de gauge" permite que a informação carregada por estabilizadores pesados seja acessada via medições mais leves, mas também esclarece o custo: as próprias restrições de estabilizador permanecem pesadas (peso $\ge 2^{L-1} \min q_i$). Consequentemente, os autores observam que esta família não é uma família de estabilizadores QLDPC convencional (com taxa constante e distância linear com pesos limitados) no sentido assintótico, mas sim uma família que oferece parâmetros finitos exatos e um cenário de otimização específico. A inclusão da formalização em Lean garante que as provas de distância sejam verificadas por máquina, proporcionando um alto grau de rigor para os parâmetros reivindicados sem depender de busca numérica.