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

Dit artikel presenteert een methode waarbij interactieve stellingbewijzers (zoals Lean) worden gebruikt om combinatorisch complexe modelbouwproblemen in de $SU(5)$-fysica om te zetten in formeel geverifieerde, herbruikbare classificaties van fysisch haalbare lichtspectra, in plaats van zich te baseren op ondoorzichtige numerieke scans.

De kern

Stel je voor dat je een enorme bibliotheek binnenloopt, vol met boeken die allemaal een recept bevatten voor het bouwen van een nieuw universum. De uitdaging is om te vinden welke recepten echt werken (zodat er sterren, planeten en leven kunnen ontstaan) en welke leiden tot een universum dat direct instort of vol zit met fouten.

In de theoretische fysica is dit precies wat wetenschappers doen: ze zoeken door een gigantisch aantal mogelijke modellen (recepten) om te zien welke de natuurwetten van onze werkelijkheid kunnen verklaren.

Dit artikel, getiteld "Physics as Code", beschrijft een nieuwe, slimme manier om die zoektocht te doen. In plaats van blindelings door alle boeken te bladeren (wat een computer vaak doet), gebruiken de auteurs een interactief bewijssysteem (een soort super-slome wiskundige robot genaamd Lean) om de zoektocht zelf te herschrijven.

Hier is de uitleg in simpele taal, met een paar creatieve vergelijkingen:

1. Het Probleem: De "Naaiende Naald" in de Hooiberg

Stel je voor dat je een hooiberg hebt die zo groot is dat hij de aarde zou bedekken. Je moet er één specifieke, perfecte naald in vinden.

• De oude manier (Brute Force): Je laat een robot de hele hooiberg doornemen, één hooi-kluitje per keer. Als de hooiberg groter wordt, duurt het langer en langer. Als de robot een foutje maakt in zijn code, weet je niet of hij de naald gemist heeft of dat hij hem gewoon niet zag. Het resultaat is onzeker.
• Het probleem: In de fysica zijn die "hooibergen" (de mogelijke modellen) zo enorm groot dat een computer ze nooit volledig kan doorzoeken zonder fouten te maken of jaren te verspillen.

2. De Oplossing: De "Architect" in plaats van de "Zoeker"

De auteurs zeggen: "Waarom zoeken we niet eerst naar de minimaal benodigde onderdelen?"

Stel je voor dat je een huis wilt bouwen dat aan strenge veiligheidsregels voldoet.

• In plaats van alle mogelijke huizen te tekenen en dan te controleren welke veilig zijn, beginnen we met de kleinste mogelijke basis die al voldoet aan de belangrijkste regel (bijvoorbeeld: "het dak moet niet instorten").
• Dit noemen ze in het artikel "minimale getuigen" (minimal witnesses). Het zijn de kleinste, meest essentiële bouwstenen die al werken.

Vervolgens vragen we: "Hoe kunnen we deze kleine basis uitbreiden tot een volledig huis, zonder de veiligheidsregels te schenden?"

• Dit noemen ze "gecontroleerde aanvullingen" (controlled completions).
• De wiskundige robot (Lean) bewijst dan niet alleen dat een huis werkt, maar bewijst dat elk mogelijk veilig huis noodzakelijkerwijs opgebouwd moet zijn uit één van die kleine basisblokken, op een specifieke manier.

3. De Magie: Van "Zoeken" naar "Bewijzen"

Het belangrijkste verschil in dit artikel is de overstap van scannen naar bewijzen.

• Scannen (Oude manier): "We hebben 1 miljoen huizen gecontroleerd en 100 bleken veilig. Misschien zijn er er nog 100 die we gemist hebben."
• Bewijzen (Nieuwe manier): "We hebben bewezen dat elk veilig huis moet beginnen met een van deze 5 specifieke basisblokken. We hebben alle manieren geteld om die blokken uit te breiden. Er zijn precies 102 mogelijke veilige huizen. Er zijn er geen andere. Het is een feit, net als 2+2=4."

Dit is wat ze "ITP API's" noemen. Ze hebben een taal (een API) bedacht waarmee fysici hun vragen kunnen stellen aan de wiskundige robot, en de robot geeft niet alleen een antwoord, maar een garantie.

4. De Concrete Voorbeeld: Het SU(5) Model

