💻 computer science

Complex Bounded Operators in Isabelle/HOL

Cet article présente une formalisation complète des opérateurs bornés sur les espaces vectoriels complexes dans Isabelle/HOL, étendant les développements existants sur les réels avec des concepts avancés tels que les unitaires, les adjoints et l'ordre de Loewner, tout en fournissant également la génération de code basée sur les matrices pour les cas de dimension finie.

Auteurs originaux : Dominique Unruh, José Manuel Rodríguez Caballero

Publié 2026-06-02

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Dominique Unruh, José Manuel Rodríguez Caballero

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayiez de construire une bibliothèque massive et complexe de règles mathématiques. Pendant longtemps, cette bibliothèque possédait une section très solide et bien organisée dédiée aux Nombres Réels (les nombres que nous utilisons pour compter, mesurer des distances et effectuer des calculs quotidiens). Cependant, les auteurs de cet article ont remarqué qu'il manquait une aile cruciale, tout aussi importante, à cette bibliothèque : la section dédiée aux Nombres Complexes (les nombres qui incluent la racine carrée de moins un, essentiels pour décrire les ondes, l'électricité et la mécanique quantique).

L'article, intitulé "Complex Bounded Operators in Isabelle/HOL", décrit le voyage des auteurs pour construire cette aile manquante à partir de zéro, en veillant à ce qu'elle soit aussi robuste, logique et utile que l'existante section sur les nombres réels.

Voici une décomposition de leur travail utilisant des analogies simples :

1. La Motivation : Pourquoi construire cela ?

Les auteurs travaillaient sur la Programmation Quantique (logiciels pour ordinateurs quantiques). Ils ont rencontré un problème : beaucoup d'articles mathématiques existants sur la mécanique quantique étaient écrits comme si l'univers ne possédait qu'un nombre fini de « pièces » (variables). Or, les vrais systèmes quantiques peuvent avoir un nombre infini de « pièces ».

Lorsque l'on tente d'appliquer des règles conçues pour une petite pièce finie à un couloir infini, les choses se cassent. Les mathématiques deviennent complexes car il faut se soucier de la manière dont les choses se comportent à la limite même de l'infini (topologie et limites). Les auteurs ont constaté que beaucoup d'articles existants étaient « négligents » sur ces détails infinis, ce qui menait à des erreurs potentielles. Ils avaient besoin d'une bibliothèque formelle, vérifiée par ordinateur, capable de gérer ces cas infinis parfaitement afin de pouvoir vérifier les logiciels quantiques sans deviner.

2. Le Concept Central : Les « Opérateurs Bornés »

Considérez un Espace Vectoriel comme une immense pièce multidimensionnelle où vous pouvez vous déplacer dans n'importe quelle direction.

Les Opérateurs sont comme des machines ou des fonctions qui prennent un point dans la pièce et le déplacent ailleurs.
Les Opérateurs Bornés sont des machines spéciales qui sont « bien élevées ». Elles ne prennent pas un petit pas pour soudainement projeter le point à travers l'univers vers l'infini. Elles maintiennent tout dans une distance raisonnable et prévisible.

Les auteurs ont créé un nouveau type d'objet dans leur bibliothèque appelé cblinfun (Fonction Linéaire Complexe Bornée). Considérez cela comme une télécommande universelle pour ces machines. Au lieu de simplement dire « cette machine existe », ils lui ont donné une carte d'identité spécifique, ce qui facilite grandement le fait de parler d'elles, de les combiner et de les tester.

3. Caractéristiques Clés de la Nouvelle Bibliothèque

Le « Miroir » (Opérateurs Adjoints)

Dans ce monde mathématique, chaque machine possède une « image miroir » appelée son Adjoint. Si vous faites fonctionner une machine puis son miroir, vous revenez souvent à votre point de départ (ou proche de celui-ci). Les auteurs ont formalisé la manière de construire ces miroirs pour les nombres complexes, ce qui est essentiel pour des choses comme les mesures quantiques.

L'« Ombre » (Projections)

Imaginez projeter une lumière sur un objet pour voir son ombre sur le sol. En mathématiques, cela s'appelle une Projection. Les auteurs ont formalisé la manière de calculer l'« ombre » d'un vecteur sur un sous-espace spécifique (une plus petite pièce à l'intérieur de la grande pièce). Ils ont prouvé que ces ombres sont toujours « bien élevées » (bornées) et possèdent des propriétés spécifiques, comme être leur propre miroir.

