La profondeur est presque invisible
Une vue contraint la translation le long du rayon dix fois moins que dans le plan : ±15 mm contre ±1,5 mm dans les mesures mêmes de la littérature.
ÉTUDE DE CAS · RECALAGE
Le scanner sur la radiographie, au millimètre prouvé.
Au bloc opératoire, le chirurgien navigue sur un scanner pris hier et des radiographies prises maintenant. Les recaler, c’est retrouver la pose de l’arceau dans le repère du scanner : six nombres. Aujourd’hui le résultat est un vecteur en virgule flottante et une impression visuelle. Ici, c’est un déplacement rigide exact, une erreur bornée, une preuve que la borne tient — ou un refus signé.
Rayons du Scanner exact à travers le scanner d’un bassin, jusqu’au détecteur d’un arceau mobile. Le sceau est le certificat.
Sans SGDL — avec SGDL, sur la même radiographie
Voyez-le avant de le lire.
Même cadavre, même scanner préopératoire, même radiographie stockée (gris). Le scanner est projeté à la pose que chaque chaîne a trouvée et posé sur la radiographie : orange là où le scanner à cette pose diverge du scanner à la pose vraie, boîtes rouges là où Lean a réfuté « ce repère est à moins de 2 mm », boîtes vertes là où Lean l’a prouvé. Chaque rendu ci-dessous vient du même noyau exact sur CSCS Alps — seule la pose change. Les nombres sont des erreurs vraies, mesurées contre la vérité-terrain du laboratoire, pas des scores de similarité.
Gauche · sans SGDL
Droite · avec SGDL
radiographie stockée scanner à la pose désaccord avec la vérité boîte de 2 mm prouvée par Lean boîte de 2 mm réfutée par Lean
Ce que vous voyez. Une radiographie fixe où se trouve l’anatomie en travers du faisceau, pas le long de celui-ci : une pose peut glisser de plusieurs millimètres en profondeur et sembler juste — c’est pourquoi une seule radiographie, même avec la chaîne exacte, laisse l’erreur à 5–12 mm. Un système classique lance ensuite un raffinement en virgule flottante qui maximise un score de similarité ; ici il part de la pose exacte à une vue, et son score monte à chaque fois — sur 17-1905 et 18-2799 alors que l’erreur vraie augmente. Rien, dans un système fondé sur un score, ne peut le dire. La chaîne SGDL fait trois choses à la place : elle garde chaque nombre exact (ℚ), elle ajoute les radiographies de la même séance (prouvée même séance par égalité d’entiers), et elle demande au prouveur Lean, repère par repère, si la pose est à moins de 2 mm — un verdict qui ne dépend pas de l’origine de la pose. Les sections suivantes montrent comment, et l’explorateur de rendus permet de regarder chaque vue de chaque scène certifiée.
Ce qui rend le recalage 2D/3D difficile
Trente ans de « rendre et comparer » — une radiographie reconstruite numériquement, une similarité, un optimiseur — atteignent le sous-millimètre si le départ est bon. Ce qui reste difficile est structurel.
Le paysage a beaucoup de vallées
Au-delà de quelques centimètres ou degrés d’erreur initiale, la similarité a d’autres minima. Des vertèbres répétitives, des instruments, la collimation et un fragment qui a bougé depuis le scanner ajoutent les leurs.
La géométrie est fragile en flottant
Une taille de pixel fausse de centièmes de millimètre donne des dizaines de millimètres d’erreur sur la cible. Chaque étape arrondit : calibration, pose inverse, projection, interpolation. Rien n’en est tracé.
Un score n’est pas une erreur
Une corrélation normalisée de 0,90 ne dit ni 1 mm ni 6 mm. Le cahier demande « une confiance de recalage ou une erreur sur la cible » par cas ; aucune méthode publiée n’en fournit une qui soit fiable.
Rien n’est rejouable
Sur les mêmes images DeepFluoro, les taux de succès publiés vont de 41 % à 87 % selon le protocole, le budget et la graine. Le résultat dépend de la version de la bibliothèque et du matériel.
L’os n’est pas un seul corps rigide
Entre le scanner et la radiographie, fémurs, vertèbres et — après une ostéotomie — un fragment ont bougé. La plupart des chaînes supposent encore une seule transformation rigide.
La chaîne, pas à pas
Des formes, pas des pixels. Dans l’arithmétique des formes, un solide est un programme sur des entiers — projectif, récursif primitif, terminant — et un point répond par une densité ternaire : extérieur, sur la frontière, intérieur. La chaîne de recalage est écrite dans ce langage de bout en bout. Lancez la lecture.
01 · Encoder
BigNum
Chaque radiographie, son en-tête DICOM complet et son sens deviennent un seul entier. 3 243 clichés, 26,4 Go ; 37 séries de scanner avec l’en-tête de chaque coupe.
02 · Localiser
Indexeur
La boîte du scanner et les sources d’arceau connues comme une scène .sl ; octree exact, rangs de Peano. La source estimée trouve sa vraie voisine.
03 · Recaler
Recherche exacte
Six paramètres BigNum, une rotation rationnelle avec RᵀR = I exactement, un score entier. 121 à 196 évaluations, une à deux secondes.
04 · Vérifier
Exolangage
meet_line_plane recalcule chaque reprojection en coordonnées homogènes entières : deux codes, un rationnel. 168/168 égaux.
05 · Certifier
Lean
Le repère recalé est-il dans une boîte de 2 mm autour du vrai ? Décidé sur ℚ, 336 fois. « Extérieur » vérifié, « intérieur » réfuté.
06 · Montrer
EXviator
Le noyau exact rend le scanner à chaque pose sur un GH200 : 36 rendus, 1536², chaque cellule. Mesure en gris, modèle en or, doute en orange.
Explorer les rendus
Choisissez un exemple, une vue, une pose. Fondez la mesure et le modèle.
Chaque rendu est produit par le noyau exact (EXviator, CSCS Alps GH200, toutes les cellules, 1536² natif) et posé sur la fluoroscopie stockée. Le gris est la mesure ; le violet, l’or et le cyan sont le scanner projeté à la pose initiale, estimée et vraie ; l’orange marque l’endroit où le modèle à cette pose diverge du modèle à la pose vraie ; les boîtes de 2 mm sont vertes quand Lean a vérifié « intérieur », rouges quand il l’a réfuté. Les quatre scènes certifiées montrent la même pose dans chacune de leurs vues ; les douze cas à une vue montrent ce qu’une radiographie laisse indécis.
Passez le pointeur sur le rendu : la loupe agrandit le détail dessous · au toucher, un tap ouvre le plein écran.
Le certificat, décidé exactement
Un certificat est une phrase sur un repère, vérifiée par le prouveur Lean : « le point recalé est à l’intérieur d’une boîte de côté 2,3 mm centrée sur le point vrai. » La boîte est une Forme (densité : intérieur / frontière / extérieur). Si le point est intérieur, chaque erreur d’axe est inférieure à 1,15 mm, donc la distance est inférieure à 2 mm — prouvée, non estimée. S’il ne l’est pas, le prouveur réfute la phrase et vérifie la phrase opposée (« extérieur ») : un non signé. Quatorze repères donnent quatorze phrases ; toute la décision tourne sur des nombres rationnels (ℚ), jamais sur des flottants, et chaque phrase porte un défi SHA-256 pour que quiconque puisse la rejouer.
Le widget ci-dessous exécute la même décision dans votre navigateur, sur des rationnels exacts (BigInt). Déplacez l’erreur — ou chargez-en une réelle : avec une seule radiographie, l’erreur de 18-2799 est presque entièrement en profondeur (Δz ≈ −10 mm) : l’ombre ne pouvait pas la voir, le certificat l’a vue.
Deux des 336 cartes. Chacune porte l’énoncé, le but Lean tel que compilé, la portée, l’arbitre et un défi SHA-256 de la charge utile canonique : quiconque dispose du prouveur peut le rejouer.
Douze cas, six cadavres, un protocole
Pose initiale perturbée de 8 mm et 1° par rapport à la vérité-terrain DeepFluoro, 2 500 points de surface osseuse nommés par l’exolangage, un score de chanfrein entier, une descente de coordonnées sur six paramètres BigNum. Triez le tableau.
| Spécimen | proj | mTRE init (mm) | mTRE est (mm) | score est / vérité | exolangage | Lean int / ext | incertitude | NCC est / vérité | lecture |
|---|
Les douze poses estimées, un rendu GPU par cas — fluoroscopie en gris, scanner à la pose estimée en or, incertitude en orange. Les trois cas divergents se voient d’un coup d’œil : la bande orange dans le rendu, et le mTRE qui augmente sous la tuile.
Calculé sur CSCS Alps, 395 minutes GPU, à partir de poses exactes converties en flottant seulement à la frontière du moteur de rendu.
Pourquoi tout encoder
Le contrat v3 place, dans le même entier que l’image, chaque élément DICOM — balises privées Toshiba et Siemens comprises, en octets exacts — et le sens certain écrit par les auteurs du jeu de données : démographie, phase chirurgicale, côté opéré, billes, fiduciaire. Non parce qu’il serait complet pour lui-même, mais parce que chacun de ces faits change ce qu’un recalage peut affirmer.
Toshiba (7005,100B)
AIDR 3D STD
La reconstruction itérative qui a façonné chaque valeur de Hounsfield. Une DRR rendue à partir d’un scanner « AIDR 3D » n’a pas la texture d’une rétroprojection filtrée. L’enregistrement la porte, donc un résultat peut être groupé par reconstruction — et une affirmation de robustesse prouvée par classe, au lieu d’être noyée dans une moyenne.
Toshiba (7005,1041) · (0018,1210)
0,5×80 · FC18 / FC30
Collimation 0,5 mm × 80 rangées et le noyau de convolution — mou (FC18) ou osseux (FC30). Deux séries du même examen, deux textures. Laquelle a alimenté le recalage est un fait de l’enregistrement, pas une note dans un carnet.
Siemens (0019,1006) · (0019,1007) · (0021,1013)
table–objet, table–détecteur, rotation du patient
La géométrie d’arceau que les balises publiques ne donnent pas. Avec SDD = 1020 mm et un pixel de 0,1940 mm conservé comme chaîne décimale — pas le float32 0,19400000572 — la matrice intrinsèque est exacte. La littérature mesure des dizaines de millimètres d’erreur pour des centièmes de millimètre de taille de pixel.
Readme, tableaux 1–2
18-1109 : femme, 57 ans · 18-2800 : homme, 94 ans
La densité osseuse, l’épaisseur corticale et le contraste suivent l’âge et le sexe. Le lot se lit par cohorte sans tableur annexe : c’est dans l’entier de chaque image. Ce qui n’est pas dans les tableaux des auteurs (poids, côté dominant) n’est pas encodé.
Readme, ct/<dir> · fluoro/session_<dir>
preop · preop_2_bb_injected · postop_1_right · postop_2
Après l’ostéotomie droite, l’hémibassin droit est deux corps rigides. Un recalage rigide du bassin entier y est faux par construction. La phase dit à l’arithmétique des formes quels solides se déplacent ensemble : une union de formes, chacune avec son propre déplacement, densités combinées par min et max.
Tableau des rotations, « other notes » · FTRAC
Ostéotomies achevées et fragment NON fixé · FTRAC : oui
Des billes de tantale qui « ne sont pas restées fixées à l’os », un fiduciaire visible sur certaines images : du métal connu dans le champ, le désaccord de contenu que toute méthode redoute. Savoir exactement quelles images le portent permet de le masquer, de tester avec et sans — ou d’utiliser le FTRAC comme seconde vérité-terrain.
Ce que cela rend possible
Une requête — « toutes les images de spécimens féminins, après ostéotomie, fragment non fixé, rotation orbitale, FTRAC présent » — est un ensemble d’entiers, pas une jointure entre un tableur, un fichier HDF5 et un PACS. Chaque enregistrement se rejoue seul : la géométrie, l’image, la licence et le défi du certificat sont dedans. Et les cadavres C304HZ ont été imagés avant et après une ostéotomie périacétabulaire : la même région, la même modalité, un changement chirurgical connu. L’hémibassin inchangé recale scanner sur scanner sans écart de domaine ; le déplacement du fragment est alors une quantité mesurée, certifiable.
En quoi cela diffère
Le HDF5 de DeepFluoro garde un sous-ensemble float32 : matrices, poses, étiquettes, quatorze repères — pas d’en-tête, pas de phase, 366 images sur 399. Les anonymiseurs hospitaliers retirent les balises privées. Les chaînes d’apprentissage lisent les intrinsèques en flottant, rééchantillonnent vers des valeurs canoniques et abandonnent le reste — puis publient des taux de succès qu’on ne peut pas réconcilier sur les mêmes images. Ici rien n’est abandonné et rien n’est interprété au-delà de ce qui est certain : les octets d’une balise privée sont gardés exactement, leur sens est laissé à qui détient le dictionnaire.
Cinq preuves lisibles d’un coup d’œil
Avec SGDL, sans SGDL — la preuve
Chaque figure ci-dessous est calculée à partir des fichiers de résultats du dépôt ; aucun nombre n’est saisi à la main. Quatre spécimens servent de témoins — 18-2800, 18-2799, 17-1905, 18-1109 — et chacun porte une ligne du tableau de comparaison.
Commencez ici — les mêmes entrées, deux chaînes
Ce que le jeu de données fournit, et ce que chaque chaîne en fait
La radiographie telle qu’elle sort de l’arceau — comptes de photons entiers en 1536², os sombre —, le scanner en unités Hounsfield avec les étiquettes des auteurs, et l’en-tête DICOM avec ses éléments privés Siemens et Toshiba. À gauche : une chaîne classique en fait des flottants, un en-tête réduit et un score. À droite : SGDL en fait un seul entier qui contient tout, une caméra exacte, des Formes, une scène et des preuves. Les preuves ci-dessous suivent cette colonne de droite.
Ce qu’est, concrètement, la « chaîne flottante classique ». Pas un homme de paille : la chaîne de référence du domaine, lue dans le code public de xReg/DeepFluoro (Grupp et al., 2020), DiffDRR/DiffPose (Gopalakrishnan et al., 2024) et xvr (2025). (1) Les matrices de calibration K et E sont lues en float32 — l’espacement de pixel DICOM 0.1940 devient 0,19400000572 ; l’inverse de la pose est calculé en float64. (2) L’image est rééchantillonnée vers une caméra « canonique » (xvr : 256–512 px), normalisée en flottant, passée au logarithme. (3) Le scanner devient un tenseur d’atténuation float32 et la DRR est rendue par interpolation trilinéaire le long des rayons (Siddon flottant) sur GPU. (4) La pose est un vecteur de se(3) ou des angles d’Euler en flottant ; R = exp(ξ) satisfait RᵀR = I à 10⁻⁷. (5) Une similarité flottante (NCC, NCC de gradient ou apprise) est maximisée par Adam ou CMA-ES avec une règle d’arrêt en ε, depuis une initialisation apprise (DiffPose : ≈ 12 h d’apprentissage par patient). (6) Le biplan est supposé d’après l’appareil ; la phase chirurgicale est une métadonnée, quand elle existe. (7) Sortie : six flottants et un score ; l’erreur vraie n’est connue qu’au laboratoire ; le rejeu dépend de la graine, du GPU et des versions de bibliothèque (41 % contre 87 % de succès sur les mêmes images). La chaîne BigNum reprend ces sept étapes une à une — c’est ce que la figure met côte à côte.
Preuve 1 — Le certificat ne dépend pas de la méthode
Trois façons d’obtenir une pose, les mêmes quatorze verdicts
18-2800. Une radiographie et la chaîne exacte : 5,17 mm, quatorze réfutations. Un raffinement flottant classique enrobé par la chaîne : 0,575 mm, quatorze preuves. Quatre radiographies de la même séance et la chaîne exacte seule : 0,497 mm, quatorze preuves — pas un flottant dans l’estimation. Même prouveur, mêmes boîtes de 2 mm, trois provenances : il dit non quand c’est faux et oui quand c’est vrai, sans savoir d’où vient la pose.
Preuve 2 — Un score peut mentir ; un certificat ne le peut pas
Le raffinement a dit « mieux » trois fois. La vérité a dit « pire » deux fois.
Le raffinement flottant — celui que font tourner les systèmes de navigation — améliore sa propre similarité dans les trois cas. Sur 17-1905 et 18-2799 l’erreur vraie augmente pendant que le score monte : un système fondé sur un score aurait validé. Le certificat Lean a réfuté les deux et prouvé le troisième. C’est la ligne « et s’il a tort ? », mesurée.
Preuve 3 — Une radiographie ne dit pas la profondeur
Chaque radiographie de la même séance ajoutée à la scène divise l’erreur — exactement
Mêmes données, même protocole, mêmes générateurs de silhouette. Aucune radiographie seule ne passe sous 3 mm ; chaque vue de la même séance ajoutée par induction divise l’erreur : 0,40 mm (18-2799, quatre vues), 0,50 mm (18-2800), 0,88 mm (17-1882, deux vues), 0,89 mm (17-1905). Lean signe 14/14, 14/14, 14/14, 13/14. 18-2799 était divergent à une vue (10,6 mm).
Preuve 4 — Deux radiographies vont ensemble si leurs entiers le disent
L’appartenance à une séance est une égalité d’entiers, pas un champ de métadonnées
18-1109 a été imagé quatre fois, de part et d’autre de deux ostéotomies, avec un seul scanner préopératoire. La vue 098 (1er décembre, après l’ostéotomie droite) avait piégé la scène à 11–21 mm. Sa séance n’est pas un champ que l’on consulte : c’est l’égalité exacte des comptes stockés entre la projection publique et l’image DICOM d’origine — 366 projections sur 366 appariées en 67 s. La scène la refuse avant de lire un pixel.
Preuve 6 — Ce que voit le chirurgien : une radiographie, puis quatre
18-2799 : l’orange disparaît, les boîtes passent au vert
À gauche : une radiographie, chaîne exacte — 10,6 mm, divergence, 3,7 % du champ en désaccord, quatorze réfutations. À droite : la même radiographie avec la pose de la scène à quatre vues de la même séance — 0,402 mm, 0,0 % de désaccord, quatorze preuves. Entre les deux, pas de flottant : des cônes, des tubes, un DLint, une induction. Rendus EXviator du noyau exact ; les validations portent sur la scène, l’image est pour l’œil.
18-2800, la même comparaison : 5,17 mm et 7,0 % du champ en doute avec une radiographie ; 0,497 mm et 0,13 % avec quatre.
Une pose, quatre arceaux
La pose certifiée d’une scène est une seule pose du volume ; ici elle est projetée par le noyau exact dans chacune des quatre radiographies de la scène (rendus pleine résolution sur CSCS Alps). Désaccord avec la vérité : 0,0 % du champ dans les quatre vues de 18-2799, 0,0–0,13 % pour 18-2800 ; chaque boîte verte. C’est ce qu’un biplan montrerait — obtenu ici sans en avoir un.
Preuve 5 — « Biplan » n’est plus une intention : c’est un intervalle prouvé
Le banc de référence ne contient aucun vrai biplan
Chaque radiographie laisse un tube d’incertitude de 5 mm autour de son rayon ; ce que la scène ignore encore de la profondeur est l’intersection des tubes, comptée en pas rationnels, les deux extrémités prouvées par Lean. Un vrai biplan virtuel (rayon orthogonal) laisse toujours 10 mm — la largeur du tube ; la meilleure paire qu’offre le jeu public laisse 20 à 48 mm. La méthode atteint 0,40 mm sans en avoir un.
Les témoins
Quatre spécimens, quatre preuves
18-2800 — de l’octet à la preuve
Un homme de 94 ans, un scanner, 55 radiographies en une seule séance (prouvée par égalité d’entiers). Départ 13,8 mm. Une radiographie, chaîne exacte : 5,17 mm, 0/14. Raffinement flottant enrobé : 0,575 mm, 14/14. Scène par induction, sans flottant : +003 (la vue la plus « biplan » du jeu) 1,25 mm, +009 0,64 mm, +046 0,497 mm, 14/14 — quatorze repères entre 0,29 et 0,83 mm ; rayons concourants 14/14, quatre sources hors du volume, 5 s de recherche, neuf minutes de preuves.
18-2799 — perdu, pris, gagné
Une radiographie : la chaîne exacte diverge (10,6 mm). Le raffinement flottant enrobé s’enfonce encore : 17,1 mm — réfuté quatorze fois, sans que la chaîne sache que le flottant avait échoué : elle le mesure. La scène construite par induction dans l’unique séance — 000 + 035 (0,77) + 001 (0,57) + 007 — donne 0,402 mm, quatorze repères entre 0,21 et 0,69 mm, 14/14 prouvés. Le meilleur résultat de l’étude, sur le cas qui partait le plus mal.
17-1905 — le score qui ment
Le raffinement flottant fait passer sa similarité de 0,51 à 0,67 ; l’erreur vraie passe de 12,1 à 13,2 mm. Tout système fondé sur un score aurait validé cette pose. Lean la réfute 14/14. La scène à trois vues (000 + 007 + 002) atteint ensuite 0,889 mm, 13/14 — ASIS gauche à 1,21 mm, une composante au-dessus de 1,15.
18-1109 — deux radiographies qui ne vont pas ensemble
Quatre séances de part et d’autre de deux ostéotomies, un scanner. La vue 098 (séance 2, trois jours après la coupe du côté droit) a piégé la scène à 11–21 mm, avec un score de vérité-terrain double de celui de l’estimée. L’égalité d’entiers avec son image DICOM la place en séance 2 : refusée avant qu’aucune image ne soit lue. La séance 1 n’offre que des vues opposées (de dos), qui n’améliorent pas la pose : 18-1109 reste à 6,7 mm — une limite du jeu public, dite comme telle.
18-2800, pose à une vue (5,17 mm) rendue sur Alps : l’or déborde du gris et l’orange marque l’écart — presque invisible de face parce qu’il est en profondeur. C’est ce que corrige la scène à quatre vues.
Vérification humaine seulement. Toute validation porte sur la scène SGDL : densités de Kleene, constructions projectives exactes, certificats Lean.
Plusieurs vues, comme Formes : profondeur, phase, biplan
Chaque arceau est une Forme — le cône de son collimateur, placé par une matrice exacte ; le champ commun de deux arceaux est l’intersection des cônes ; un point osseux est vu si sa densité de Kleene dans le cône est INT, décidée par l’exolangage et évaluée identiquement en local (1 121 = 1 121). Ce qu’une vue ignore de la profondeur est un tube autour de son rayon ; ce que la scène ignore encore est l’intersection des tubes — comptée en pas rationnels, sans trigonométrie, et prouvée par Lean à ses deux extrémités. Deux vues n’entrent dans la même scène que si leurs images sont de la même séance, décidée par égalité exacte des comptes.
| Spécimen | chaque vue seule | deux vues | trois vues | quatre vues · certificats |
|---|---|---|---|---|
| 18-2799 | 000 : 9,45 · 012 : 14,16 · 019 : 1,84 | 000+035 : 0,77 | +001 : 0,57 | +007 : 0,402 — Lean 14/14, rayons 14/14, sources 4/4 |
| 18-2800 | 000 : 3,11 · 003 : 10,53 · 009 : 3,71 | 000+003 : 1,25 | +009 : 0,64 | +046 : 0,497 — Lean 14/14, rayons 14/14, sources 4/4 |
| 17-1882 | 000 : 3,82 | 000+026 : 0,879 (point fixe) | — | Lean 14/14 ; vues de la séance 2 (après l’ostéotomie gauche) exclues par égalité d’entiers |
| 17-1905 | 000 : 9,63 · 011 : 10,99 · 004 : 19,88 | 000+007 : 1,61 | +002 : 0,889 | Lean 13/14 (ASIS gauche à 1,21 mm) |
| 18-1109 | 000 : 6,71 | 000+098 (autre séance) : 11–21, refusé | — | la séance 1 n’offre que des vues de face et de dos (sources opposées) : aucune n’améliore — une limite du jeu |
| 18-0725 | 000 : 22,0 | — | — | aucune seconde vue admissible : toutes opposées (le tube rend le rayon entier) |
Aucune vue seule ne passe sous 1,8 mm (3,1 mm pour la meilleure vue frontale) ; la scène divise l’erreur par 4 à 25. Quatre spécimens sur six sont certifiés sous 2 mm par la chaîne exacte seule ; les deux autres n’ont, dans le jeu public, aucune seconde vue de la même séance qui ne soit pas opposée à la première.
L’espace des poses comme objet à n dimensions. Une pose est un point de ℤ⁶ ; une boîte de poses est parcourue par la métacourbe de Gray du brevet d’indexation SGDL (WO 2025/003999 ; propriété de Gray et bijectivité prouvées dans SGDL Lean). Deux usages à ce jour : un balayage grossier exhaustif (5⁶ = 15 625 poses en 45–75 s) avant la descente, qui a retiré la divergence induite par la recherche de 17-1905/010 (20,8 → 3,8 mm) ; et, par vue, des ensembles de poses quasi optimales (34–163 cellules), dont l’intersection et la plus petite tolérance commune δ* classent les vues selon combien elles corrigent la profondeur (7–18 % pour les vues qui ont le plus aidé, ≈ 0 pour les coaxiales) — mais ne séparent pas une vue d’une autre séance chirurgicale (18-1109/098 : 18,9 %). L’identité de séance reste une égalité d’entiers ; ce résultat négatif est consigné comme tel.
Avec SGDL, sans SGDL — en clair
| La question au bloc | Sans SGDL (aujourd’hui) | Avec SGDL (mesuré ici) |
|---|---|---|
| Cette superposition est-elle juste ? | Un score de similarité. Aucune méthode publiée ne donne une erreur fiable par cas ; l’erreur vraie n’est connue qu’au laboratoire, après coup. | Quatorze repères, quatorze erreurs exactes (des fractions, pas des arrondis), quatorze verdicts d’un prouveur : « sous 2 mm : prouvé » ou « réfuté ». (Preuve 1) |
| Et s’il a tort ? | Rien ne le dit. Sur les mêmes images, deux laboratoires publient 41 % et 87 % de succès. | L’échec est détecté et signé : deux raffinements flottants qui dégradaient la pose ont été réfutés alors que leur similarité s’améliorait ; une image d’une autre séance a été refusée par la scène. (Preuve 2) |
| Une radiographie suffit-elle ? | On le croirait — la profondeur cache l’erreur. | La profondeur est mesurée comme une Forme (des tubes) ; avec deux à quatre vues de la même séance, l’erreur passe de 3–12 mm à 0,40–0,89 mm, prouvée point par point. (Preuve 3) |
| Ces deux radiographies vont-elles ensemble ? | Un champ de métadonnées dont on espère qu’il est juste. | Égalité d’entiers : 366/366 images appariées à leur séance en 67 s. (Preuve 4) |
| Est-ce un vrai biplan ? | Une intention du fabricant. | Un intervalle certifié : le prouveur signe combien d’ambiguïté chaque paire laisse. (Preuve 5) |
| Peut-on le refaire dans dix ans ? | Des poids, des versions de bibliothèque, des flottants. | Tout est un entier : image, en-tête complet, géométrie, pose, preuve ; chaque certificat porte un défi rejouable. |
| Faut-il entraîner un modèle ? | Oui : 12 heures par patient pour le meilleur (DiffPose, 0,60 mm). | Pas d’apprentissage. Géométrie exacte, recherche entière, preuves — explicable ligne à ligne. |
| Que voit le chirurgien ? | Une superposition colorée. | Le rendu EXviator du noyau exact : gris, or, et orange là où la machine ne sait pas. |
Glossaire
Les mots de cette étude de cas, en clair — y compris ceux qui sont propres à SGDL.
| ℚ | Lire « Q ». L’ensemble des nombres rationnels : toute fraction p/q d’entiers. Calculer « sur ℚ » signifie ne jamais arrondir — 1/3 reste 1/3, pas 0,333. Tout le géométrique ici (caméra, pose, projection, erreur) vit sur ℚ. |
|---|---|
| BigNum | Un entier de taille arbitraire (des milliers ou des millions de chiffres) traité exactement par la machine. Une image et son en-tête DICOM complet tiennent dans un seul BigNum. Bibliothèque : gmpy2 (entier mpz, rationnel mpq). |
| Flottant (float32 / float64) | Le format numérique usuel de l’ordinateur : rapide, mais arrondi à chaque opération. Les méthodes de l’état de l’art calculent en flottant ; cette chaîne ne le fait pas (sauf l’« enrobage » déclaré). |
| Arithmétique des formes (AdF) | Théorie de J.-F. Rotgé (thèse, 1997, L’arithmétique des formes, Université de Montréal) : une forme n’est pas un maillage mais une expression arithmétique ; en chaque point elle renvoie une densité. Opérateurs : voir DL. |
| Densité, Kleene (INT / FRO / EXT) | La valeur d’une forme en un point : 2 = intérieur (matière), 1 = frontière (exactement sur la surface), 0 = extérieur (vide). Logique trivaluée de Kleene, décidée exactement. |
| DLint, DLuni, DLadd, DLmin, DLsqr, DLdif | Opérateurs de densité : intersection (ce qui est commun), union, addition (collage), minimum (saturation), racine carrée entière, différence positive (surplomb). Opérations sur des entiers, pas des booléens. |
| GDconseg, GDcylseg, SDmatrep | Formes et attributs du langage SGDL : un cône à partir d’un rayon et de deux points (le collimateur), un cylindre sur un segment (le tube d’incertitude), une matrice de déplacement exacte (la pose). |
| Exolangage SGDL, SL, Scheme | Langage de description de formes de SGDL (SGDLscript 2003, syntaxe Scheme), servi par un moteur exact (le WMCP) qui valide une expression et sonde ses densités en entiers. Un second calcul indépendant. |
| Lean, native_decide, certificat, kind | Lean 4 est un assistant de preuve : il vérifie un énoncé mécaniquement. native_decide le décide par calcul exact sur ℚ. Un certificat est un énoncé vérifié (« ce point est dans cette boîte ») ; un kind est un modèle d’énoncé (boîte, distance, tube…). Le prouveur ne signe jamais ce qui est faux. |
| Pose, six degrés de liberté | Où se trouve l’arceau par rapport au scanner : trois translations et trois rotations. Ici : six entiers (translations en 0,1 mm, rotation comme quaternion entier), donc une rotation exactement orthogonale. |
| Arceau, collimateur, source, détecteur | L’appareil de radiographie peropératoire : une source face à un détecteur plan ; le collimateur limite le champ (le cône que l’on voit). |
| DRR | Digitally Reconstructed Radiograph : radiographie reconstruite numériquement à partir du scanner, à une pose donnée. EXviator les produit avec le noyau exact — l’image or des figures. |
| Repères (ASIS, FH, GSN, IOF, IPS, MOF, SPS ; -l / -r) | Quatorze points du bassin définis par DeepFluoro (épines iliaques, têtes fémorales, échancrures sciatiques, foramens obturateurs…), gauche / droit. L’erreur s’y mesure. |
| TRE, mTRE | Target Registration Error : distance entre un repère recalé et sa position vraie ; mTRE = moyenne sur les quatorze. Calculée exactement (une fraction), affichée en mm. |
| Boîte de 2 mm, « intérieur » / « extérieur » | Le certificat Lean par repère : le point recalé est-il dans une boîte de 2,3 mm centrée sur le point vrai ? Intérieur prouvé ⇒ erreur < 2 mm. |
| Chanfrein, générateurs de silhouette | Le score : distance entière de chaque point de surface projeté au contour de radiographie le plus proche. Les générateurs sont les seuls points qui impriment une arête (rayon rasant l’os). |
| Tube, ambiguïté résiduelle, nombre logique | Ce qu’une radiographie ignore de la profondeur : un cylindre de 5 mm autour de son rayon. Ce que la scène ignore encore : l’intersection des tubes, comptée en pas (le nombre logique). Un biplan laisse 10 mm. |
| Métacourbe de Gray, rang, couplage | Une façon de parcourir une grille à n dimensions pas à pas (brevet WO 2025/003999) : chaque cellule a un numéro (rang), les numéros consécutifs sont voisins. Le couplage transforme un n-uplet en un entier, de façon réversible et prouvable. |
| Induction (construction inductive) | Construire la scène vue par vue : une base (la vue frontale), une règle d’ajout (la vue qui conserve l’invariant), un arrêt. La même logique que les définitions récursives de la thèse et de CSGTree dans Lean. |
| Séance, phase | L’ensemble des radiographies d’un jour sur un spécimen ; la phase chirurgicale (avant / après ostéotomie). Décidée ici par égalité exacte des octets entre la projection publique et son image DICOM. |
| Enrobage | Enrober un raffinement flottant classique dans la chaîne exacte : il propose une pose, la chaîne la ramène sur ℚ et la certifie ou la réfute. |
| EXviator | Moteur de rendu de SGDL (noyau exact, CPU ou GPU) : produit les DRR des figures ; sert la vérification humaine, pas la validation. |
| Défi SHA-256, rejeu | Chaque certificat porte l’empreinte de son énoncé ; quiconque le soumet au prouveur obtient le même verdict. |
| DeepFluoro, C304HZ | Le jeu de données de référence public (6 cadavres, 366 radiographies avec vérité-terrain, Johns Hopkins) et les archives DICOM originales dont il a été extrait (CC BY-NC). |
| Biplan | Deux radiographies prises en même temps depuis des directions très différentes ; lève la profondeur. DeepFluoro n’en contient aucun vrai (prouvé plus haut). |
Face à l’état de l’art — honnêtement
Les meilleures méthodes publiées atteignent 0,5–1,1 mm sur DeepFluoro après une initialisation apprise et un raffinement par gradient — une vue, virgule flottante, des heures d’apprentissage propre au patient pour la meilleure, aucun certificat par cas. À comparer à l’identique : notre vue exacte unique n’est pas compétitive (4–12 mm) ; notre raffinement flottant enrobé atteint leur précision sur deux cas, avec preuves ; nos scènes exactes multi-vues atteignent 0,40–0,89 mm sur quatre spécimens avec 13–14/14 preuves et sans apprentissage — un résultat de type biplan, que la même mesure montre obtenu sans aucun vrai biplan dans le jeu. À une vue, la chaîne SGDL ne concurrence pas ce nombre : son objectif de contour s’arrête à 4–12 mm et diverge dans trois cas. Avec deux à quatre vues de la même séance, exactement et sans apprentissage, elle atteint 0,40–0,89 mm certifiés sur quatre spécimens sur six — l’ordre de grandeur des meilleures méthodes apprises, avec une preuve par repère. Ce qu’elle apporte est orthogonal, et peut enrober n’importe quel raffinement : l’exactitude à chaque étape, un second calcul indépendant de la géométrie, un certificat qui refuse ce qui est faux, et une image du doute.
| Méthode | famille | précision (DeepFluoro) | préparation du patient | arithmétique | certificat par cas · détection d’échec | rejouabilité |
|---|---|---|---|---|---|---|
| DiffPose (CVPR 2024) | rendu différentiable | 0,60 mm médiane, 83–87 % sous le mm | ≈ 12 h par patient | float32 / float64 | score de similarité | dépend de la graine, de la bibliothèque, du GPU |
| xvr (2025) | fondation + raffinement | 1,1 mm médiane, 95 % ≤ 10 mm | 5 min d’ajustement fin | flottant | aucun par cas | 41 % contre 87 % SMSR sur les mêmes images, selon le protocole |
| Chen & Kong SO(4) (2025) | similarité apprise + LM | 0,51 mm médiane, 86 % | heures | flottant | aucun | code partiel |
| LevelCheck (2013–2018) | CMA-ES + information de gradient | 99,99 % < 5 mm (PDE), capture ±200 mm | aucune | flottant | aucun | pas open source |
| SGDL, chaîne exacte, une vue (cette étude) | BigNum, exolangage, Lean, EXviator | 4–12 mm dans 9/12, 3 divergent (le balayage par métacourbe retire une divergence : 20,8 → 3,8 mm) | aucune | ℚ partout | 336 verdicts, toutes les réfutations — correctes | enregistrement à un seul entier, défi SHA-256 par certificat |
| SGDL, enrobage d’un raffinement flottant (cette étude) | Powell/NCC float64, puis frontière exacte + Lean | 0,58 et 0,97 mm (14/14) sur 2/9 ; deux dégradations réfutées | aucune | flottant à l’intérieur, ℚ à la frontière | par repère ; deux échecs silencieux pris | oui |
| SGDL, scène exacte multi-vues, 2 à 4 vues de la même séance (cette étude) | Formes : cônes, tubes, DLint, induction, métacourbe de Gray | 0,40 / 0,50 / 0,88 / 0,89 mm sur 4/6 spécimens ; 14/14, 14/14, 14/14, 13/14 prouvés | aucune | ℚ partout, pas de flottant | par repère + scène (rayons, sources, intervalle d’ambiguïté) | oui ; séance par égalité d’entiers |
Douze fois la chaîne a dit la vérité : quatre fois « proche », cinq fois « mieux », trois fois « non ». Une navigation qui peut dire non vaut plus qu’une corrélation qui dit toujours 0,9. L’étape suivante n’est pas un autre flottant : c’est un meilleur objectif exact, et un théorème qui porte la borne des repères jusqu’à la pose elle-même.