The continuous functional calculus in Lean

Technische Samenvatting: De Continue Functionele Calculus in Lean

Probleemstelling
De continue functionele calculus is een fundamenteel instrument in de theorie van $C^*$-algebra's, waarmee de identificatie van commutatieve $C^*$-subalgebra's met algebra's van continue functies op compacte Hausdorff-ruimten mogelijk wordt gemaakt. Hoewel wiskundig goed begrepen, vormt de formalisering ervan in bewijsassistenten zoals Lean een aanzienlijke uitdaging. De primaire moeilijkheid ligt in het balanceren van wiskundige getrouwheid met bruikbaarheid. Een "natuurlijke" wiskundige definitie leunt vaak op afhankelijke typen (bijv. functies die alleen gedefinieerd zijn op het spectrum van een element) en gebundelde structuren (bijv. continue afbeeldingen als een specifiek type). Hoewel deze rigoureus zijn, creëren ze frictie in formele bewijzen: het herschrijven van gelijkheden wordt moeilijk omdat typen afhangen van specifieke elementen, en het samenstellen van functies vereist het beheren van complexe subtype-coercies en continuiteitsbewijzen. De auteurs identificeerden dat een ontwerp dat prioriteit geeft aan strikte wiskundige eenvoud vaak faalt voor de "litmustests" van praktische bruikbaarheid die vereist zijn voor een bibliotheek als Mathlib.

Methodologie en Ontwerpbeslissingen
De auteurs hebben een formalisering van de continue functionele calculus ontwikkeld in Lean 4, geïntegreerd in de Mathlib-bibliotheek. Hun methodologie omvatte een iteratief ontwerpproces, bewegend van een wiskundig "zuivere" definitie naar een "utilitaire" interface. Belangrijke ontwerpbeslissingen omvatten:

1. Unbundling en "Junk Values":
   In plaats van de functionele calculus te definiëren als een afbeelding van het type continue functies op het spectrum $C(\sigma(a), \mathbb{C})$ naar de algebra, hebben de auteurs een functie cfc ontwikkeld die elke functie $f: \mathbb{C} \to \mathbb{C}$ en elk element $a$ accepteert. Als $a$ niet normaal is of $f$ niet continu is op het spectrum, geeft de functie een "junk value" terug (meestal 0).

   • Rationale: Dit stelt gebruikers in staat om uitdrukkingen zoals $f(a)$ te schrijven zonder eerst te bewijzen dat $a$ normaal is of dat $f$ continu is. Dit bootst de "eerst schrijven, later nadenken"-benadering van informele wiskunde na, waarbij de bewijslast wordt uitgesteld tot een niet-triviale eigenschap nodig is. Dit maakt ook naadloos herschrijven (rw) mogelijk omdat de typen van de argumenten niet langer afhangen van de specifieke eigenschappen van $a$.

2. Class-Based Abstraction:
   Om verschillende scalaire ringen ($\mathbb{C}$, $\mathbb{R}$, en $\mathbb{R}_{\ge 0}$) en verschillende elementtypen (normaal, zelfadjunct, niet-negatief) te behandelen, hebben de auteurs de calculus geïmplementeerd als een type class ContinuousFunctionalCalculus.

   • Predicaat-generalisering: De class is geparametriseerd door een predicaat $p$ op de algebra-elementen (bijv. IsStarNormal, IsSelfAdjoint, 0 ≤ a). Dit maakt het mogelijk om een enkele interface te gebruiken voor diverse gevallen zonder code-duplicatie.
   • Prop-Valued vs. Data: Vroege versies bevatten de $*$-homomorfisme als data. Echter, om problemen met definitionele gelijkheid te voorkomen (waarbij twee verschillende constructies van dezelfde afbeelding niet definitioneel gelijk zijn), maakt het uiteindelijke ontwerp de class een Prop. Het stelt de existentie van een unieke $*$-homomorfisme met specifieke eigenschappen vast, in plaats van de afbeelding zelf op te slaan.

3. Afhandeling van Niet-Unitale Algebra's:
   De formalisering strekt zich uit tot niet-unitale $C^*$-algebra's. In plaats van te vertrouwen op extrinsieke constructies zoals de minimale unitarisering voor elke definitie, hebben de auteurs een intrinsieke definitie van de quasispectrum geïntroduceerd. De niet-unitale functionele calculus is gedefinieerd op functies die in 0 verdwijnen (of 0 naar 0 mappen), waardoor het voortdurend wisselen tussen unitale en niet-unitale contexten wordt vermeden.

