Formalizing building-up constructions of self-dual codes through isotropic lines in Lean

Título: Formalização de Construções de "Building-Up" de Códigos Auto-Duais através de Linhas Isotrópicas em Lean

1. Problema e Contexto

A teoria de códigos busca a construção e classificação de códigos lineares, com foco especial nos códigos auto-duais (onde o código é igual ao seu dual, $C = C^\perp$). Estes códigos têm conexões profundas com teoria de grupos, teoria de números e códigos de correção de erros quânticos.

O problema central abordado no artigo é a unificação e formalização rigorosa de duas abordagens distintas para a construção de códigos auto-duais:

1. Construção "Building-Up" (Kim): Um método indutivo que constrói um código auto-dual de comprimento $2n+2$ a partir de um código de comprimento $2n$, adicionando vetores específicos.
2. Construção via Símbolos de Hilbert (Chinburg-Zhang): Uma abordagem topológica e aritmética baseada na cohomologia de étale de variedades de dimensão 3 e anéis de inteiros $S$.

Existe uma lacuna na compreensão explícita de como essas duas visões se relacionam, especialmente no caso de campos finitos $q$-ários onde $q \equiv 1 \pmod 4$. Além disso, a implementação prática dessas construções muitas vezes carece de uma caracterização precisa das linhas geradoras, tratando-as como vetores "aleatórios" que satisfazem certas condições, em vez de derivá-las de uma estrutura geométrica subjacente.

2. Metodologia

Os autores utilizam uma abordagem tripla, combinando álgebra, geometria e verificação formal:

• Análise Algébrica e Geométrica:

  • Focam em campos finitos $F_q$ onde $q \equiv 1 \pmod 4$. Neste caso, $-1$ é um quadrado perfeito em $F_q$ (existe $c$ tal que $c^2 = -1$).
  • Demonstram que essa condição permite decompor o espaço euclidiano em um plano hiperbólico (gerado por uma linha isotrópica).
  • Reinterpretam a construção "building-up" de Kim não apenas como uma adição de vetores, mas como uma decomposição geométrica onde as linhas corretoras são organizadas por uma linha isotrópica no plano hiperbólico.
  • Estabelecem uma equivalência entre a redução "caixa" (boxed reduction) de Chinburg-Zhang (top-down) e a extensão de Kim (bottom-up), mostrando que são mecanismos inversos do mesmo processo de predecessor-sucessor.

• Generalização para o Caso $q$-ário:

  • Desenvolvem uma versão $q$-ária da forma "caixa" (split boxed form). Diferentemente do caso binário, onde a última coluna é fixa, no caso $q$-ário as entradas fora da diagonal são múltiplos de uma linha isotrópica $(1, c)$.
  • Derivam fórmulas explícitas para os vetores de extensão e condições de ortogonalidade.

• Formalização em Lean 4:

  • Implementam a teoria algébrica central no assistente de prova Lean 4, utilizando a biblioteca Mathlib.
  • O desenvolvimento formaliza 256 teoremas em um único arquivo (BuildingUpFormalization.lean) com zero "sorry" (sem lacunas de prova), cobrindo a interface auto-dual/Lagrangiana, a decomposição hiperbólica e as teoremas de reconstrução.

3. Contribuições Principais

1. Unificação Teórica (Teorema 3.4):

   • Prova que a construção de Kim (binária) e a redução de Chinburg-Zhang são a mesma mecânica vista de direções opostas. A redução de Chinburg-Zhang é uma redução Lagrangiana "top-down", enquanto Kim é uma extensão "bottom-up".

2. Construção Generalizada $q$-ária (Teoremas 3.9 e 3.12):

   • Apresenta uma construção "building-up" geral para códigos auto-duais sobre $F_q$ ($q \equiv 1 \pmod 4$).
   • Introduz a forma "split boxed", onde a estrutura do gerador do código é rigidamente determinada por uma linha isotrópica $(1, c)$. Isso fornece uma caracterização precisa das linhas corretoras, eliminando a ambiguidade de vetores aleatórios.

3. Formalização Rigorosa:

   • O trabalho fornece a primeira formalização completa da teoria de construção de códigos auto-duais baseada em geometria hiperbólica e cohomologia, validando a lógica algébrica subjacente através de prova assistida por computador.

4. Construção de Códigos Ótimos:

   • Utiliza a nova estrutura "split boxed" para construir explicitamente códigos auto-duais ótimos (que atingem o limite de distância mínima) sobre $GF(5)$e$GF(13)$.

4. Resultados Experimentais e Exemplos

Os autores aplicaram a construção "split boxed" para gerar códigos específicos com parâmetros ótimos:

• Sobre $GF(5)$:
  • Código auto-dual $[6, 3, 4]$: Ótimo (atinge o limite de Singleton).
  • Código auto-dual $[8, 4, 4]$: Ótimo.
• Sobre $GF(13)$:
  • Código auto-dual $[8, 4, 5]$: Ótimo entre todos os códigos lineares (não apenas auto-duais).
  • Código auto-dual $[10, 5, 6]$: Ótimo.
  • Código auto-dual $[12, 6, 6]$: Exato.

Para cada caso, as matrizes geradoras foram construídas explicitamente usando as fórmulas derivadas, e a otimalidade foi verificada através de buscas exaustivas (computacionais externas) e limites teóricos (como o limite de Griesmer e Singleton).

5. Significado e Impacto

• Teórico: O papel esclarece a conexão profunda entre a teoria de códigos, a geometria de espaços quadráticos (planos hiperbólicos) e a cohomologia de étale. Mostra que a condição $q \equiv 1 \pmod 4$ (existência de raiz quadrada de -1) é o insumo algébrico unificador que permite a decomposição Lagrangiana e a construção recursiva.
• Prático: A "forma split boxed" oferece um método sistemático e eficiente para construir códigos auto-duais de comprimento par, superando as limitações de métodos anteriores que não eram universais ou eficientes para comprimentos maiores.
• Computacional/Formal: A formalização em Lean serve como uma base verificada para futuras pesquisas em teoria de códigos. Ela garante que as propriedades algébricas usadas para gerar códigos são matematicamente corretas, separando a prova teórica da busca computacional por parâmetros ótimos.

Em resumo, o artigo fornece uma ponte rigorosa entre a teoria abstrata de cohomologia e a construção prática de códigos, validada matematicamente por um assistente de prova, e resulta em novos códigos ótimos para aplicações em comunicação confiável e correção de erros quânticos.