Le « Papillon » (Opérateurs de Rang 1)

Les auteurs ont introduit un concept mignon qu'ils appellent le « Papillon ». C'est une machine simple qui prend une direction spécifique et écrase tout le reste jusqu'à zéro, ne laissant qu'une seule ligne d'action. Ils ont montré que ces simples « Papillons » sont les blocs de construction de machines beaucoup plus complexes. Tout comme on peut construire une sculpture complexe à partir de formes d'argile simples, on peut construire des opérations quantiques complexes à partir de ces simples Papillons.

L'« Ordre de Loewner » (Comparer les Machines)

Comment décider si la Machine A est « plus grande » ou « plus forte » que la Machine B ? Dans le monde réel, on compare des nombres. Dans ce monde complexe, c'est plus difficile. Les auteurs ont créé un livre de règles spécial (l'Ordre de Loewner) qui permet aux mathématiciens de dire « la Machine A est inférieure ou égale à la Machine B » d'une manière mathématiquement rigoureuse. Ils ont dû être très ingénieux pour faire fonctionner ce livre de règles avec des machines qui n'ont même pas la même taille, en utilisant une astuce impliquant des « identités hétérogènes » (une façon sophistiquée de dire « prétendre que des choses différentes sont les mêmes pour faire fonctionner les mathématiques »).

4. Le Pont entre le Fini et l'Infini

L'un des aspects les plus pratiques de leur travail est de connecter le monde de l'Infini au monde du Fini.

Infini : La théorie générale fonctionne pour des espaces à dimensions infinies (comme un couloir infini).
Fini : Parfois, vous avez juste une petite grille finie (comme une matrice 3x3).

Les auteurs ont construit un pont entre leur théorie complexe et une bibliothèque existante appelée Jordan_Normal_Form (JNF). La JNF est comme une calculatrice puissante capable de traiter des nombres pour des matrices finies. Les auteurs ont prouvé que leurs « machines » complexes sont exactement les mêmes que les matrices de la JNF lorsque l'espace est fini.

Pourquoi est-ce important ?
Parce que la JNF possède la Génération de Code. Cela signifie que vous pouvez écrire une preuve mathématique dans leur bibliothèque, et l'ordinateur peut automatiquement la transformer en un véritable programme exécutable (comme en OCaml ou Haskell) qui s'exécute sur votre ordinateur portable. Ils peuvent désormais prouver un théorème sur un algorithme quantique et immédiatement l'exécuter pour voir s'il fonctionne, le tout au sein du même système.

5. L'Astuce de la « Dimension Un »

Les auteurs ont également formalisé un cas particulier : les Espaces de Dimension Un.
En mathématiques, un espace de dimension 1 est simplement une ligne. C'est si simple que c'est pratiquement la même chose que les nombres complexes eux-mêmes. Les auteurs ont créé un « traducteur » spécial (un isomorphisme) qui leur permet de traiter un espace de dimension 1 exactement comme un nombre complexe unique. Cela simplifie de nombreuses équations, transformant des opérations de machines complexes en de simples multiplications de nombres.

Résumé

En résumé, cet article traite de la construction d'un fondement rigoureux et vérifié par ordinateur pour les mathématiques des espaces complexes de dimension infinie.

Ils n'ont pas seulement écrit les règles ; ils ont construit une boîte à outils (cblinfun) pour manipuler ces règles.
Ils ont créé des ponts pour connecter la théorie infinie aux matrices finies calculables.
Ils ont permis la génération de code, permettant à ces preuves abstraites de devenir des logiciels exécutables.

Le but ultime, comme ils l'indiquent, est de fournir un socle mathématique solide et sans erreur pour la vérification des technologies quantiques, garantissant que lorsque nous construirons des ordinateurs quantiques, les mathématiques qui les sous-tendent seront aussi solides que le matériel lui-même.

Problématique

La motivation principale de ce travail découle de la formalisation des langages de programmation quantique et des logiques de Hoare quantiques. La littérature existante dans ce domaine restreint souvent, de manière implicite ou explicite, les résultats aux systèmes de dimension finie (par exemple, les qubits) ou ne distingue pas rigoureusement les espaces de Hilbert de dimension finie et de dimension infinie. Lorsqu'on traite de variables infinies (telles que les entiers quantiques), les mathématiques nécessitent des espaces de Hilbert de dimension infinie, où l'intuition et les théorèmes valables pour les systèmes de dimension finie (qui reposent sur les matrices) échouent souvent ou nécessitent des ajustements subtils concernant les types d'opérateurs (bornés vs non bornés), les topologies (norme d'opérateur, forte, faible, norme de trace, etc.) et la convergence des sommes infinies.