4. Automatisering via autoParam:
   Om de verbositeit van het handmatig doorgeven van continuiteits- en normaliteitbewijzen te verminderen, hebben de auteurs gebruikgemaakt van de autoParam-functie van Lean. Hypothesen zoals "$f$ is continu op het spectrum" zijn uitgerust met standaard tactieken. Als de gebruiker geen bewijs verstrekt, probeert Lean dit automatisch te synthetiseren met behulp van bestaande lemmas (bijv. aesop, fun_prop).

5. Uniciteit als Afzonderlijke Class:
   De compositie-eigenschap ($g(f(a)) = (g \circ f)(a)$) staat centraal in de theorie. De auteurs hebben dit bewezen met een uniciteitsargument in plaats van de Stone–Weierstrass-stelling (die faalt voor $\mathbb{R}_{\ge 0}$). Zij hebben de uniciteit van $*$-homomorfismen gecapsuleerd in een aparte class ContinuousMap.UniqueHom, waardoor de compositie-eigenschap generiek over verschillende scalaire ringen kan worden afgeleid.

Belangrijkste Bijdragen en Resultaten

• Eerste Formalisering: Dit werk vormt de eerste formalisering van de continue functionele calculus in enige bewijsassistent.
• Mathlib Integratie: De implementatie is samengevoegd met Mathlib, wat een verenigde interface biedt voor complexe, reële en niet-negatieve reële functionele calculi.
• Bruikbaarheidsverificatie: Het ontwerp is gevalideerd tegen specifieke "litmustests", waaronder:
  • Het definiëren van inversen ($f(a^{-1})$) met functies die niet overal continu zijn (bijv. $x \mapsto x^{-1}$).
  • Het construeren van positieve/negatieve delen en vierkantswortels voor zelfadjuncte en niet-negatieve elementen.
  • Het toepassen van de calculus op matrices over $\mathbb{R}$ (die in Mathlib geen globale metriekstructuur hebben).
• Automatisering: De interface ondersteunt hoogwaardige automatisering, waardoor gebruikers eigenschappen kunnen bewijzen zoals $f(-a) = (x \mapsto f(-x))(a)$ met minimale handmatige interventie.
• Applicaties: De interface is al gebruikt voor het formaliseren van geavanceerde resultaten, waaronder:
  • Het bestaan van benaderende eenheden in niet-unitale $C^*$-algebra's.
  • De continuïteit van de functionele calculus in beide variabelen.
  • Eigenschappen van afbeeldingen $a \mapsto |a|$, $a \mapsto a^p$, en $a \mapsto \log(a)$.
  • Resultaten met betrekking tot unitaire elementen en projecties.

Betekenis en Beperkingen
Het artikel claimt vooral betekenis in zijn ontwerpphilosofie: het demonstreren dat voor een tool om effectief te zijn in een grootschalige formele bibliotheek, het de ergonomie van de eindgebruiker (bruikbaarheid) moet prioriteren boven strikte wiskundige zuiverheid in de definitie. Door "junk values" te accepteren en typen te ontbinden, hebben de auteurs een interface gecreëerd die intuïtief werkt voor wiskundigen, wat complexe manipulaties (zoals compositie en herschrijven) mogelijk maakt die met een strikt afhankelijk-type benadering prohibitief moeilijk zouden zijn.

De auteurs zijn bescheiden over de huidige staat en erkennen enkele beperkingen:

• Simp Lemmas: Vanwege de noodzaak van expliciete argumenten om autoParam te triggeren, kunnen veel lemmas niet als simp regels worden gebruikt zonder handmatige interventie, wat sommige bewijzen meer talig maakt dan gewenst.
• $\mathbb{R}_{\ge 0}$ Complicaties: Het gebruik van de niet-negatieve reële getallen als scalaire ring introduceert specifieke technische hindernissen (bijv. getrunceerde aftrekking, gebrek aan ringstructuur) die aparte stellingverklaringen vereisen.
• Reële $C^*$-algebra's: Hoewel het framework is ontworpen om reële $C^*$-algebra's te ondersteunen, is het specifieke geval van de functionele calculus over $\mathbb{C}$ voor reële algebra's (die een andere domein van functies vereist) nog niet volledig geïntegreerd en staat gepland voor toekomstig werk.

Concluderend documenteert het artikel een succesvolle vertaling van een diepe operatoralgebra-theorie naar een bruikbaar formeel systeem, waarbij de afwegingen tussen wiskundige elegantie en praktische nuttigheid in de context van interactief bewijzen worden belicht.