💻 logic

Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound

Este artículo cierra una brecha crítica de verificación en el límite mínimo de Kochen–Specker mediante la introducción de certificados de árbol de casos racionales exactos y dos verificadores independientes (uno en Python y otro probado formalmente en Lean 4) para verificar mediante máquinas la no embebibilidad geométrica de los 180 grafos distintos en la base de datos de bloqueo publicada, reemplazando así decisiones de Z3 no verificadas con teoremas verificados por el kernel mientras, simultáneamente, descubre y resuelve varios fallos y discrepancias ocultos en el flujo de trabajo de la prueba original.

Autores originales: Shayaan Siddique, Ibrahim Mian

Publicado 2026-07-29

📖 6 min de lectura🧠 Análisis profundo

Autores originales: Shayaan Siddique, Ibrahim Mian

✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagine que estás intentando construir una casa con bloques mágicos e invisibles. En el mundo de la física cuántica, estos bloques se llaman "vectores", y tienen una regla muy extraña: si dos bloques están en un ángulo recto perfecto entre sí, no pueden estar ambos "encendidos" al mismo tiempo. Este es el corazón del teorema de Kochen–Specker, una idea famosa que demuestra que el universo no es solo una máquina gigante y predecible donde cada parte tiene un interruptor secreto preestablecido. En cambio, sugiere que el acto de observar un sistema cuántico cambia su comportamiento.

Durante décadas, los físicos han estado jugando un juego de alto riesgo de "¿qué tan pequeño podemos hacer esto?". Quieren encontrar el conjunto más pequeño posible de estos bloques mágicos que cree una contradicción: una situación en la que las reglas del juego hagan imposible asignar estados de "encendido" o "apagado" sin romper las leyes de la física. El récord actual para el conjunto más pequeño conocido es de 31 bloques. Pero la gran pregunta es: ¿cuál es el mínimo absoluto? ¿Podría hacerse con 25? ¿24? ¿O incluso menos?

Para responder a esto, los investigadores utilizan potentes programas informáticos para generar miles de posibles disposiciones de bloques y luego intentan demostrar que ninguna de ellas puede existir realmente en nuestro mundo 3D. Es como un detective intentando demostrar que un sospechoso no pudo haber cometido un crimen al demostrar que su coartada es matemáticamente imposible. El problema es que, para la parte más difícil de esta demostración, los detectives anteriores tuvieron que confiar en un resolvedor informático de "caja negra". Le preguntaban al ordenador: "¿Es posible esta disposición?", y el ordenador decía: "No". Pero el ordenador no mostraba su procedimiento, dejando un pequeño vacío en la lógica donde un error podría esconderse.

Este artículo trata de cerrar ese vacío. Los autores, Shayaan Siddique e Ibrahim Mian, decidieron construir un nuevo tipo de "recibo" para cada una de las disposiciones imposibles. En lugar de simplemente confiar en el "No" del ordenador, crearon un certificado paso a paso y matemáticamente perfecto que cualquiera (o cualquier otro ordenador) puede revisar para verificar el resultado. No se limitaron a revisar uno o dos; revisaron 291 casos específicos (que representan 180 formas únicas) que forman la base del actual mejor límite inferior: 24 vectores.

Aquí explicamos cómo lo hicieron y qué encontraron:

El Recibo Mágico
Imagina que estás intentando demostrar que una forma específica hecha de bloques no puede existir. La forma antigua era preguntar a una IA superinteligente, que procesaría números y diría: "Imposible". La nueva forma, inventada en este artículo, es pedirle a la IA que escriba una historia. Esta historia es un "certificado de árbol de casos". Comienza con unos pocos bloques básicos y luego se ramifica como un libro de "elige tu propia aventura". En cada bifurcación del camino, la historia explica por qué un cierto camino conduce a una contradicción.

Los autores hicieron estas historias increíblemente rigurosas. Utilizaron "aritmética racional exacta", lo que significa que no usaron aproximaciones o conjeturas (como decir "esto es aproximadamente 3.14"). En su lugar, utilizaron fracciones perfectas. Si la historia dice que un número es cero, es exactamente cero, no "casi cero". Construyeron dos verificadores independientes —uno escrito en Python y otro en un lenguaje de prueba formal llamado Lean 4— para leer estas historias. Estos verificadores son como bibliotecarios estrictos que verifican cada uno de los pasos de la historia. Si la historia tiene un error tipográfico o un salto lógico, el bibliotecario la rechaza.

Las Sorpresas en la Biblioteca
Cuando los autores empezaron a leer los antiguos resultados de "caja negra" con sus nuevos y estrictos verificadores, encontraron algunas sorpresas que los investigadores originales habían pasado por alto porque confiaban demasiado en el ordenador.