Les auteurs ont observé que de nombreux articles dans ce domaine définissent des concepts tels que les unitaires, les traces et les produits tensoriels sans spécifier les contraintes topologiques nécessaires pour les dimensions infinies, ce qui conduit à des erreurs mathématiques potentielles difficiles à vérifier sans une expertise approfondie en analyse fonctionnelle. De plus, les formalisations existantes dans Isabelle/HOL (par exemple, celles de Li et al.) ont été contraintes de se restreindre aux variables finies en raison de l'absence d'un socle formel en analyse complexe de dimension infinie.

Méthodologie

Les auteurs ont développé une bibliothèque complète au sein du prouveur de théorèmes Isabelle/HOL, spécifiquement la session Complex_Bounded_Operators. La méthodologie comprend :

Alignement structurel : La bibliothèque reflète la structure des développements existants d'Isabelle/HOL pour les espaces vectoriels réels (présents dans HOL-Analysis), en créant des théories parallèles pour les espaces complexes (ex: Complex_Vector_Spaces, Complex_Inner_Product, Complex_Bounded_Linear_Function). Cela facilite la comparaison et le portage futur des résultats des vecteurs réels vers le domaine complexe.
Abstraction par types : Au lieu de s'appuyer uniquement sur des prédicats pour les fonctions linéaires bornées, les auteurs définissent un type dédié cblinfun (ou ⇒CL) pour les opérateurs bornés. Cela permet aux opérateurs bornés d'être instanciés comme un espace vectoriel normé et un espace de Banach en soi, simplifiant l'énoncé des théorèmes et permettant l'utilisation du système de classes de types d'Isabelle pour les opérateurs.
Gestion des dimensions infinies : La formalisation traite explicitement les espaces de dimension infinie, définissant des concepts tels que les sous-espaces fermés, les compléments orthogonaux et diverses topologies d'opérateurs (par exemple, la topologie forte de l'opérateur). Elle distingue rigoureusement les opérateurs bornés des opérateurs non bornés et gère la convergence des sommes infinies.
Génération de code : Pour le cas de dimension finie, la bibliothèque établit une correspondance entre les opérateurs complexes bornés et les matrices formalisées dans l'entrée AFP Jordan_Normal_Form (JNF). Cela permet la génération de code, permettant l'exécution et la vérification de calculs concrets sur des opérateurs et des vecteurs de dimension finie.

Contributions clés

1. Espaces vectoriels complexes et espaces préhilbertiens

Espaces vectoriels : Définit les espaces vectoriels complexes, les espaces normés, les espaces de Banach et les algèbres en tant que classes de types. Introduit les concepts de fonctions antilinéaires et sesquilinéaires.
Espaces conjugués : Introduit un type d'« espace conjugué » ('a conjugate_space) pour transformer les fonctions antilinéaires en fonctions linéaires, permettant ainsi la réutilisation des théorèmes sur les fonctions linéaires.
Espaces de Hilbert : Formalise les espaces de Hilbert complexes, incluant l'existence de bases orthonormées (ONB), de compléments orthogonaux et le théorème de représentation de Riesz.
Espaces de dimension un : Définit une classe de type one_dim pour les espaces de dimension un, fournissant un isomorphisme canonique entre deux espaces quelconques de ce type et les nombres complexes. Cela formalise le raccourci mathématique courant (par exemple, identifier $\psi^* \phi$ avec le produit scalaire).

2. Opérateurs complexes bornés (cblinfun)

Définition de type : Introduit le type cblinfun pour les opérateurs linéaires bornés entre espaces normés complexes.
Propriétés des opérateurs : Développe la théorie des adjoints, des unitaires, des isométries, des isométries partielles et des projecteurs.
Ordre de Loewner : Définit l'ordre de Loewner ( $A \le B$ ) pour les opérateurs positifs. Cela a nécessité un contournement technique pour gérer la classe de type order pour les opérateurs non carrés en utilisant une « identité hétérogène » et des isomorphismes unitaires.
Opérateurs de rang 1 : Formalise les opérateurs « papillon » ( $|\psi\rangle\langle\phi|$ ) et prouve leurs propriétés, y compris leur rôle dans la construction de projecteurs et l'engendrement de l'espace des opérateurs compacts.
Théorèmes d'extension : Fournit le théorème de Banach-Steinhaus et le théorème de la transformation linéaire bornée (BLT) pour étendre les opérateurs bornés de sous-espaces denses à l'espace entier.

