Physics as Code: From Scans to Theorems with ITP APIs in $SU(5)$ Model Building

Este artículo presenta una metodología basada en APIs dentro del demostrador de teoremas interactivo Lean para formalizar y verificar exhaustivamente la clasificación de espectros de carga viables en modelos $SU(5)$, transformando problemas combinatorios complejos en teoremas certificados reutilizables mediante el desarrollo de la infraestructura PhysLib.

Lo esencial

Imagina que los físicos teóricos son como arquitectos que intentan diseñar el edificio perfecto (un modelo del universo) usando un set de bloques de construcción infinitos. El problema es que hay tantos bloques y tantas formas de combinarlos que, si intentas probar cada combinación una por una (como un "barrido" o scan), te perderías en un laberinto sin salida. Además, si usas un algoritmo para adivinar las mejores combinaciones, nunca estarás 100% seguro de que no te has perdido ninguna solución oculta.

Este paper propone una solución radical: dejar de adivinar y empezar a demostrar.

Aquí tienes la explicación sencilla, usando analogías:

1. El Problema: El Laberinto de Bloques

En el mundo de la física (específicamente en la teoría de cuerdas y modelos como el SU(5)), los científicos buscan configuraciones de cargas eléctricas que permitan que el universo funcione como el nuestro (que exista la masa del quark top, que no haya explosiones de protones, etc.).

• El enfoque antiguo: Es como intentar encontrar una aguja en un pajar de un millón de pajitas. Haces un programa que revisa una por una. Si el pajar crece un poco más, tu programa tarda años. Peor aún, si el programa tiene un error, podrías descartar la aguja o creer que la encontraste cuando no es así.
• La limitación: No puedes confiar en una lista generada por computadora si no puedes probar matemáticamente que la lista es completa y correcta.

2. La Solución: El "Arquitecto Certificado" (Lean)

Los autores usan una herramienta llamada Lean, que es un "probador de teoremas interactivo". Piensa en Lean como un juez matemático infalible que no acepta "creo que funciona", sino que exige "demuéstralo paso a paso".

En lugar de escribir un script para buscar, escriben un manual de instrucciones (API) que define las reglas del juego de forma tan precisa que el juez puede verificar la lógica.

3. La Estrategia: Semillas y Crecimiento Controlado

En lugar de revisar todo el pajar, usan una estrategia inteligente basada en dos conceptos:

• Las "Semillas Mínimas" (Witnesses): Imagina que quieres construir una casa con una chimenea. En lugar de buscar entre todas las casas posibles, primero buscas la pieza más pequeña posible que ya tenga una chimenea funcional. En física, esto es el "mínimo espectro de carga" que permite la interacción del quark top.
• El "Crecimiento Controlado" (Completions): Una vez que tienes esa semilla (la chimenea), preguntas: "¿Cómo puedo agregar paredes, ventanas y un techo sin que la casa se derrumbe (sin violar las leyes de la física)?".
• La Magia: El paper demuestra matemáticamente que todas las casas viables (modelos físicos que funcionan) se pueden construir a partir de un número finito de estas "semillas" añadiendo piezas de forma controlada.

4. El Resultado: Un Mapa Certificado

Gracias a este método, los autores no solo obtienen una lista de modelos que funcionan, sino que demuestran que:

1. Ninguna solución válida se ha perdido: Si un modelo funciona, nuestro método lo encontrará.
2. Ninguna solución inválida se ha incluido: Si un modelo está en nuestra lista, es 100% seguro que cumple las reglas.

Es como si, en lugar de darte una lista de 100 restaurantes que parecen buenos, te dieran un mapa certificado que dice: "Estos son los únicos 100 restaurantes en la ciudad que cumplen con todas las normas de higiene y tienen comida deliciosa. No existen otros".

5. ¿Por qué es importante? (La Analogía del "Lego")

Antes, los físicos hacían "barridos" (scans) que eran como intentar armar un castillo de Lego probando millones de combinaciones al azar.

• Antes: "Probamos 1 millón de combinaciones y estas 50 parecen funcionar. ¡Genial!" (Pero ¿y si la combinación 1,000,001 también funcionaba y la computadora se quedó dormida?).
• Ahora: "Hemos probado la lógica de cómo se unen las piezas. Hemos demostrado que solo hay 50 formas de armar el castillo que no se caigan. Aquí está la lista de las 50. Es una verdad matemática, no una suposición".

En Resumen

Este paper es un paso gigante hacia la física con garantías. Convierte la búsqueda de modelos del universo de un "búsqueda a ciegas" en un proceso de construcción lógica y verificada.

Usan el software Lean para crear un "lenguaje de física" donde cada afirmación está respaldada por una prueba matemática. Esto permite a los científicos decir con total seguridad: "Hemos encontrado todos los modelos posibles que cumplen estas reglas, y no hay ninguno más".

Es como pasar de buscar una aguja en un pajar a tener un mapa que te dice exactamente dónde están las agujas y por qué no puede haber ninguna otra.

Resumen técnico

Resumen Técnico: Física como Código en la Construcción de Modelos SU(5)

1. El Problema: La Limitación de los Escaneos Exhaustivos

En la fenomenología de cuerdas y la física más allá del Modelo Estándar, un desafío recurrente es hacer afirmaciones globales y fiables sobre espacios de modelos acotados pero combinatoriamente masivos.

