feat(lean,#15066): pont modal Tweety<->FFL — FormalLogic.ModalBridge (tranche C)

[jsboige]

Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: DEEP/research-code #16903

Summary

Tranche C de l'EPIC #15066 : le lake formal_logic_lean consomme désormais le
paquet ModalLogic (FFL) et un module FormalLogic.ModalBridge certifie la
discrimination des logiques modales K/T/K4/S5 par le kernel.

Pourquoi un fork (mesures, pas hypothèses)

• upstream FormalizedFormalLogic/ModalLogic : origin/main reste lean-toolchain v4.31.0
  (mesuré 2026-09-20, dernier push 2026-08-01), 14 branches toutes pré-bump, 0 PR ouverte —
  aucune rev ne compile sous le toolchain 4.33.1 du lake ;
• la fermeture transitive depuis ModalBridge force Modal.LogicSymbol (public imports :
  Kripke.Basic → Logic.Basic → Formula.Basic → Modal.LogicSymbol) — aucun import plus étroit ;
• le fork MyIntelligenceAgency/ModalLogic @ 71968137b917a708c700047e1e6d3eb6cc4ed078
  (branche coursia-v4.33.1-compat, = upstream 9c485ca95e35 + 3 commits de compat,
  Modal/LogicSymbol.lean, Vorspiel/AdjunctiveSet.lean, Logic/Semantics.lean — +17/−3,
  zéro changement sémantique) :
  1. 83367d1 — Modal/LogicSymbol.lean:347,430 : by dsimp [boxItr] laisse un résidu
     définitionnel (map f [φ] = [f φ]) sous 4.33.1 → by simp [boxItr] (fermé par
     List.map_cons/List.map_nil) ;
  2. 7d29f68 — Vorspiel/AdjunctiveSet.lean : mathlib v4.33.1 a retiré les instances
     HasSubset (Set α)/HasSubset (Finset α) (la notation ⊆ s'élabore désormais en
     LE.le via Set.instLE/Preorder.toLE) — la classe étend HasSubset α, d'où
     Fields missing: Subset ; restaure les deux instances sur les ordres LE existants ;
  3. 7196813 — Logic/Semantics.lean : fermeture de setOf_iff — la dépréciation
     setOf → Set.ofPred (v4.33.1) casse le simp qui réduisait φ ∈ setOf P.

Contenu FormalLogic/ModalBridge.lean

• forces_kdist : l'axiome K (distribution) est valide sur tout cadre — sans hypothèse
  de structure (normalité sémantique, preuve 2 lignes) ;
• contre-modèles finis certifiés par le kernel, chacun violant exactement la condition frame
  de son axiome : T_invalid (cadre irréflexif, relation 0≺1 seule), four_invalid
  (chaîne 0≺1≺2 non transitive), five_invalid (éventail 0≺1, 0≺2 non euclidien) —
  mondes sur ℕ (sous-cadre fini {0,1}/{0,1,2}, autres mondes isolés), preuves réduites
  à by decide sur des égalités ℕ. Cadres en abbrev (reducibles) : c'est ce qui rend
  les numéraux (0 : model.World) synthétisables (OfNat traverse la projection jusqu'à
  ℕ) — un def le refuse, piège mesuré sur la première version de cette section ;
• côté S4 (Fin74.Kripke, cadres réflexifs et transitifs par construction — rel_refl/
  rel_trans sont des champs de données) : forces_dia_of_refl (dual diamant de T) et
  forces_dia_dia (dual de 4) — la structure du cadre les donne en une ligne chacun.

Le notebook consommateur Tweety-3b-Modal-Lab-Lean.ipynb (patron #16888 Tweety-02d) est le
grain suivant de la lane — pas dans cette PR (un sujet par PR).

Manifeste — effet mesuré de l'ajout

lake-manifest.json : 19 → 20 paquets, aucun supprimé, ModalLogic ajouté (url fork, rev
7196813…, inputRev = rev, configFile: lakefile.toml). Six deps héritées changent de pin
parce que le manifest de ModalLogic les apporte : «doc-gen4» v4.33.1 → v4.31.0,
BibtexQuery master → nightly-testing, et LeanTypst/MD4Lean/UnicodeBasic/leansqlite
re-résolues à la tête de leur branche. Ce sont des outils de documentation, hors du build de
la librairie — mesuré : 0 occurrence de doc-gen4/DocGen4/Bibtex/LeanTypst dans le log de
build. Les revs des paquets qui sont dans le build (plausible, batteries, Qq,
proofwidgets) restent ceux de mathlib v4.33.1 : c'est pourquoi require mathlib est laissé
en dernier (l'ordre décide de la résolution des revs transitives).

Exigences Lean B.1-B.3

• B.1 (sorry) : python scripts/lean/count_code_sorry.py --repo D:/Dev/CoursIA-ffl-modal-lab --json
  → MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean | files 5 | code_sorry 0 | distinct_code_sorry 0 (fichier nouveau, aucun sorry ; les 3 commits du fork n'en
  introduisent aucun non plus — diff mesuré +17/−3, fichiers nommés plus haut) ;
• B.2 (build) : lake build FormalLogic.ModalBridge SUCCESS sur le contenu du head —
  RC=0, 0 ligne error, « Build completed successfully (1021 jobs) », toolchain v4.33.1 /
  mathlib v4.33.1 (chaîne ModalLogic complète compilée). Le build du défaut (agrégateur
  FormalLogic.lean, qui importe le module) tourne au même contenu — verdict posté en
  commentaire dès qu'il tombe ;
• B.3 (proof-integrity) : NON APPLICABLE (a) — le workflow lean-axiom.yml n'est pas
  câblé sur formal_logic_lean (vérifié : formal_logic absent des target-modules et aucun
  workflow lean-formal-logic*.yml).

Verdict SOTA

SOTA-OK — le vrai paquet upstream FFL ModalLogic est consommé (pin exact du fork
documenté ci-dessus), témoins et certificats produits par le kernel Lean, aucune
réimplémentation locale.

Notes review

• FormalLogic.lean (agrégateur) : +1 import — chevauchement attendu avec feat(tweety,#15066): laboratoire FOL Tweety vers certificats Lean #16888 (FolBridge
  ajoute le sien) : rebase trivial pour le second mergé ;
• lake-manifest.json : entrée ModalLogic = fork (url + rev 7196813…), le reste inchangé ;
• le diff AdjunctiveSet du fork est documenté dans le memory de la lane
  (mathlib-v4-33-hassubset-le-migration) — tout consommateur FFL sous 4.33 le rencontrera.

See #15066

🤖 Generated with Claude Code

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2024:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-20) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=3 cap=3)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #17017 (feat(lean,#15066): pont modal Tweety<->FFL — FormalLogic.ModalBridge (tranche C)) 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.

• fort -- feat(tweety,#15066): laboratoire FOL Tweety vers certificats Lean #16888 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic.lean (issues communes : [EPIC] Formalized Formal Logic — articuler les séries Tweety et Lean #15066)

[jsboige]

Verdict du build du défaut (agrégateur FormalLogic.lean) — promis dans le body (B.2).

Build complet lake build sur le contenu exact du head 2d6592dc1169 (worktree propre, rev-parse vérifié au head avant la conclusion du run) :

• RC0, 1400 jobs, « Build completed successfully (1400 jobs) »
• erreurs : 0 ligne(s) error dans le log complet
• toolchain v4.33.1 / mathlib v4.33.1 — le défaut importe FormalLogic.ModalBridge, la chaîne ModalLogic complète (fork 7196813…) est compilée dans ce build

La preuve B.2 est complète sur les deux cibles : module isolé lake build FormalLogic.ModalBridge = 1021 jobs SUCCESS (body), défaut = 1400 jobs SUCCESS.

✔ [1398/1400] Built ProvabilityLogic.ProvabilityLogic.GL.Basic (178s)
✔ [1399/1400] Built FormalLogic.GLBridge (275s)
Build completed successfully (1400 jobs).

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17017
head: 2d6592d
complete: true
body: read
comments-reviewed: 3
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: fab62b5430b0708a4a1783be1831ac705c29f291ae7fa4be8bcaaa06cf793cdf
diff-files: 4
diff-additions: 214
diff-deletions: 55
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA
pr: 17017
head: 2d6592d
complete: true
body: read
comments-reviewed: 4
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 07c750693092f6632767efcc61c0957405f40d4b545fe3f4f8433ad4a4ee89f6
diff-files: 4
diff-additions: 214
diff-deletions: 55
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Re-stamp PERIME-SURFACES du dossier precedent (meme head, verdicts identiques) — seule l'empreinte de discussion avait bouge. Checks verifies latest-wins-green firsthand a l'instant.