3. Fonctions sommables au carré ( $\ell^2$ ) et matrices

Espace $\ell^2$ : Formalise l'espace de Hilbert des fonctions sommables au carré ('a ell2), l'établissant comme l'espace de Hilbert canonique pour tout type de base 'a.
Kets et troncature : Définit les vecteurs de base canoniques (« kets ») et une opération de troncature pour approximer les vecteurs infinis par des vecteurs finis, facilitant les arguments de limite.
Correspondance matricielle : Pour les espaces de dimension finie, établit un isomorphisme rigoureux entre cblinfun et les matrices JNF. Cela inclut la mise en correspondance des opérations (addition, composition, adjoint, application) entre le domaine de l'opérateur et le domaine matriciel.

4. Génération de code

Met en place la génération de code pour les vecteurs, opérateurs et sous-espaces de dimension finie en enveloppant le code de génération JNF existant.
Représente les sous-espaces comme des listes de vecteurs générateurs (vecteurs JNF) et implémente des opérations telles que le span, l'intersection et la projection en utilisant l'orthogonalisation de Gram-Schmidt.
Permet aux utilisateurs de vérifier des faits sur des opérateurs concrets de dimension finie par calcul explicite (ex: commandes value).

Résultats et portée

La bibliothèque contient environ 18 758 lignes de code, 186 définitions et 1 645 lemmes prouvés.

Complétude : Elle couvre la théorie centrale des espaces de Hilbert complexes et des opérateurs bornés requise pour les formalisations de logiques quantiques, incluant le théorème de représentation de Riesz, les propriétés spectrales des projecteurs et la structure du treillis des sous-espaces fermés (treillis orthomodulaire complet).
Limitations : La formalisation est restreinte aux espaces vectoriels complexes. Bien que de nombreux théorèmes soient également valables pour les espaces réels, les auteurs n'ont pas créé de cadre générique couvissant les deux simultanément en raison des limitations des classes de types d'Isabelle/HOL concernant le corps scalaire. Par conséquent, certaines définitions et preuves ont dû être dupliquées ou adaptées à partir des bibliothèques de vecteurs réels existantes.
Dimension finie vs infinie : La bibliothèque prend en charge les dimensions finies et infinies. Cependant, la génération de code est explicitement limitée au cas de dimension finie, où les opérateurs sont isomorphes aux matrices.

Signification

L'article affirme que cette formalisation comble une lacune critique dans l'écosystème Isabelle/HOL, permettant la vérification rigoureuse de résultats en programmation quantique et en cryptographie quantique qui reposent sur des espaces de Hilbert de dimension infinie.

Vérification des logiques quantiques : Elle sert de fondement mathématique à des outils tels que qrhl-tool et aux formalisations de références quantiques, qui ne pouvaient pas auparavant traiter des variables infinies sans hypothèses mathématiques ad hoc ou incomplètes.
Rigueur mathématique : En traitant explicitement les topologies, la bornitude et les sommes infinies, la bibliothèque prévient les erreurs subtiles présentes dans la littérature informelle où l'intuition de dimension finie est incorrectement appliquée aux systèmes infinis.
Réutilisabilité : La bibliothèque est conçue comme une ressource générale pour l'analyse fonctionnelle dans Isabelle/HOL, et non seulement pour la mécanique quantique. Les auteurs notent que si de nombreux résultats existent probablement dans d'autres bibliothèques (comme mathlib de Lean), l'intégration spécifique avec le système de types d'Isabelle, la génération de code et le traitement explicite du cas complexe pour les opérateurs bornés en font une ressource unique et nécessaire pour leurs cas d'usage spécifiques.

Les auteurs soulignent que leur sélection de théorèmes a été guidée par les besoins pratiques de la formalisation des logiques quantiques, garantissant que la bibliothèque est « bien équilibrée » pour ce domaine tout en restant une contribution significative à la formalisation de l'analyse fonctionnelle en général.