In het artikel gebruiken ze een specifiek voorbeeld uit de deeltjesfysica (SU(5) modellen met extra symmetrieën).

• De taak: Vind alle combinaties van elektrische ladingen (de "recepten") die een top-quark Yukawa-koppeling toestaan (belangrijk voor de massa van deeltjes) en geen gevaarlijke deeltjes creëren die deeltjes zouden laten vervallen.
• Het resultaat: De computer heeft niet zomaar een lijst gemaakt. De robot heeft bewezen dat er in dat hele enorme universum van mogelijkheden slechts 102 geldige combinaties zijn. En dat is niet toeval; het is een wiskundig bewezen feit.

5. Waarom is dit belangrijk? (De "Bewijsbare" Lijst)

Stel je voor dat je een lijst hebt met alle mogelijke auto's die veilig zijn.

• Met de oude methode zou je zeggen: "We hebben 1000 auto's getest en deze 50 leken veilig."
• Met deze nieuwe methode zeg je: "We hebben bewezen dat er precies 50 veilige auto's bestaan die aan deze regels voldoen. Als je een 51e auto ziet, is hij per definitie onveilig."

Dit maakt de lijst betrouwbaar. Andere wetenschappers kunnen deze lijst gebruiken om verder onderzoek te doen, wetende dat ze geen mogelijke opties missen.

Samenvatting in één zin

Dit artikel laat zien hoe we complexe natuurkundige vraagstukken niet meer oplossen door blindelings te zoeken in een enorme chaos, maar door slimme wiskundige regels te gebruiken om de chaos te reduceren tot een klein, bewezen en volledig overzicht van wat er mogelijk is.

Het is alsof je van het zoeken naar een naald in een hooiberg overschakelt naar het bewijzen dat de hooiberg eigenlijk maar uit één klein vakje bestaat, en dat je de naald daar precies kunt vinden.

Technische samenvatting

Titel: Fysica als Code: Van Scans naar Stellingen met ITP-API's in SU(5) Modelbouw

1. Het Probleem

In de theoretische fysica, en specifiek in de snaarfenomenologie, is het een terugkerende uitdaging om betrouwbare globale uitspraken te doen over modelruimtes die begrensd zijn maar combinatorisch enorm groot zijn.

• De beperking van brute-force scans: Traditionele methoden om alle mogelijke ladingsspectra te scannen en te filteren, worden snel ondoorzichtig en onpraktisch naarmate de zoekruimte groeit. De correctheid van dergelijke scripts hangt vaak af van implementatiedetails en biedt geen wiskundige garanties.
• De beperking van statistische exploratie: Statistische steekproeven kunnen geen stellingen ondersteunde garanties bieden over de volledigheid van de gevonden modellen.
• Het doel: Het is noodzakelijk om een methode te ontwikkelen die de modelbouwproblematiek formaliseert binnen een interactieve stellingbewijzer (Interactive Theorem Prover - ITP), zodat classificaties niet alleen worden "gescand", maar wiskundig bewezen en herbruikbaar zijn.

2. Methodologie

De auteurs introduceren een API-gedreven methodologie binnen Lean, een interactieve stellingbewijzer. In plaats van een eenmalig verificatiescript, bouwen ze een herbruikbare infrastructuur genaamd PhysLib.

• Formalisatie van het probleem: Het fysieke probleem (het vinden van phenomenologisch levensvatbare SU(5)-modellen met extra Abelse symmetrieën) wordt vertaald naar een formeel classificatieprobleem.
  • Basisobject: ChargeSpectrum (Ladingsspectrum), een structuur die optionele Higgs-ladingen en eindige verzamelingen (Finsets) van materieladingen vastlegt.
  • Predicaten: Fysische eisen worden vertaald naar Lean-predicaten, zoals AllowsTerm (is een term toegestaan?), IsPhenoConstrained (ontbreken gevaarlijke operatoren?), en IsComplete (zijn alle benodigde sectoren aanwezig?).
• Reductiestrategie (Witness-and-Completion):
  • In plaats van de volledige ruimte te scannen, bewijzen de auteurs dat elke levensvatbare oplossing kan worden gegenereerd uit een eindig aantal minimale getuigen (minimal witnesses) en gecontroleerde aanvullingen (controlled completions).
  • Een minimaal getuige is het kleinste ladingsspectrum dat de gewenste koppeling (bijv. de top-Yukawa-koppeling) toelaat.
  • Gecontroleerde aanvullingen zijn stappen om dit getuige uit te breiden tot een volledig model zonder de fysische beperkingen te schenden.
