Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4

Resumo Técnico: Fundações Formais e Certificados de Prova para Códigos de Cobertura $q$-ários em Lean 4

Enunciado do Problema
Códigos de cobertura em espaços de Hamming finitos buscam o menor conjunto de palavras (palavras-chave) tal que a união de suas bolas de Hamming de raio $r$ cubra todo o espaço $A^n$. A quantidade central é o número de cobertura $q$-ário $K_q(n,r)$, definido como o tamanho mínimo de tal código. Embora a definição seja elementar, determinar valores exatos ou limites estreitos para $K_q(n,r)$ normalmente depende de uma mistura de construções explícitas, argumentos de contagem, relações recursivas e buscas computacionais. Um desafio significativo no campo é que afirmações exatas $K_q(n,r) = k$ requerem dois componentes independentes: uma construção explícita provando um limite superior ($K_q(n,r) \le k$) e uma prova de que nenhum código menor existe (um limite inferior $K_q(n,r) \ge k$). Esses componentes frequentemente originam-se de fontes díspares, tornando a verificação de valores exatos difícil de auditar.

Metodologia
O artigo apresenta uma formalização da teoria elementar de códigos de cobertura no provador de teoremas Lean 4. A metodologia é caracterizada por três escolhas de design centrais:

1. Representação de Palavras: As palavras são modeladas como funções dependentes de um tipo de coordenada para um tipo de alfabeto. O espaço de Hamming $q$-ário geral de comprimento $n$ é representado como Fin n → Fin q. Essa representação funcional preserva uma interface geral para tipos de coordenadas abstratos ao mesmo tempo em que simplifica a especialização $q$-ária.
2. Predicados Estilo Certificado: Em vez de definir $K_q(n,r)$ como uma função de minimização não computável, a formalização utiliza predicados lógicos para representar asserções sobre números de cobertura.
   • KUpper r k: Afirma a existência de um código de cobertura finito de tamanho no máximo $k$ (limite superior).
   • KLower r k: Afirma que todo código de cobertura finito tem tamanho pelo menos $k$ (limite inferior).
   • KSpec r k: Combina ambos para afirmar a exatidão ($K_q(n,r) = k$).
     Este método modular permite que limites superiores e inferiores de diferentes fontes sejam montados independentemente.
3. Banco de Dados de Prova Carregada: O artigo implementa um banco de dados onde os limites armazenados não são meramente valores numéricos, mas objetos "com prova carregada". Cada entrada inclui um traço de derivação. Replay deste traço no Lean reconstrói uma prova formal do predicado correspondente QaryKUpper ou QaryKLower. O sistema distingue entre teoremas matemáticos escritos à mão (verificados pelo kernel) e dados gerados (produtores não confiáveis cujo output é validado via replay de traço).

Contribuições Principais
O artigo estabelece uma fundação reutilizável e auditável para certificados de códigos de cobertura verificados por máquina. Suas contribuições específicas incluem:

• Infraestrutura Formal: Um framework completo em Lean 4 para espaços de Hamming finitos, distância de Hamming, bolas fechadas e predicados de cobertura, lidando com casos de borda (ex: $q=0$, $n=0$, $r \ge n$) rigorosamente dentro das definições, em vez de como convenções informais.
• Resultados Analíticos: Provas formais da fórmula do volume da bola de Hamming $q$-ária e do clássico limite inferior de cobertura de esfera. O limite de cobertura de esfera é encapsulado como uma função computável sphereLower que gera certificados de limite inferior certificados.
• Teoremas Estruturais: Formalização de casos exatos elementares (ex: $K_q(n,0) = q^n$, $K_q(n, n-1) = q$) e construções estruturais, incluindo um teorema de cobertura de produto e várias relações de vizinhança (perfuração, prolongamento, projeção de alfabeto e concatenação) que transportam limites entre triplas de parâmetros.
• Estudo de Caso (Van Laarhoven et al.): Um fluxo de trabalho de ponta a ponta demonstrando a formalização de códigos explícitos publicados. Os autores transcreveram códigos de cobertura de um artigo de 1989 (Van Laarhoven et al.) para o Lean, codificando-os como arrays compactados para evitar limites de elaboração. O sistema verificou a propriedade de cobertura e a cardinalidade, produzindo certificados de limite superior verificados por máquina para $K_3(6,1) \le 73$, $K_3(7,1) \le 186$ e $K_3(8,1) \le 486$.
• Implementação de Banco de Dados: Um banco de dados de prova carregada contendo 52.822 entradas para parâmetros $0 \le q \le 21$, $0 \le n \le 48$ e $0 \le r \le 48$. Este banco de dados inclui certificados exatos para casos pequenos (ex: $K_2(5,1)=7$, $K_3(3,1)=5$) e intervalos derivados de replay de traço.

Resultados
A formalização verifica com sucesso:

• A fórmula do volume da bola $q$-ária e o limite inferior de cobertura de esfera.
• Valores exatos elementares como $K_2(5,1)=7$, $K_2(6,2)=4$, $K_3(3,1)=5$ e $K_4(3,1)=8$.
• Limites superiores para o problema ternário de "football-pool" derivados de códigos explícitos, especificamente $K_3(6,1) \le 73$, $K_3(7,1) \le 186$ e $K_3(8,1) \le 486$.
• Uma construção cíclica de dois blocos uniforme provando $K_q(3,1) \le \lceil q^2/2 \rceil$.

O processo de fechamento do banco de dados propagou com sucesso estas fontes primitivas através de regras de relação certificadas para gerar uma tabela consistente de limites. O sistema suporta dois modos de prova: um "modo kernel" usando decide padrão para garantias de replay mais fortes e um "modo nativo" usando o avaliador compilado do Lean para desenvolvimento mais rápido, com fronteiras de confiança claras definidas para cada um.

Significância e Alegações
O artigo afirma explicitamente que sua contribuição primária não é a descoberta de novos limites recordistas ou a reprodução de tabelas da literatura existente. Em vez disso, sua significância reside em fornecer uma interface formal e uma fundação auditável para certificados de códigos de cobertura.

O trabalho faz a ponte entre a literatura clássica de códigos de cobertura e futuros certificados computacionais. Ao separar testemunhas de limite superior, argumentos de limite inferior e predicados de exatidão, a formalização permite que resultados de construções explícitas, contagem combinatória e (potencialmente) futuros resolvedores de SAT ou programação inteira sejam verificados e compostos dentro de um único framework confiável. A natureza de "prova carregada" do banco de dados garante que cada limite relatado possa ser rastreado até uma prova verificada por máquina, abordando os desafios de reprodutibilidade e verificação inerentes ao campo. O artigo posiciona-se como um passo fundamental para um futuro onde os resultados de busca computacional possam ser integrados perfeitamente em bibliotecas matemáticas formais.