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

This paper introduces an API-based methodology using the Lean interactive theorem prover to formally verify and classify viable charge spectra in $SU(5)$ model building, transforming combinatorially complex searches into rigorously proven, reusable theorems rather than relying on opaque exhaustive scans.

The Gist

Imagine you are a master chef trying to create the perfect recipe for a new dish. You have a pantry full of ingredients (charges, particles, symmetries), and you need to find every single combination that results in a delicious, safe meal (a viable physics model) while avoiding toxic ingredients (dangerous operators).

In the past, physicists tried to solve this by brute force: they would mix every possible combination of ingredients in a giant computer simulation, taste them one by one, and keep the ones that worked.

The Problem:
The number of combinations is so huge (like trying every possible arrangement of a deck of cards) that the computer gets overwhelmed. Even if the computer finds a "good" recipe, you can never be 100% sure it didn't miss a better one, or that it didn't accidentally include a toxic ingredient because of a coding error. It's like searching a massive library for a specific book by reading every page of every book; you might find the right one, but you can't prove you didn't miss another.

The Solution: "Physics as Code"
This paper proposes a smarter way. Instead of just searching, the authors use a Interactive Theorem Prover (ITP). Think of this as a super-strict, unblinking librarian who doesn't just find books but proves mathematically that the list of books you have is the only possible list.

Here is how they did it, using simple analogies:

1. The "Seed" Strategy (Minimal Witnesses)

Instead of looking at the whole library at once, the authors realized you don't need to start with a full meal. You just need the core ingredient that makes the dish work.

• The Analogy: Imagine you want to make a cake. You don't need to check every possible cake in the world. You just need to find the smallest, simplest "seed" that proves a cake can exist (e.g., flour + eggs + sugar).
• In the Paper: They found the "Minimal Top-Yukawa Witnesses." These are the smallest, simplest sets of particle charges that allow the "top quark" (a heavy particle) to exist. If a model doesn't have this tiny seed, it's automatically disqualified.

2. The "Growth" Strategy (Controlled Completions)

Once you have the seed, you don't just guess what to add next. You follow a strict set of rules for how the cake can grow.

• The Analogy: You take your seed (flour/eggs) and ask: "What can I add safely?" You can add milk, but you can't add poison. You can add vanilla, but you can't add sand. The theorem prover acts as a rule-enforcing gardener. It says, "Yes, you can grow this branch, but only if it stays within the fence of safety rules."
• In the Paper: They proved that any valid, complete model is just one of these "seeds" grown in a specific, controlled way. They didn't just scan for models; they proved that every possible valid model must come from one of these seeds.

3. The "Certified List" (The Theorem)

This is the magic part.

