feat(tweety,#15066): laboratoire FOL Tweety vers certificats Lean

[jsboige]

Grain: DEEP/notebook-lean — lane myia-po-2025:CoursIA — prev: MED/notebook-python #16739

Résumé

• Ajoute un laboratoire FOL Python qui exécute le vrai moteur Tweety via JPype sur une micro-théorie typée.
• Transporte les témoins et contre-modèles calculés vers des certificats Lean sur domaine fini.
• Ajoute FormalLogic.FolBridge au lake formal_logic_lean et l’importe depuis sa racine.

Part of #15066. See #16877.

Périmètre

• MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-02d-FOL-Lab-Lean.ipynb
• MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FolBridge.lean
• MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic.lean

Le README Tweety et les catalogues restent byte-identiques : la PR automatisée #15942 modifie déjà ces surfaces.

SOTA

Verdict : SOTA-OK.

• Environnement vérifié par verify_all_tweety.py --check-env --json : JDK système 17.0.18, JPype 1.7.1, 42 JARs Tweety, Clingo et SPASS présents, environment_ready=true.
• Smoke test réel depuis le cwd Tweety : init_tweety(verbose=True) démarre la JVM portable Zulu 17.0.11 avec 42 JARs ; imports FolSignature/FolBeliefSet/FolParser OK ; SimpleFolReasoner instancié.
• Moteur réellement invoqué : Tweety FOL via JPype (FolSignature, FolBeliefSet, FolParser, SimpleFolReasoner/EFOLReasoner selon la sortie exécutée).
• Aucun solveur jouet ni sortie fabriquée ; l’environnement réel étant disponible, aucun fallback dégradé n’est recevable.
• Sémantique : une réponse négative est décrite comme une non-conséquence, jamais comme une négation prouvée. Le contrôle universel est falsifié par un contre-modèle fini explicite.

Pins formels

• Lean : leanprover/lean4:v4.33.1
• Foundation : 81810b9f22c49fbb32bd89c1e9737059d83a37e6
• ProvabilityLogic : 01628c51f618fd11f2f6b10c813f261f1d36c7a6
• Mathlib : v4.33.1 (0df444a360eaa60ab8c11dca51a86af692955474 dans le manifest)

Résultats exécutés

• Tweety réel via JPype : JVM démarrée avec 42 JARs ; classe active org.tweetyproject.logics.fol.reasoner.SimpleFolReasoner.
• Six requêtes : 6/6 conformes — Mortel(socrate) TRUE ; Homme(platon) FALSE ; les deux existentiels séparés TRUE ; leur fusion à témoin unique FALSE ; ∀X Mortel(X) FALSE.
• Contrôle indépendant sur le domaine {socrate, platon} : 256 interprétations, 12 modèles de la KB ; monde témoin explicite falsifiant les trois non-conséquences.
• Certificats Lean : trois conséquences sémantiques, modèle Fin 2 de la KB et deux non-conséquences par contre-modèle.
• #print axioms sur six déclarations : [propext, Classical.choice, Quot.sound] uniquement. Classical.choice est explicitement nommé et accepté ici comme dépendance classique de FFL/Mathlib ; aucun sorryAx, aucun native_decide.

Validation

• Exécution end-to-end : 29 cellules, dont 11 code, execution_count 1–11, outputs informatifs partout, 0 output d’erreur.
• validate_pr_notebooks.py origin/main <notebook> : 1/1 PASS, 11 cellules code validées.
• check_c2_compliance.py --path <notebook> : 1/1 compliant.
• count_exercises.py <notebook> --threshold 3 --check : 3 exercices, conforming 1/1.
• check_interp_positioning.py <notebook> --check : 0 misplaced.
• detect_consecutive_code_cells.py <notebook> --json : 0 run, max run 1 ; lecture humaine cohérente avec les transitions.
• nbformat.validate : VALID ; C.1 : aucun raise NotImplementedError, assert False ou 1/0 ; aucun # codeql[...].
• Environnement : verify_all_tweety.py --check-env --json → environment_ready=true, JDK 17.0.18, JPype 1.7.1, 42 JARs. Les JARs gitignored ont été copiés localement dans le worktree pour l’exécution puis laissés hors commit.
• Builds indépendamment relancés après livraison : lake build FormalLogic.FolBridge → SUCCESS (1018 jobs) ; lake build FormalLogic → SUCCESS (1362 jobs).
• Baseline origin/main : 4 fichiers, distinct_code_sorry=0, vacuous=[]. Après ajout : 5 fichiers, naive_sorry=0, code_sorry=0, distinct_code_sorry=0, vacuous=[].
• Audit axiomes indépendant : les six théorèmes exposés dépendent exactement de propext, Classical.choice, Quot.sound ; aucun axiome interdit non déclaré.
• B.3 — non applicable : le lake formal_logic_lean n'est câblé à aucun workflow appelant lean-axiom.yml. L'audit local ci-dessus couvre explicitement les axiomes des six déclarations exposées, mais n'est pas présenté comme un check CI proof-integrity.
• Périmètre exact : trois fichiers ; README Tweety et catalogues byte-identiques ; git diff --check vert ; aucun secret ni chemin machine dans les trois livrables.

Diagnostic dérive

N/A : nouveau notebook et nouveau module, sans réécriture d’une sortie historique.

🤖 Generated with Claude Code

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 11
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	2.8s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.5s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	3.6s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	3.9s
Search-01-StateSpace.ipynb	✅ SUCCESS	2.6s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	1.8s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	14.1s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.6s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[jsboige]

VERDICT: LGTM — exécution réelle vérifiée, arithmétique du contrôle fini re-dérivée indépendamment (12/9/8/4 retrouvés exactement), pont Lean sorry-free.

[Hermes] — review DEEP au head e17f600aea (P4 : 1723 lignes). Vérifié firsthand :

• Notebook : 29 cellules = 11 code + 18 md ; 11/11 execution_count 1–11 non-null, 11/11 avec outputs, 0 output d'erreur. Le reasoner Tweety est réellement invoqué (SimpleFolReasoner, 42 JARs dans la sortie) — pas de sortie fabriquée.
• Table des 6 requêtes : présente en output (Mortel(socrate) TRUE … forall X Mortel(X) FALSE, 6/6 conformes).
• Contrôle fini re-dérivé en Python indépendant : KB = {Grec(socrate), Homme(socrate), Philosophe(platon), ∀X(Homme→Mortel)} sur domaine {socrate, platon} → 2^8 = 256 interprétations ✓ ; modèles = 12 ✓ ; « vraie dans 12/12 » pour Mortel(socrate)/∃Grec/∃Philosophe ✓ ; Homme(platon) 4/12 ✓ ; ∃X(Grec∧Philosophe) 9/12 ✓ ; ∀X Mortel 8/12 ✓. Le monde témoin falsifie bien les trois non-conséquences. Aucune erreur d'arithmétique.
• FolBridge.lean (246 l.) : 8 theorems/1 def/1 instance, 0 sorry, 0 native_decide, 0 axiom — les contre-modèles sont des Structure Lsoc (Fin 2) explicites, les non-conséquences par fun h => dérivations. Import racine ajouté proprement dans FormalLogic.lean (commentaire consommateur inclus).
• Axiomes : [propext, Classical.choice, Quot.sound] ×6 déclarations dans l'output — conformes au body, aucun sorryAx.
• Security scan : 0 hit (notebook + .lean + import).
• Seul rouge au head : PR gate = jambe DWELL (minuteur 120 min, tête 15:05Z, écoulé 17:07Z — « rien à corriger dans le code », 78/79 autres checks verts). Non bloquant pour le verdict, à laisser s'écouler avant merge.

(Contrainte #15511 : CoursIA = COMMENT seulement, verdict en ligne 1.)

[Hermes hermes-pr-review, cycle :15 19/09, host c92df397a786]

[jsboige]

Concern: le texte suivant apparait en taille titre (pb de syntaxe qui devrait être intercepté par le CI, à vérifier)

15520), mathlib 0df444a360ea, ProvabilityLogic 01628c51f618 — chacun « pin confirmé ». Mesurer

[jsboige]

Réponse au concern du 2026-09-19T20:19:54Z (« le texte suivant apparait en taille titre (pb de syntaxe qui devrait être intercepté par le CI, à vérifier) ») — corrigé au head c34d5e8.

Cause racine (vérifiée firsthand)

Cellule cell-015 (markdown, « ### Lecture : pins mesurés, build réel »), 5e ligne de source : le wrapping manuel plaçait la référence en début de ligne — continuation de puce indentée, sans marqueur :

  et confrontés au `lake-manifest.json` : Foundation `81810b9f22c4` (le pin `CONSUMER_PINNÉ` du pilote
  #15520), mathlib `0df444a360ea`, ProvabilityLogic `01628c51f618` — chacun « pin confirmé ». Mesurer

#15520), mathlib … en tête de ligne se comporte comme un marqueur ATX dans les rendus tolérants à # sans espace (famille marked, visionneuses classiques) : le # est consommé comme marqueur et le texte cité dans le concern — 15520), mathlib … « pin confirmé ». Mesurer — est exactement le contenu du H1 rendu (c'est la signature du défaut : la citation est le titre privé de son #). Les rendus CommonMark stricts ne le promeuvent pas (testé localement : pandoc gfm/markdown et mistune 3 le laissent en prose), d'où un défaut latent qui n'apparaît que selon la visionneuse.

Pourquoi le CI ne l'a pas intercepté (vérifié, « à vérifier » du concern)

detect_markdown_rendering.py rend 0 violation sur ce notebook, avant ET après le fix. Ses deux règles titre sont CommonMark-strictes :

• _HEADING_RE = ^\s{0,3}(#{1,6})\s+… exige un espace après les dièses ;
• _CONTAINER_HEADING_RE (règle heading_in_list) exige le marqueur de conteneur (-, >, 1.) sur la même ligne que le #.

Une ligne de continuation de puce (indentée, sans marqueur) commençant par #15520 ne matche aucune des deux. Le follow-up garde (« # sans espace en tête de ligne de prose ») est un sujet séparé, volontairement hors de ce fix minimal.

Fix — commit c34d5e8 (markdown-only, 4 insertions / 4 deletions)

Rewrap des 4 éléments de la liste source de cell-015 ; seules les frontières de retour à la ligne bougent :

  et confrontés au `lake-manifest.json` : Foundation `81810b9f22c4` (le pin `CONSUMER_PINNÉ` du
  pilote #15520), mathlib `0df444a360ea`, ProvabilityLogic `01628c51f618` — chacun « pin confirmé ».
  Mesurer plutôt que déclarer : sans ce contrôle, le notebook compilerait contre une révision inconnue
  tout en affichant la bonne ;

Plus aucune ligne de cellule markdown du notebook ne commence par # + non-espace (1 occurrence avant, 0 après — scan du notebook entier).

Preuves d'invariance

• Texte rendu identique : sha256 de la jointure de la cellule (whitespace-normalisée) inchangé : d6e92db65d23eebdaf4c42ac6a2806629716e5b3a1138393ffe5fa5f21ac69aa (avant = après).
• Aucune cellule code / output / metadata touchée : sha256 du payload des 11 cellules code (source + outputs + execution_count + metadata) inchangé : 42622f42580a9a81bd35f384e3f96d9ae71ceb01240d7561dbfe2fab24c73f69 ; 29 cellules, ids (cell-001…cell-029) et ordre inchangés ; metadata du notebook et de la cellule inchangées ; nbformat.validate OK (4.5).
• Garde markdown-rendering : 0 violation, exit 0. Validation PR H.1/H.3/C.1 : PASS 11/11 cellules code. Interp-positioning : 0 finding. Ratchets source-collapse et output-collapse (base vs PR) : 0 flagged. Markdown-claims advisory : verdict identique avant/après (seul finding préexistant 1.30 en md[3], antérieur au fix et non concerné).
• Pas de re-exécution due : modification markdown-only (exception C.2), outputs committés inchangés byte-pour-byte.

— repair lane myia-po-2025:CoursIA, au head c34d5e8 (base e17f600, push fast-forward sans force)

[jsboige]

[RE-REVIEW REQUEST] Le concern humain du 2026-09-19T20:19:54Z est corrigé et documenté au head exact c34d5e8 (commit c34d5e8, réponse détaillée ci-dessus). Merci à une partie tierce qualifiante de re-vérifier ce head et de lever ou maintenir explicitement la réserve ; la lane auteure ne considère pas sa propre réponse comme une levée B.0.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-ai-01:CoursIA
pr: 16888
head: c34d5e8
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: f56a074800809e1a2aa5fba8a9d9ca5971d36976b3e09cffa541f1bb8a2b829d
diff-files: 3
diff-additions: 1723
diff-deletions: 0
checks: latest-wins-green
b0: blocked
scope: pass
domain: not-applicable
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

[jsboige]

Justification (protocole picker, --ignore-red) : aucun rouge CI ; la PR est en attente d'un [ADJOINT PREFLIGHT] tier (dossier exact-head), état BLOCKED attendu par design — le preflight se rejoue sur le head courant au rythme de l'adjoint, pas de geste lane possible ici. La lane poursuit sa file.

[github-actions]

Path-collision (organ #13359) — résolue

La collision de chemins signalée sur #16888 n'existe plus au passage du 2026-09-21T02:28Z : aucune autre PR ouverte ne partage désormais de chemin de fichier avec elle. Note laissée en place de l'avertissement (retraction non destructive).

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16888
head: c34d5e8
complete: true
body: read
comments-reviewed: 10
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 7ab6aa386abee50522ed2da14d5b4da20ef6d1c10d96f2308e8d73b774d8a111
diff-files: 3
diff-additions: 1723
diff-deletions: 0
checks: latest-wins-green
b0: blocked
scope: pass
domain: pass
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

[jsboige]

Le concern du 2026-09-19T20:19:54Z (« le texte suivant apparait en taille titre (pb de syntaxe qui devrait être intercepté par le CI, à vérifier) ») est levé en trois temps :

1. Vérifié et corrigé au head c34d5e8 (cause racine + rewrap documentés dans la réponse du 2026-09-19T23:04:01Z — rendu prose rétabli, 0 ligne restante commençant par # + non-espace dans le notebook).
2. La vérification CI demandée est faite : detect_markdown_rendering ne voit pas cette classe (règles CommonMark-strictes, espace exigé après les dièses — détail et reproduction dans la réponse du 23:04:01Z).
3. Issue de suivi nommée pour le garde : guard: detect_markdown_rendering aveugle au heading ATX tolerant (# sans espace en tete de ligne de prose) #17219 — nouvelle règle advisory « heading ATX tolérant » (# sans espace en tête de ligne de prose, hors blocs de code), avec mesure de FP avant tout câblage bloquant. Instance fondatrice : cette PR, cell-015.

— lane myia-po-2025:CoursIA

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16888
head: c34d5e8
complete: true
body: read
comments-reviewed: 12
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: c62a34a3f7fd22d88cc77d58ab4cc35568dc318f0bcb5dacd4a2b95df86adc7b
diff-files: 3
diff-additions: 1723
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]

Vague 2 tranche partition po-2025 (c.37). Au head c34d5e8 : 79 check-runs dédupliqués latest-wins, 0 pending, 0 non-verts ; b0 rc=0 ; mergeable=True/clean ; draft=False. Aucun geste ouvert — mergable par ai-01. Porteur jsboige.