• Limitaciones actuales: Los métodos tradicionales se basan en escaneos exhaustivos (brute-force) o exploración estadística.
  • Los escaneos exhaustivos se vuelven opacos, dependientes de la implementación y difíciles de verificar cuando el espacio de búsqueda crece.
  • La exploración estadística no proporciona garantías teóricas ni certezas sobre la exhaustividad de los resultados.
• El objetivo: Formalizar el problema de construcción de modelos dentro de un Demostrador de Teoremas Interactivo (ITP), específicamente utilizando Lean, para transformar la búsqueda de modelos en un problema de clasificación con garantías matemáticas.

2. Metodología: APIs de Teoremas y el Enfoque de "Reducción Certificada"

Los autores proponen una metodología basada en APIs (Interfaces de Programación de Aplicaciones) dentro de Lean. En lugar de escribir scripts de escaneo ad hoc, se construye una infraestructura reutilizable que formaliza la lógica física.

• Estructura del Flujo de Trabajo:
  1. Objeto Central: Definición de un tipo de datos ChargeSpectrum (Espectro de Cargas) que representa las cargas de los sectores de Higgs y materia (representaciones $\mathbf{5}$ y $\mathbf{10}$ en SU(5)).
  2. Predicados Físicos: Definición de predicados formales para verificar condiciones físicas:
     • AllowsTerm: Permite un acoplamiento específico (ej. Yukawa del quark top).
     • IsPhenoConstrained: Evita operadores peligrosos (que violan simetrías o causan desintegración de protones).
     • IsComplete: Garantiza la presencia de todos los sectores necesarios (Higgs y materia).
  3. Estrategia de Reducción (Witness-and-Completion):
     • En lugar de escanear todo el espacio, el método identifica testigos mínimos (minimal witnesses): los espectros de carga más pequeños que permiten el acoplamiento deseado (ej. Yukawa del top).
     • Luego, se estudian completaciones controladas: cómo agregar sectores adicionales a estos testigos para formar modelos completos sin violar las restricciones físicas.
  4. Teorema de Reducción: Se demuestra que todo modelo viable y completo en el espacio acotado se genera a partir de un número finito de testigos mínimos mediante pasos de completación y cierre certificados.

3. Contribuciones Clave

• Desarrollo de PhysLib: Creación de una biblioteca de código abierto (PhysLib) que actúa como una capa semántica reutilizable para la física de altas energías. No es un script único, sino una infraestructura modular.
• Formalización de SU(5) con Simetrías Abelianas: Aplicación del método a un caso de estudio concreto: modelos SU(5) inspirados en la teoría F con simetrías U(1) adicionales.
• Clasificación Certificada: Demostración de que el conjunto de modelos viables no es solo una lista generada por un algoritmo, sino un conjunto definido por un teorema que garantiza:
  • Sonido (Soundness): Todo modelo en la lista es físicamente viable.
  • Completitud (Completeness): No hay modelos viables fuera de la lista generada.
• Separación entre Prueba y Cálculo: Distinción clara entre lo que se prueba (la estructura lógica y la exhaustividad) y lo que se computa (la enumeración finita de los resultados).

4. Resultados Principales

En el caso de estudio SU(5) con un conjunto de cargas acotado:

• Reducción del Espacio de Búsqueda: Se demostró que el espacio de modelos viables completos se genera a partir de un número finito de "testigos mínimos" del acoplamiento Yukawa del top.
• Resultados Numéricos: Para una configuración específica de codimensión uno (con cargas permitidas en el rango $\{-3, \dots, 3\}$):
  • El espacio de modelos acotado total tiene 1,048,576 combinaciones posibles.
  • El teorema reduce esto a una clase viable certificada de solo 102 espectros de carga.
• Verificación Formal: Se ha probado en Lean que la lista de 102 modelos es exhaustiva para las condiciones dadas (presencia de Yukawa del top, ausencia de operadores peligrosos, completitud de sectores).

5. Significado e Impacto Científico

• Cambio de Paradigma: El trabajo transforma la construcción de modelos de una "búsqueda ciega" a un proceso de clasificación teórica verificada. La exhaustividad no depende de la potencia de cálculo, sino de la validez del teorema de reducción.
• Reutilización y Escalabilidad: Al encapsular la lógica en una API (PhysLib), los físicos pueden extender estos resultados a espacios de carga más grandes o a otros modelos BSM (Beyond Standard Model) sin tener que reescribir la lógica fundamental.
• Interfaz con la IA y Futuro: La estructura formal proporciona un "terreno de juego" estable para herramientas de IA. Mientras que la IA puede proponer conjeturas o reducciones, el demostrador de teoremas garantiza que las definiciones y transformaciones centrales sean correctas, actuando como un filtro de verificación riguroso.
• Flujo de Trabajo Híbrido: Establece un flujo donde la reducción teórica (probada) alimenta la enumeración computable, la cual sirve como entrada certificada para análisis fenomenológicos posteriores (como datos de flujo, cancelación de anomalías, etc.).

En conclusión, este artículo demuestra que los demostradores de teoremas interactivos pueden utilizarse no solo para verificar resultados finales, sino para reformular problemas físicos complejos en lenguajes formales que permiten reducir la combinatoria mediante pruebas matemáticas, ofreciendo así garantías de exhaustividad que los métodos computacionales tradicionales no pueden proporcionar.