• The Old Way: "Here is a list of 100 recipes the computer found. I think they are good." (You have to trust the computer didn't make a mistake).
• The New Way: "Here is a list of 100 recipes. We have mathematically proven that:
  1. Every recipe on this list is safe and complete.
  2. There are absolutely no other safe recipes that we missed.
  3. If a recipe isn't on this list, it is impossible for it to work."

Why This Matters

The authors built a reusable "API" (a set of tools) inside a programming language called Lean.

• Think of it like a Lego set: Instead of building a castle from scratch every time, they built a sturdy, certified foundation. Now, other scientists can snap new pieces (like new physics rules or different particle types) onto this foundation without having to rebuild the whole castle or worry that the foundation will collapse.

The Result

In their specific example (building a universe based on SU(5) symmetry):

• The computer had to check over 1 million possible combinations.
• Using their "seed and growth" method, they proved that only 102 of those combinations are actually valid.
• Crucially, they didn't just find those 102; they proved that the other 999,975 are impossible.

Summary

This paper is about moving from guessing and checking to proving and knowing.
They turned a chaotic, overwhelming search for the "perfect universe" into a structured, step-by-step construction process. They proved that if you start with the right tiny seeds and follow the rules, you will find all the possible universes, and only the possible ones. It turns a "maybe" into a "definitely."

Technical Summary

1. Problem Statement

The paper addresses a fundamental challenge in theoretical physics, specifically in string phenomenology and Beyond-the-Standard-Model (BSM) model building: how to make reliable global statements about bounded but combinatorially large model spaces.

• The Limitation of Current Methods: Traditional approaches rely on exhaustive brute-force scans or statistical sampling.
  • Scans: Become opaque and impractical as the search space grows. Their correctness depends heavily on implementation details (e.g., pruning logic, symmetry handling), making it difficult to prove that all viable models have been found or that no viable models were missed.
  • Sampling: Does not provide theorem-backed guarantees regarding the completeness of the classification.
• The Specific Case: The authors focus on SU(5) Grand Unified Theory (GUT) model building with additional Abelian ($U(1)$) symmetries, a setting common in F-theory constructions. The goal is to classify charge spectra that:
  1. Admit a top-quark Yukawa coupling.
  2. Avoid a specific set of "dangerous" operators (e.g., proton decay, R-parity violation).
  3. Satisfy a minimal completeness condition (presence of both Higgs and matter sectors).
  4. Avoid one-step Yukawa-induced regeneration of dangerous operators.

2. Methodology: Physics as Code via Interactive Theorem Provers (ITP)

The authors propose a methodology where the model-building problem is formalized inside Lean, an interactive theorem prover. Instead of writing a script to scan models, they build a reusable Application Programming Interface (API) called PhysLib.

Core Components of the Methodology:

• Formal Vocabulary (The API):
  • Object Definition: A ChargeSpectrum is defined as a structured object containing optional Higgs charges and finite sets (Finset) of distinct matter charges for the $\mathbf{10}$ and $\mathbf{\bar{5}}$ representations.
  • Predicates: Physical constraints are encoded as reusable boolean predicates (e.g., AllowsTerm, IsPhenoConstrained, IsComplete).
  • Bounded Space: The search space is defined mathematically as a finite set of spectra derived from bounded charge menus ($S_{\bar{5}}, S_{10}$).
• The Reduction Strategy (Witness-Completion-Closure):
  Rather than enumerating the entire space, the authors prove a reduction theorem that shrinks the problem:
  1. Minimal Witnesses: Identify the smallest charge spectra (seeds) that satisfy the primary local constraint (e.g., allowing the top Yukawa coupling).
  2. Controlled Completions: Prove that any viable complete model containing a witness can be constructed by adding specific sectors in a controlled manner without violating constraints.
  3. Certified Closure: Prove that the set of viable models is closed under admissible enlargement steps within the bounded space.
• Executable Classification:
  The proof of the reduction theorem justifies an executable algorithm. The algorithm starts with the minimal witnesses, iteratively applies admissible enlargements, and filters out invalid spectra. Because the reduction is proven, the final output is guaranteed to be the exact set of viable models, not just a subset found by a heuristic.

3. Key Contributions

1. PhysLib Framework: The development of a reusable, open-source Lean library (PhysLib) that formalizes charge spectra, structural relations (subset, emptiness), and phenomenological predicates. This allows future formalizations to build upon existing definitions rather than starting from scratch.
2. Certified Reduction Theorem: A formal proof (Theorem 1) stating that within a bounded model class $U(I)$, a charge spectrum $x$ is viable if and only if it belongs to a constructed class $V(I)$ generated by minimal witnesses and controlled completions.
   • Soundness: Every element in $V(I)$ is physically viable.
   • Completeness: Every physically viable spectrum in $U(I)$ is in $V(I)$.
3. Separation of Proof and Computation: The paper distinguishes between the proven reduction logic (which guarantees correctness) and the computed enumeration (which generates the finite list). The computation is merely the evaluation of the theorem-backed construction.
4. Case Study Implementation: A concrete implementation for SU(5) F-theory models that successfully classifies viable charge spectra, demonstrating the feasibility of the approach.

4. Results

• Theoretical Result: The paper establishes that the set of viable charge spectra is not an opaque result of a scan but a mathematically derived set generated from a finite number of minimal seeds.
• Quantitative Result: In a specific test case (a codimension-one configuration with charge menus $S_{\bar{5}}, S_{10} = \{-3, \dots, 3\}$):
  • The ambient bounded model class contains 1,048,576 candidate spectra.
  • The certified viable class contains exactly 102 spectra.
  • The reduction theorem guarantees that these 102 are the only viable models in that space; no others exist.
• Workflow Validation: The authors demonstrate a workflow where a user can input bounded charge menus, evaluate the viableCharges function, and receive a list with a formal proof attached that the list is exhaustive.

5. Significance and Outlook

• Paradigm Shift: The paper moves theoretical physics from "implementation-dependent scanning" to "theorem-backed classification." It replaces the question "Did we find all models?" with "We have proved that this is the complete set."
• Scalability: By proving the reduction mechanism once, the method scales to larger charge menus without re-running opaque scans. The complexity is handled by the proof structure, not just raw compute power.
• Reusability: The API-based approach allows the community to extend the formalization to more complex scenarios (e.g., adding flux data, anomaly cancellation, or chirality assignments) without rebuilding the core logic.
• AI Integration: The authors suggest that such formal APIs provide a stable semantic layer for AI-assisted research. AI agents could propose conjectures or downstream analyses, while the ITP ensures the core definitions and transformations remain mathematically rigorous.
• Broader Impact: While demonstrated in SU(5) GUTs, the methodology is applicable to any BSM setting with combinatorial explosion in gauge sectors, charge assignments, and consistency conditions.

In summary, this paper demonstrates that Interactive Theorem Provers can be used not just to verify the final answer of a physics calculation, but to restructure the entire model-building workflow into a certified, reusable, and mathematically rigorous pipeline.