Add(notebooks,#15066): tranche D — atelier calculs de preuve Hilbert/LK (Tweety-02e)

[jsboige]

Grain: DEEP/notebook-lean — lane myia-po-2024:CoursIA — prev: MED/notebook-dotnet #17671

Résumé

Tranche D de l'EPIC #15066 : atelier calculs de preuve. Le notebook Tweety-02e-Preuves-Hilbert-Gentzen-Lean fait calculer la même micro-théorie {p, q, r} par trois moteurs, et mesure la taille de ce que chacun produit.

See #15066 (tranche D — l'EPIC reste ouverte : les tranches E/F ne sont pas livrées ici).

Section	Moteur	Ce qui est produit	Ce qui est mesuré
2-3	Axiomes + modus ponens (Hilbert)	une liste de formules justifiées	instances d'axiomes, MP, tours, durée
4	Calcul des séquents LK	un arbre de dérivation	hauteur et taille, avant/après élimination des coupures
2, 3	SimplePlReasoner / SatReasoner	un verdict True/False	— (aucune preuve produite)

Le versant Lean : un théorème du noyau, pas une procédure décrite

constructiveHauptsatz (Foundation, pin 81810b9f22c4) n'est pas invoqué comme un récit : le notebook l'appelle et évalue le résultat.

• la dérivation éliminée est extraite (.1 du sous-type) et sa hauteur/taille sont #eval-uées contre celles de la dérivation d'origine ;
• le témoin Derivation.IsCutFree est extrait (.2) et type-checké par le noyau ;
• #print axioms liste ce sur quoi repose le théorème lui-même.

La leçon est que l'élimination des coupures est un objet qu'on peut manipuler comme un lemme de Mathlib, pas un algorithme évoqué en commentaire.

Contre-expérience : un résultat négatif, mesuré puis expliqué

Le notebook ne se contente pas de montrer ce qui marche. La section 3 inclut une contre-expérience dont l'issue n'était pas acquise :

• le syllogisme hypothétique (p → q) → ((q → r) → (p → r)) est déclaré valide par les deux oracles (True) ;
• le moteur de chaînage avant ne le trouve pas dans le vivier de la section 3 ;
• l'hypothèse naturelle — « il manque quelques formules, élargissons le vivier » — est testée et réfutée : avec les sous-formules de la cible ajoutées, la formule reste introuvable ;
• un contrôle positif au même budget retrouve p → p (5 étapes), ce qui écarte l'explication « budget global trop court ».

Le notebook conclut donc à une borne structurelle de la recherche, pas quantitative. Ce paragraphe a été ajouté après mesure : une première rédaction affirmait qu'élargir le vivier suffisait — c'est faux, et la mesure l'a montré avant le commit.

Position sur l'organe natif (règle organ-first-implementation)

1. Quelle série possède la sémantique ? — Foundation (FFL), via formal_logic_lean qui l'épingle ; c'est lui qui possède Derivation, Canonical.constructiveHauptsatz et IsCutFree.
2. Peut-on invoquer son module réel ? — Oui, et c'est ce qui est fait : le notebook importe Foundation.FirstOrder.Hauptsatz et appelle le théorème réel. Aucune réimplémentation locale du Hauptsatz.
3. Faut-il exporter quelque chose de la série source ? — Non. La consommation se fait en convive (CONSUMER_PINNE), sans modification du pin.
4. Quel témoin négatif l'organe natif fournit-il ? — La paire constructiveHauptsatz (computable) / hauptsatz (noncomputable) fait l'objet de l'exercice 3 : #print axioms sur les deux, et l'échec attendu de #eval sur la seconde.
5. Quelle vérification indépendante ? — Les deux oracles Tweety, qui re-vérifient chaque formule de la preuve Hilbert trouvée (section 3), indépendamment du moteur qui l'a produite.

Déviations déclarées

Ce lot n'ajoute aucun module de pont au lake formal_logic_lean/ et n'édite aucun de ses fichiers : FormalLogic.lean, FormalLogic/ModalZoo.lean et l'index sont sous claim actif d'une autre lane — mesuré, pas supposé. Le lac vit sous SymbolicAI/Lean/, pas sous SymbolicAI/Tweety/ ; le chemin est nommé ici pour que la mesure soit rejouable telle quelle :

python scripts/check_lane_claim.py 15066 --lane myia-po-2024:CoursIA \
  --paths MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/ModalZoo.lean \
  --paths MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic.lean \
  --paths MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/README.md

  blocked            : true
  blocking_lanes     : ["myia-po-2025:CoursIA"]
  intersection_summary: "3 fichiers bloques / 1 libres dans le scope"
  claim bloquant     : marker=CLAIMED  at=2026-09-23T08:20:42Z
                       url=https://github.com/jsboige/CoursIA/issues/15066#issuecomment-5791489867
  -> rc=1

Le versant Lean de la tranche D vit donc dans le notebook (préambule Lean soumis au noyau par lake env lean, qui hérite du toolchain et du LEAN_PATH du pin). C'est une déviation assumée, tracée dans le changelog du README, pas un contournement silencieux.

Validation

• C.1 — mesuré : raise NotImplementedError / assert False / 1/0 absents des 13 cellules de code (0 hit) ; les trois exercices sont des stubs qui s'exécutent (print("Exercice a completer")).
• C.2 / H.3 — re-exécution réelle par batch_reexecute.py (kernel python3, --cwd notebook) : SUCCESS en 1038 s, REAL_EXIT=0 (le code de sortie réel du lanceur, pas celui du wrapper). Contrôles sur le notebook committé : 13/13 cellules de code portent un execution_count réel (1 → 13), 0 sortie vide, 0 sortie d'erreur.
  • Les trois cellules Lean s'exécutent vraiment — invocation lake env lean en WSL, dont chaque sortie porte son [exit 0]. Leurs sorties impriment les nombres que la prose cite : cellule 21 → 0, 2, 1, 4 (hauteur/taille d'identité puis de coupure) ; cellule 23 → 6, 7, 2, 4 (dérivation rendue par le Hauptsatz, puis rappel) suivi de 'FFL.FirstOrder.Derivation.Canonical.constructiveHauptsatz' depends on axioms: [propext, Classical.choice, Quot.sound].
  • Les trois stubs d'exercice s'exécutent et affichent Exercice a completer (C.1 respectée : le notebook va au bout).
  • Aucun scrub de sortie : la seule normalisation appliquée est metadata.papermill.input/output_path ramené au basename (tolérance 1 de secrets-hygiene.md, qui porte sur la métadonnée et non sur une sortie). Contrôle indépendant : 0 chemin machine (D:\, /mnt/, /tmp/) dans l'ensemble des sorties.
