Tranche F — pilote GL/ProvabilityLogic consommateur pour Löb et points fixes #15916

Contexte

Sous-grain atomique de la tranche F de #15066 et pilote L3 de #15062. Le pilote Foundation #15520, livré par #15563, a établi un consommateur propositionnel CONSUMER_PINNÉ sous Lean/Mathlib 4.33.1. Il ne mesure pas encore le dépôt séparé FormalizedFormalLogic/ProvabilityLogic, son fragment GL, ses points fixes ni son interprétation arithmétique.

Le dépôt canonique à tester est FormalizedFormalLogic/ProvabilityLogic au commit exact :

01628c51f618fd11f2f6b10c813f261f1d36c7a6

Pins déjà vérifiés :

• toolchain ProvabilityLogic : v4.33.1 ;
• Mathlib : v4.33.1 / 0df444a360eaa60ab8c11dca51a86af692955474, identique au lake consommateur ;
• snapshot Foundation de ProvabilityLogic : bfeaca91213835a3a5fc313f40b0cd2cc66ffd3c ;
• pin Foundation actuel de CoursIA : 81810b9f22c49fbb32bd89c1e9737059d83a37e6, six commits en avance. Le delta touche notamment des modules FirstOrder : sa compatibilité n'est pas présumée, elle doit être démontrée par le build. Le fallback mesuré est un alignement sur bfeaca9, avec reconstruction du pont propositionnel.

Livrable

Étendre le lake existant :

MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean

avec une dépendance pinnée vers ProvabilityLogic et un module consommateur minimal FormalLogic.GLBridge qui expose, sans axiome local ad hoc :

1. l'axiome/théorème modal de Löb importé depuis ProvabilityLogic.Hilbert.GL.Basic ;
2. un verdict positif de membership GL calculé par l'instance décidable de LogicGL ;
3. une non-prouvabilité certifiée par un contre-modèle fini concret ;
4. une spécialisation concrète du théorème de point fixe de de Jongh–Sambin ;
5. si la fermeture arithmétique reste soutenable, le pont HBL/diagonalisation vers LogicGL.arithmetical_soundness et formalized_löb_theorem.

Imports candidats à mesurer séparément :

import ProvabilityLogic.Logic.GL.Basic
import ProvabilityLogic.Logic.GL.Fixedpoint
import ProvabilityLogic.ProvabilityLogic.GL.Basic

Le pilote commence par un clone/build du pin upstream, puis mesure la fermeture réellement compilée du consommateur modal et du versant arithmétique. Le verdict final doit être l'un de : IMPORTABLE, CONSUMER_PINNÉ, PORT_BORNÉ, RÉFÉRENCE_SEULE.

Critères de validation

• Build frais du pin upstream avec lake exe cache get puis lake build, résultat et durée consignés.
• lake build FormalLogic.GLBridge puis lake build du lake étendu : succès au pin choisi, nombre de jobs et durées consignés.
• Fermeture d'imports mesurée séparément pour le fragment modal et le fragment arithmétique ; aucune confusion entre modules source et jobs Lake.
• Au moins un verdict GL positif par decide et une réfutation par contre-modèle fini concret, tous deux falsifiables en changeant la formule.
• fixpointTheorem spécialisé sur une formule modalisée concrète.
• Löb est importé via une déclaration upstream vérifiée (ProvableHilbert.modalL et/ou formalized_löb_theorem), jamais déclaré comme axiome propre.
• #print axioms sur chaque déclaration exposée : zéro sorryAx, zéro native_decide.*; toute présence de Classical.choice, propext ou Quot.sound est nommée, pas masquée.
• python scripts/lean/count_code_sorry.py --json : distinct_code_sorry du lake formal_logic_lean reste à 0.
• Audit de licence et de maintenance des dépendances matérialisées, y compris LeanTypst et Forgive; leur présence hors fermeture compilée n'est affirmée qu'après mesure.
• Pins exacts dans lakefile.lean et lake-manifest.json; aucune branche mouvante dans le consommateur.
• README du lake mis à jour avec le verdict, les fermetures et les coûts mesurés; aucun catalogue généré modifié.
• Si le port exige plus de 3 modules propres / 1000 lignes adaptées, un fork permanent ou un nouveau sorry, arrêt en RÉFÉRENCE_SEULE sans maquiller l'échec.

Chemins

• MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/lakefile.lean
• MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/lake-manifest.json
• MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/GLBridge.lean
• MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic.lean
• MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/README.md

Hors périmètre

• FairBot, ProgramGames et tout fichier GameTheory : ils restent dans [EPIC] Math for AI Safety — jeux-programmes, coopération transparente et prouvabilité Lean #15062-L2 après verdict du pilote ;
• notebook pédagogique ;
• formalisation locale de Löb, Gödel II ou Solovay ;
• vendoring/fork permanent de Foundation ou ProvabilityLogic ;
• adaptation de modules upstream au-delà du seuil de sortie ;
• régénération manuelle du catalogue.

Part of #15066.
See #15062.