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

Resumen Técnico: Fundamentos Formales y Certificados de Prueba para Códigos de Cobertura $q$-arios en Lean 4

Planteamiento del Problema
Los códigos de cobertura en espacios de Hamming finitos buscan el conjunto más pequeño de palabras (palabras clave o codewords) tal que la unión de sus bolas de Hamming de radio $r$ cubra todo el espacio $A^n$. La cantidad central es el número de cobertura $q$-ario $K_q(n,r)$, definido como el tamaño mínimo de tal código. Si bien la definición es elemental, determinar valores exactos o cotas ajustadas para $K_q(n,r)$ suele depender de una mezcla de construcciones explícitas, argumentos de conteo, relaciones recursivas y búsquedas computacionales. Un desafío significativo en este campo es que las afirmaciones exactas $K_q(n,r) = k$ requieren dos componentes independientes: una construcción explícita que pruebe un límite superior ($K_q(n,r) \le k$) y una prueba de que no existe un código más pequeño (un límite inferior $K_q(n,r) \ge k$). Estos componentes a menudo provienen de fuentes dispares, lo que dificulta la verificación de los valores exactos.

Metodología
El artículo presenta una formalización de la teoría elemental de los códigos de cobertura en el probador de teoremas Lean 4. La metodología se caracteriza por tres decisiones de diseño fundamentales:

1. Representación de Palabras: Las palabras se modelan como funciones dependientes de un tipo de coordenada a un tipo de alfabeto. El espacio de Hamming $q$-ario general de longitud $n$ se representa como Fin n → Fin q. Esta representación funcional preserva una interfaz general para tipos de coordenadas abstractos al tiempo que simplifica la especialización $q$-aria.
2. Predicados Estilo Certificado: En lugar de definir $K_q(n,r)$ como una función de minimización no computable, la formalización utiliza predicados lógicos para representar aserciones sobre los números de cobertura.
   • KUpper r k: Asevera la existencia de un código de cobertura finito de tamaño máximo $k$ (límite superior).
   • KLower r k: Asevera que todo código de cobertura finito tiene un tamaño de al menos $k$ (límite inferior).
   • KSpec r k: Combina ambos para aseverar la exactitud ($K_q(n,r) = k$).
     Este enfoque modular permite que los límites superiores e inferiores de diferentes fuentes se ensamblen de forma independiente.
3. Base de Datos con Carga de Prueba: El artículo implementa una base de datos donde las cotas almacenadas no son meramente valores numéricos, sino objetos con "carga de prueba" (proof-carrying). Cada entrada incluye un rastro de derivación. Reproducir este rastro en Lean reconstruye una prueba formal del predicado QaryKUpper o QaryKLower correspondiente. El sistema distingue entre teoremas matemáticos escritos a mano (verificados por el núcleo o kernel) y datos generados (productores no confiables cuyo resultado es validado mediante la reproducción del rastro).

Contribuciones Clave
El artículo establece una base reutilizable y auditable para certificados de códigos de cobertura verificados por máquina. Sus contribuciones específicas incluyen:

• Infraestructura Formal: Un marco completo en Lean 4 para espacios de Hamming finitos, distancia de Hamming, bolas cerradas y predicados de cobertura, manejando casos de borde (por ejemplo, $q=0$, $n=0$, $r \ge n$) de manera rigurosa dentro de las definiciones en lugar de como convenciones informales.
• Resultados Analíticos: Pruebas formales de la fórmula del volumen de la bola de Hamming $q$-aria y del clásico límite inferior de cobertura de la esfera. El límite de cobertura de la esfera se encapsula como una función computable sphereLower que genera certificados de límite inferior certificados.
• Teoremas Estructurales: Formalización de casos exactos elementales (por ejemplo, $K_q(n,0) = q^n$, $K_q(n, n-1) = q$) y construcciones estructurales, incluyendo un teorema de cobertura de producto y diversas relaciones de vecindad (puncionamiento, alargamiento, proyección de alfabeto y concatenación) que transportan cotas entre triples de parámetros.
• Estudio de Caso (Van Laarhoven et al.): Un flujo de trabajo de extremo a extremo que demuestra la formalización de códigos explícitos publicados. Los autores transcribieron códigos de cobertura de un artículo de 1989 (Van Laarhoven et al.) a Lean, codificándolos como arreglos empaquetados para evitar los límites de elaboración. El sistema verificó la propiedad de cobertura y la cardinalidad, produciendo certificados de límite superior verificados por máquina para $K_3(6,1) \le 73$, $K_3(7,1) \le 186$ y $K_3(8,1) \le 486$.
• Implementación de Base de Datos: Una base de datos con carga de prueba que contiene 52,822 entradas para parámetros $0 \le q \le 21$, $0 \le n \le 48$ y $0 \le r \le 48$. Esta base de datos incluye certificados exactos para casos pequeños (por ejemplo, $K_2(5,1)=7$, $K_3(3,1)=5$) e intervalos derivados de la reproducción de rastros.

Resultados
La formalización verifica con éxito:

• La fórmula del volumen de la bola $q$-aria y el límite inferior de cobertura de la esfera.
• Valores exactos elementales tales como $K_2(5,1)=7$, $K_2(6,2)=4$, $K_3(3,1)=5$ y $K_4(3,1)=8$.
• Límites superiores para el problema ternario de las apuestas de fútbol (football-pool problem) derivados de códigos explícitos, específicamente $K_3(6,1) \le 73$, $K_3(7,1) \le 186$ y $K_3(8,1) \le 486$.
• Una construcción cíclica de dos bloques uniforme que prueba $K_q(3,1) \le \lceil q^2/2 \rceil$.

El proceso de cierre de la base de datos propagó con éxito estas fuentes primitivas a través de reglas de relación certificadas para generar una tabla consistente de cotas. El sistema soporta dos modos de prueba: un "modo de núcleo" utilizando decide estándar para garantías de reproducción más fuertes, y un "modo nativo" utilizando el evaluador compilado de Lean para un desarrollo más rápido, con fronteras de confianza claras definidas para cada uno.

Significado y Reivindicaciones
El artículo establece explícitamente que su contribución principal no es el descubrimiento de nuevos límites que rompan récords o la reproducción de tablas de la literatura existente. En cambio, su importancia radica en proporcionar una interfaz formal y una base auditable para los certificados de códigos de cobertura.

El trabajo cierra la brecha entre la literatura clásica de códigos de cobertura y los futuros certificados computacionales. Al separar los testigos de límites superiores, los argumentos de límites inferiores y los predicados de exactitud, la formalización permite que los resultados de construcciones explícitas, conteo combinatorio y (potencialmente) futuros resolvedores de SAT o de programación entera sean verificados y compuestos dentro de un único marco de confianza. La naturaleza de "carga de prueba" de la base de datos asegura que cada límite reportado pueda rastrearse hasta una prueba verificada por máquina, abordando los desafíos de reproducibilidad y verificación inherentes al campo. El artículo se posiciona como un paso fundacional hacia un futuro donde los resultados de búsqueda computacional puedan integrarse sin problemas en las librerías matemáticas formales.