• Cellules code consécutives — detect_consecutive_code_cells.py : Run >= 2: 0 (le notebook portait un run de 2, résolu par une cellule de transition).
• Chaîne Python (sections 1-3) — les 6 cellules exécutées en processus : 6/6 sans erreur (cellules 2, 5, 8, 10, 12, 14).
• Provenance Lean — les trois pins sont vérifiés contre le disque, pas déclarés : Foundation 81810b9f22c4, mathlib 0df444a360ea, ProvabilityLogic 01628c51f618 — identiques à lake-manifest.json (assertion de la cellule 17). Foundation.FirstOrder.Hauptsatz a été construit depuis le pin (962/962, Hauptsatz.olean du 2026-09-25T06:49Z) : le théorème invoqué n'est pas un binaire préexistant.
• Audit README fichier-entier (§E) — voir le changelog v1.2.5 : comptes, durées et arborescence re-mesurés sur disque, résidus déclarés. Contrôle indépendant de ce PR : 1165 cellules / 438 code = 1153 + 12 (37 notebooks racine) et 433 + 5 (probe) — réconcilié avec la ligne 67.

🤖 Generated with Claude Code

[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: 13
• 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	3.2s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.4s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	3.9s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.6s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.8s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.6s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	17.9s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.8s

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

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[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.

[jsboige]

Rouge prose-counts réparé (a6430e3) — il était propre à cette PR, pas hérité de la base.

Le picker l'avait attribué à la base (« tache COORDINATEUR, unique réparateur possible ») ; la lecture du corps du job disait autre chose : [REFUS] 15 compteur(s) quantitatif(s) en prose — MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md, et le témoin de contrôle #17753 est vert sur le même check (prose-counts: success @2026-09-25T06:19:33Z). Les 15 compteurs étaient tous sur des lignes ajoutées par cette PR (le mode --diff de l'organe ne juge que les lignes ajoutées) : **18 notebooks, **36 notebooks ×2, 12 fichiers, 6 modules, et 10 dans l'entrée changelog v1.2.5.

Fix conforme à la prescription de l'organe (#9377 : supprimer la mesure, garder le prédicat) :

• comptes d'état du dépôt retirés du corps (« 36 notebooks principaux », « 18 notebooks », « 12 fichiers », « 6 modules ») ;
• deltas historiques du changelog reformulés en forme nom-d'abord (« notebooks principaux 33 → 34 », « lignes 31 → 33 ») — le fait historique reste, la forme périssable part ;
• « (+1 ligne 2e) » → « (+ entrée 2e) ».

Vérifié localement après commit, plage exacte du CI : check_prose_quantitative_claims.py --diff origin/main...HEAD --strict → rc=0, « aucun compteur quantitatif en prose ». Le verdict du run CI sur la nouvelle tête suit en commentaire.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #17757 (Add(notebooks,#15066): tranche D — atelier calculs de preuve Hilbert/LK (Tweety-02e)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• terminal -- feat(tweety,#15066): Tweety-3b-Modal-Lab-Lean — labo modal croisé Kripke/Lean (Tranche C) #17122 partage : MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md, recouvrement de chemins 50% -- feat(tweety,#15066): Tweety-3b-Modal-Lab-Lean — labo modal croisé Kripke/Lean (Tranche C) #17122 est deja sur main. (issues communes : [EPIC] Formalized Formal Logic — articuler les séries Tweety et Lean #15066) (issues communes : [EPIC] Formalized Formal Logic — articuler les séries Tweety et Lean #15066)

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[jsboige]

VERDICT: LGTM (contrainte token : COMMENT only)

[Hermes hermes-pr-review] — Notebook FULL READ au head a6430e3983 (33 cellules, 13 code, toutes executees, 0 null).

Gates #17040

• 8 lectures, toutes placees immediatement APRES leur code cell (index 3/6/11/15/18/20/22/24) ;
• cross-verif des cites numeriques dans les lectures vs outputs : Lecture[15] annonce "~2 700 formules, ~180 MP, 3 tours, 5 etapes" — output confirme formules_connues: 2713, modus_ponens: 178, tours: 3, etapes: 5 (approximations honnetes, pas fabriquees) ;
• 3 exercices avec stubs # TODO etudiant, aucune solution leak ;
• prose de liaison dense mais justifiee (moteur/oracle/Hauptsatz articules).

Substance verifiee

• Section 2 : les 3 schemas Lukasiewicz (A1/A2/A3) soumis aux deux oracles — 6 True dans le stream, contrat d'environnement visible (SimplePlReasoner installe: True, SatReasoner: True) ;
• Section 3 : moteur chainage avant derive p→p en 5 etapes avec cout mesure (instances_axiomes: 2535, formules_connues: 2169) ; chaque etape re-verifiee par les 2 oracles ([OK] x5) ;
• Contre-experience (section 3) : syllogisme hypothetique valide par les oracles mais NON derive par le moteur — vivier elargi (|candidats|=14, sous-formules ajoutees) toujours trouvee=False. La lecon "limite structurelle, pas budget trop court" est mesuree, pas affirme ;
• Section 4 : Hauptsatz constructiveHauptsatz invoque comme objet du noyau Lean (extraction .1/.2, #eval hauteur/taille avant/apres elimination, #print axioms), pas decrit en commentaire ;
• README Tweety (+19/-12) : corps substantiel pour Tweety-02e (resume, navigation, tableau par-notebook mis a jour) — conforme a la directive README-TOTALS #17633.

Securite : 0 hit.

Bloquant : aucun. LGTM de substance.

Marker cycle: hermes-pr-review 25/09 08:58Z

[Hermes hermes-pr-review, cycle :08 25/09, host f6be46d1b7a3]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
pr: 17757
head: a6430e3
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 59fab1aec3a86edc06b27e6514a4307bc986a35a422b83e03cf0badf96ee391c
diff-files: 2
diff-additions: 1601
checks: latest-wins-green -- fold a la tete : 0 jambe non-verte (89 check-runs) ; PR gate re-agrege SUCCESS 08:49:37Z par le sweep (tete a 137 min > plancher) ; mergeStateStatus a verifier au moment du merge
b0: clear -- organe rc=0 ; commentaire post-commit A RELIRE (c.5827995360, 06:33:01Z) lu : self-report du fix prose-counts par la lane, pas une reserve tierce ; prose-counts reverifie firsthand a la tete (organ --strict sur le README de la tete) : aucun compteur
scope: pass -- 2 fichiers (notebook Tweety-02e + README de serie), sujet unique tranche D #15066, +1601/-12
domain: not-applicable -- kernel python3 (JPype/Tweety), aucun fichier .lean dans le diff (les croisements Lean sont pedagogiques, cites) ; pas de metrique ML/QC
verdict: READY
[/ADJOINT PREFLIGHT]

Verification firsthand (adjoint po-2023) :

• C.2 : 13/13 cellules code execution_count 1..13 sequentiels, toutes avec sorties, 0 sortie d'erreur, 0 erreur volontaire (C.1 propre).
• prose-counts : le rouge initial (15 compteurs sur lignes ajoutees) est repare a la tete a6430e3983 — reverifie localement avec l'organ en mode strict sur le README de la tete : aucun compteur restant. Le temoin feat(qc,#16239): QC-Py-14b — liquidité et coûts d'exécution (proxys, capacité, stress COVID réel) #17753 vert sur le meme check confirme le caractere propre-a-la-PR du rouge initial.
• Le seul rouge restant etait le minuteur DWELL (88/88 checks verts au fold, jambe PR gate a 8 min d'age < plancher 120 min). Un replay a 08:20Z etait premature (109 min < plancher, re-echec attendu du minuteur) ; jambe rejouee post-echeance 09:07Z -- voir champ checks ci-dessus.
• Advisory path-collision feat(tweety,#15066): Tweety-3b-Modal-Lab-Lean — labo modal croisé Kripke/Lean (Tranche C) #17122 (terminal) : l'organe mesure le recouvrement de chemins, pas le contenu ; feat(tweety,#15066): Tweety-3b-Modal-Lab-Lean — labo modal croisé Kripke/Lean (Tranche C) #17122 est deja sur main, la livraison est disjointe (tranche D nouvelle).

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
pr: 17757
head: a6430e3
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 2925c35dcf36bfaa4cd368b4cfc983478cdf22af94eb15d1829fd20a5216f79c
diff-files: 2
diff-additions: 1601
diff-deletions: 12
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]

Re-emission canonique du dossier (la version c.5829867282 etait malformee : champ diff-deletions absent, valeurs non canoniques sur checks/b0/scope — le fond mesure ci-dessous est inchange).

Mesure a la tete exacte a6430e3983 :

• Checks : PR gate success depuis le balayage 08:49Z (la jambe DWELL, seul rouge du dossier precedent, a cede au plancher 120 min ; jambe rejouee inutilement a 08:20Z a 109 min — le green est venu du balayage). Fold commits/a6430e3983/check-runs dernier-par-nom : 0 jambe non-verte, 0 jambe sans conclusion. mergeStateStatus: CLEAN, mergeable: MERGEABLE.
• B.0 : check_unaddressed_nits.py 17757 rc=0 — aucune phrase de levee manquante sur les 8 commentaires et 1 review (COMMENTED jsboige, sans reserve Hermes). 0 thread inline non resolu.
• Substance verifiee (depuis le dossier initial, non remesure ici) : prose-counts 0 (check-run success), ratchets output/source clean, C.2 13/13 cellules code execution_count coherent avec outputs.
• Scope : 2 fichiers, +1601/-12, un seul sujet (celui du titre), rien hors perimetre.

Pret au merge des l'ouverture de la fenetre coordinateur.