La Trampa de la "Distintividad": El programa informático original asumía que cada uno de los bloques del conjunto debía ser único, incluso si no se tocaban. Los autores descubrieron que, para algunas de las formas, la única razón por la que eran "imposibles" era porque dos bloques terminaban siendo accidentalmente el mismo bloque. Si se relajaba esa regla, ¡la forma podría funcionar! Esto significaba que la prueba original dependía de una regla oculta sobre la "inyectividad" (asegurarse de que las cosas sean distintas) que no era obvia.
Callejones sin Salida Ocultos: El resolvedor informático a veces omitía casos "degenerados": escenarios extraños y límite donde las matemáticas se vuelven complicadas. Los nuevos certificados obligaron a los autores a escribir estos casos complicados explícitamente, demostrando que incluso en los rincones más extraños, las formas seguían sin poder existir.
Errores de Conteo: El artículo original afirmaba que quedaban 41 formas candidatas finales por comprobar. La nueva y rigurosa repetición de los datos mostró que en realidad había 43. Resulta que el recuento original fallaba por dos. Aunque esto no cambia el panorama general (el límite sigue siendo 24), demuestra que sin estos recibos perfectos, podríamos haber estado perdiendo dos piezas importantes del rompecabezas.

El Resultado
El artículo certifica con éxito que 180 formas geométricas distintas (extraídas de 291 líneas de datos) no pueden construirse en nuestro mundo 3D. Lo hicieron reemplazando las respuestas no verificadas de la "caja negra" con 291 certificados verificados y comprobables por máquina.

También demostraron que 42 de los 44 candidatos finales para el número mínimo de vectores pueden descartarse porque contienen una de estas formas imposibles certificadas en su interior. Esto deja solo 2 candidatos que aún no han sido probados, pero ahora sabemos exactamente cuáles son, y el camino para probarlos es claro.

Los autores no se limitaron a decir: "Creemos que es 24". Construyeron un sistema donde cada paso es un bucle lógico cerrado que puede ser verificado por un ordenador en aproximadamente medio segundo. Transformaron un argumento de "confía en nosotros" en un argumento de "muestra tu trabajo". Aunque la prueba final de que el mínimo absoluto es exactamente 24 (y no 23) todavía necesita algunas piezas más para ser ensamblada por completo, este artículo ha sentado la base verificada para la mitad geométrica del rompecabezas. Demuestra que, para la gran mayoría de los casos, el universo realmente prohíbe estas formas, y ahora tenemos los recibos para demostrarlo.

Resumen Técnico: Certificados Verificados por Máquina para la Mitad Geométrica del Límite Mínimo de Kochen–Specker

Planteamiento del Problema

El problema del límite mínimo de Kochen–Specker (KS) busca el número más pequeño $n$ de vectores no nulos en $\mathbb{R}^3$ , distintos por pares como rayos, tales que su grafo de ortogonalidad no admita un $\{0, 1\}$ -coloración donde cada par ortogonal contenga como máximo un $1$ y cada tríada ortogonal contenga exactamente un $1$. El límite inferior más conocido es $n \ge 24$ , establecido computacionalmente por Li et al. y Kirchweger et al.

Esta demostración consta de dos mitades:

Mitad Combinatoria: Una enumeración SAT libre de isomorfos de grafos candidatos hasta orden 23. Los resultados de insatisfacibilidad van acompañados de pruebas DRAT, que son verificables de forma independiente.
Mitad Geométrica: Una demostración de que cada grafo candidato enumerado no es embebible en $\mathbb{R}^3$ . Esta mitad depende del solver de aritmética real no lineal (NRA) de Z3 para determinar que ninguna asignación de vectores no nulos y con rayos distintos satisface las restricciones de ortogonalidad.

La brecha crítica identificada en este trabajo es que la mitad geométrica no produce objetos de prueba verificables. La cadena de confianza termina en el procedimiento de decisión de Z3 para una teoría $\exists\mathbb{R}$ -hard, lo que requiere que la comunidad acepte los veredictos de no embebibilidad por fe. Además, el flujo de trabajo publicado depende de "bases de datos de bloqueo" de subgrafos mínimos no embebibles, que también son derivados de Z3 y no verificados.

Metodología

Los autores introducen un marco para generar y verificar certificados de árbol de casos racionales exactos para la no embebibilidad real. La metodología reemplaza el opaco procedimiento de decisión de Z3 con un proceso de verificación algebraica transparente.

1. Estructura del Certificado
Un certificado es un objeto autónomo que comprende:

Anclaje y Propagación: Un paso de normalización (anclando una tríada ortogonal o una arista) seguido de un esquema de propagación que expresa todos los vectores de los vértices en términos de unos pocos parámetros utilizando productos vectoriales y parametrizaciones de planos.
Árbol de Casos: Una estructura de árbol donde los nodos internos representan divisiones basadas en:
- Factorización: $p = \prod f_k$ , verificada por expansión.
- Suma de Cuadrados (SOS): $p = \sum c_k m_k^2$ con $c_k \in \mathbb{Q}_{>0}$ , verificada por expansión.
Hojas: Las ramas se cierran mediante uno de cuatro mecanismos:
- Colisión de Inyectividad: Probar que dos vértices distintos se mapean a rayos paralelos.
- Colapso de Obligación: Mostrar que un polinomio no nulo requerido es idénticamente cero.
- Pertenencia al Ideal: Cofactores explícitos que prueban que un polinomio pertenece al ideal generado por las restricciones.
- Positividad de tipo Positivstellensatz: Un argumento generalizado que muestra que una suma de términos positivos (polinomios de inyectividad) es igual a una suma de cuadrados, lo que conduce a una contradicción en puntos reales.