• Bewijsstrategie: De auteurs bewijzen stellingen die aantonen dat de verzameling van alle levensvatbare spectra exact overeenkomt met de verzameling die gegenereerd wordt door deze getuigen en aanvullingen. Dit vervangt een exhaustieve enumeratie door een wiskundig gereduceerde constructie.

3. Belangrijkste Bijdragen

• PhysLib API: De ontwikkeling van een herbruikbare API voor ladingsspectra binnen Lean. Dit biedt een semantische laag die toekomstige formalisaties kan uitbreiden zonder de hele redeneerstack opnieuw te hoeven bouwen.
• Gecertificeerde Reductie: Het bewijzen van een reductiestelling die de zoekruimte drastisch verkleint. De stelling garandeert dat elke levensvatbare, complete ladingsspectrum in de begrende ruimte voortkomt uit een eindige set minimale getuigen.
• Van Theorema naar Uitvoer: Het koppelen van het bewijs aan een uitvoerbare routine. De auteurs tonen aan hoe een bewezen reductie kan worden omgezet in een concrete berekening die de exacte lijst van levensvatbare modellen genereert.
• Herbruikbaarheid: De code is ontworpen als een open-source bibliotheekcomponent, niet als een eenmalig script, waardoor het een fundamenteel hulpmiddel wordt voor toekomstig onderzoek.

4. Resultaten

De methode werd getest in een concreet geval: SU(5) modelbouw met extra Abelse symmetrieën (geïnspireerd door F-theory).

• De Stelling: Binnen de bestudeerde begrende klasse, is een ladingsspectrum x levensvatbaar en compleet dan en slechts dan als het behoort tot de door de auteurs geconstrueerde klasse V(I).
  • Dit betekent dat er geen andere levensvatbare spectra bestaan buiten de geconstrueerde lijst.
  • De lijst is niet slechts een output van een script, maar een formeel geverifieerde beschrijving van de volledige levensvatbare klasse.
• Concrete Uitkomsten:
  • Voor een specifieke configuratie met een omgevende modelklasse van 1.048.576 mogelijke spectra, reduceerde de gecertificeerde methode dit tot precies 102 levensvatbare spectra.
  • De auteurs onderscheiden duidelijk wat bewezen is (de semantiek, de reductiestrategie, de volledigheid) en wat berekend is (de concrete lijst van 102 spectra).
• Workflow: De workflow begint met het definiëren van de fysische eisen, vertaalt deze naar Lean, bewijst de reductiestelling, en voert vervolgens de classificatie uit. De output is een "gecertificeerde" lijst die als betrouwbare input kan dienen voor verdere fenomenologische analyse (zoals flux-data en anomalie-annulering).

5. Betekenis en Impact

• Methodologische Doorbraak: Het artikel toont aan dat interactieve stellingbewijzers niet alleen dienen om eindresultaten te verifiëren, maar kunnen worden gebruikt om de fysica-problematiek zelf te structureren in een herbruikbare, formele taal.
• Schalbaarheid: Door de combinatoriek via bewijzen te reduceren (in plaats van via snellere computers), wordt het mogelijk om grotere en complexere modelruimtes te bestuderen die voor brute-force methoden ontoegankelijk zijn.
• Betrouwbaarheid: Het biedt een nieuwe standaard voor betrouwbaarheid in de theoretische fysica. Uitsluitingen en classificaties zijn nu gebaseerd op bewezen stellingen in plaats van op de output van een mogelijk defecte scan.
• Toekomstperspectief: De auteurs zien dit als een stap naar schaalbare formele methoden in de theoretische fysica. Het creëert een brug tussen exploratief zoeken, uitvoerbare berekening en betrouwbaar wetenschappelijk redeneren, wat ook potentieel heeft voor AI-ondersteund onderzoek waarbij AI suggesties doet die door de ITP worden geverifieerd.

Kortom, het paper demonstreert dat het combineren van fysica met formele verificatie (ITP) leidt tot een "correctness-first" workflow, waarbij de classificatie van modellen niet alleen gevonden, maar wiskundig gegarandeerd is.