2. Arquitectura de Verificación
El sistema emplea dos verificadores independientes que no comparten código con el generador de certificados:

Replay de Python Puro: Ejecuta la lógica del certificado utilizando aritmética racional exacta.
Verificador Total de Lean 4: Una función reflexiva Cert.check implementada en el asistente de pruebas Lean 4.
- Reducibilidad del Kernel: Para asegurar que el veredicto sea un teorema de kernel cerrado, los autores implementaron una capa de aritmética racional gcd-free (KRat) y recursión estructural con combustible (fuel). Esto permite que toda la computación sea reducida por el kernel de Lean sin reducción nativa ni axiomas personalizados.
- Cierre de Axiomas: El teorema de corrección depende únicamente de {propext, Classical.choice, Quot.sound}, evitando reducciones nativas no verificadas.

3. Teorema de Corrección
El teorema central, check_sound, establece que si check c = true, entonces no existe una realización del grafo. Una realización se define como un mapeo a $\mathbb{R}^3$ que satisface vectores no nulos, ortogonalidad en las aristas y distinción de rayos por pares (inyectividad) para todos los pares de vértices.

Contribuciones Clave

Certificados Racionales Exactos: La introducción de un formato de certificado que reemplaza las aproximaciones numéricas y los solvers opacos con aritmética racional exacta, factorizaciones polinómicas y descomposiciones SOS.
Cobertura Completa de la Base de Datos de Bloqueo: Certificación de las 291 líneas de código fuente (que representan 180 grafos distintos) de las listas de bloqueo de PhysicsCheck publicadas (órdenes 10–13), reemplazando cada veredicto de Z3 con un teorema verificado por máquina.
Doble Replay Independiente: Validación por dos verificadores distintos (Python y Lean) que rechazan 115 mutaciones adversarias (por ejemplo, coeficientes manipulados, ramas eliminadas) mientras aceptan certificados genuinos.
Hallazgos Impulsados por la Formalización: La formalización rigurosa reveló problemas específicos en el flujo de trabajo original:
- La Inyectividad es Fundamental: La codificación original de Z3 imponía la distinción de rayos por pares para todos los pares, no solo para los adyacentes. Varios grafos en la base de datos son no embebibles únicamente debido a esta restricción de inyectividad, un matiz invisible para los solvers geométricos estándar.
- Casos WLOG Ocultos: La parametrización de ortoplano utilizada en el flujo de trabajo original ocultaba casos degenerados (vectores paralelos) que deben ser descargados explícitamente mediante argumentos de inyectividad.
- Optimización Empírica: Se encontró que una optimización de "no colorabilidad" en el flujo de trabajo original era empírica en lugar de un lema fundamental.
- Conteos Reproducibles: Se encontró que el conteo publicado de candidatos finales de orden 23 (41) era irreproducible a partir de los artefactos; el conteo correcto es 43, con 42 descargados por los nuevos certificados de orden 13.

Resultados

Cobertura de Verificación: Los 180 grafos distintos en la base de datos de bloqueo ahora tienen teoremas de kernel cerrados que prueban su no embebibilidad.
Rendimiento: El costo de evaluación del kernel es de aproximadamente 0.5 segundos para grafos de orden 10/11/12 y 1.8 segundos para grafos de orden 13 en una laptop estándar. Toda la suite de verificación se ejecuta en minutos.
Impacto en el Límite: Los siete nuevos certificados de orden 13 descargan 42 de los 44 candidatos finales en la enumeración de orden 22/23 mediante monotonicidad de subgrafos verificada. Los dos candidatos restantes se rastrean como obligaciones explícitas legibles por máquina.
Robustez Adversaria: Ambos verificadores rechazaron con éxito las 115 mutaciones de certificados en la integración continua, demostrando que la lógica de verificación no es simplemente un replay de la salida del generador, sino un chequeo independiente genuino.

Significado

El artículo afirma cerrar la brecha de confianza para la mitad geométrica del límite mínimo de KS con respecto a la base de datos de bloqueo. Al convertir los veredictos de Z3 no verificados en teoremas de kernel cerrados, el trabajo asegura que la no embebibilidad de los subgrafos críticos ya no sea una cuestión de fe en un solver de caja negra.

Los autores enfatizan que el proceso de formalización en sí mismo fue una fuente primaria de valor, sacando a la luz supuestos ocultos (inyectividad), obligaciones de casos ocultos y discrepancias de datos que eran invisibles para el flujo de trabajo original. Aunque el artículo aún no compone un teorema completo de extremo a extremo verificado para $n \ge 24$ (debido a la escala de la enumeración SAT y las pruebas de canonicidad), establece la base geométrica verificada y proporciona un camino escalable a seguir. El trabajo demuestra que el razonamiento geométrico complejo en los fundamentos de la cuántica puede hacerse totalmente verificable por máquina con aritmética exacta y axiomas mínimos.