[#14169-G1] Mesurer le recouvrement : 28 PRs endjin/Z3.Linq vs fork MyIntelligenceAgency/Z3.Linq e09dae6

[jsboige]

Etat mesure au 2026-09-27T09:20Z (lane myia-po-2024:CoursIA, claim de la lane) — le corps ci-dessous date du 2026-09-22 ; deux prémisses ont bougé depuis.

Ce que le corps dit vs ce qui est mesuré :

1. Pin du fork : le corps cible e09dae6 — le submodule a été bumpé à 3b42bcc par feat(submodule,#16609): Z3.Linq bump — DIVERGENCE_STATUS.md (cartographie P0) #17906 (mergée 2026-09-27T04:14Z, cartographie DIVERGENCE_STATUS.md : fork 51 ahead / 0 behind upstream). La base de comparaison G1 est désormais 3b42bcc.
2. Ensemble amont ouvert : le corps liste 28 PRs QC Framework: Composite FamaFrench + AllWeather (Factor-Hedged) #44-feat(datascience-agents): Amélioration des notebooks ML pour Ing4 #99 (état au 2026-09-01). Mesure directe du 2026-09-27T09:10Z (gh api pulls?state=open) : 44 PRs ouvertes — les 28 du corps sont toutes encore ouvertes (aucune fermée amont), et 15 nouvelles sont arrivées depuis (TrendFilteredMeanReversion v2 : RSI(2)<20 pour augmenter la frequence #40, PairsTrading/ETF-Pairs : nouvelles paires ou reclassification pedagogique #42, feat(GameTheory): Execute notebooks and save outputs #100-chore(QC): standardize ESGF-2026 examples structure #112). La note « 28 PRs GenAI Texte: Notebook CodAg - visualisation de workflows IA agentiques #74-chore(QC): standardize ESGF-2026 examples structure #112 » de feat(submodule,#16609): Z3.Linq bump — DIVERGENCE_STATUS.md (cartographie P0) #17906 (26/09) était déjà périmée à sa publication. Le périmètre du verdict doit être ré-arbitré : les 28 d'origine (acceptance actuelle) + décision coordinateur sur les 15 nouvelles.
3. Garde-fou « pas de bump tant que G1 non rendu » : supersedé par les événements (feat(submodule,#16609): Z3.Linq bump — DIVERGENCE_STATUS.md (cartographie P0) #17906 a bumpé sous substitution R3 deux-lanes, règle HARD 3 de submodule-maintenance — état de gate mesuré au 26/09 dans le DIVERGENCE_STATUS.md livré). Le garde-fou d'origine restait raisonnable ; il est documenté comme dépassé, pas effacé.

Portée de ce qui n'a PAS été vérifié : le sort PR-par-PR des 28 du corps (fermée/mergée/toujours ouverte amont) et le tableau de verdicts G1 lui-même — aucune partie de l'acceptance n'est livrée à ce jour. L'acceptance (4 critères) reste intégralement due.

---

Sous-grain de l'EPIC #14169 (G1)

Mission : pour chacune des 28 PRs amont endjin/Z3.Linq ouvertes le 2026-09-01 entre 11:18Z et 21:48Z (cf body EPIC), produire un verdict de recouvrement vs notre fork MyIntelligenceAgency/Z3.Linq épinglé à e09dae6.

Sortie attendue : tableau 3 colonnes — PR amont · notre équivalent · verdict parmi :

• REDONDANT : la capacité existe déjà dans notre fork, et l'amont la livre sous une autre forme
• DIVERGENT : la capacité existe dans notre fork mais avec une sémantique différente
• NOUVEAU-POUR-NOUS : l'amont livre une capacité qu'on n'a pas

Périmètre

Inclusions : les 28 PRs amont listées dans le body EPIC (#14169) — 4 blocs : Modernisation build (#44/#45/#47/#94), Runtime Z3 (#61), Suite tests (#48/#59/#65/#67/#69/#71), Marshalling et sortes (#73/#74/#77/#79/#80/#81/#84/#88/#90/#91/#92/#93/#95), Sémantique résolution (#86/#96/#98/#99).

Exclusions :

• PR QC Framework: Composite MomentumSector + RegimeSwitching #43 (notre propre PR upstream, déjà trackée par G2 dans l'EPIC)
• PRs qui ne livrent pas de capacité (purement doc, refactor sans changement de comportement observable)

Acceptance

1. Pour chaque PR amont couverte : fichier:ligne dans notre fork qui porte l'équivalent (le cas échéant).
2. Verdict REDONDAT/DIVERGENT/NOUVEAU-POUR-NOUS chiffré par colonne.
3. Une note de faisabilité par verdict NOUVEAU-POUR-NOUS : la PR upstream est-elle rebasable directement sur notre fork, ou nécessite-t-elle un port ?
4. C'est le préalable de tous les autres grains G2-G5 : G2/G3/G4/G5 sont bloqués tant que G1 n'est pas rendu (cf body EPIC).

Garde-fous

• Mesure dans le code, pas dans les titres de PR (body EPIC §Garde-fous).
• Aucune nouvelle PR sortante sans feu vert user (G4 le nécessite, G1 n'en émet pas).
• Pas de bump de submodule tant que G1 n'est pas rendu (le rebase sur cible en mouvement = conflit pur).

Liens

• EPIC [EPIC] Z3.Linq amont se remet en mouvement — 28 PRs endjin en 11 h après notre #43 : mesurer le recouvrement, trancher la posture de fork #14169 (corps 2026-09-01) · Epic: Fork Z3.Linq propre + reintegration EPFdevelopment + serie notebooks + PRs upstream #1206 (EPIC parent fermé) · Epic: Fork Z3.Linq propre + reintegration EPFdevelopment + serie notebooks + PRs upstream #1206-axe-4 livré
• fix(theorem): partial-eval constraint body before visiting (cross-submission capture) endjin/Z3.Linq#43 (notre PR upstream) · Other improvements available endjin/Z3.Linq#29 (issue originelle 2023)
• Fork : MyIntelligenceAgency/Z3.Linq @ e09dae6, submodule MyIA.AI.Notebooks/SymbolicAI/SMT/Z3.Linq
• submodule-maintenance.md §F (pas de bump tant que gate indécis)

[jsboige]

[CLAIMED] lane myia-po-2027:CoursIA-2 -- G1 Z3.Linq amont : mesurer le recouvrement des 28 PRs endjin vs fork MyIntelligenceAgency/Z3.Linq e09dae6 ; tableau 3 colonnes REDONDANT/DIVERGENT/NOUVEAU-POUR-NOUS + fichier:ligne ; aucune PR sortante

[jsboige]

Grain: DEEP/research-code — lane myia-po-2024:CoursIA — prev: DEEP/notebook-python #16901

[CLAIMED] lane myia-po-2024:CoursIA -- G1-bis #16050 : trancher les 18 PRs TBD du scanner (#16052) en verdicts definitifs REDONDANT/DIVERGENT/NOUVEAU-POUR-NOUS vs fork e09dae6 -- paths: docs/ledgers/14169-g1-recouvrement.md, scripts/smt/scan_z3linq_upstream.py

Reprise apres claim perime (po-2027:CoursIA-2, 2026-09-13) dont la livraison #16052 (mergee) couvre le scanner preliminaire SEUL : 18 PRs restent TBD. Methode : pour chaque PR amont, lecture du diff upstream + recherche de l'equivalent dans le fork e09dae6 (mesure dans le code, pas dans les titres) ; verdict + fichier:ligne + note de faisabilite par NOUVEAU-POUR-NOUS (rebasable direct ou port requis). Livrable : tableau 3 colonnes complet dans docs/ledgers/14169-g1-recouvrement.md + JSON enrichi du scanner. G2-G5 debloquent sur ce grain (acceptance 4 du body).

[jsboige]

[DELIVERED] lane myia-po-2024:CoursIA -- G1-bis rendu : PR #16903 (ledger docs/ledgers/14169-g1-recouvrement.md, 18 verdicts definitifs)

Acceptance du body verifiee point par point : (1) chaque PR amont couverte porte son fichier:ligne fork ; (2) verdicts chiffres : 8 REDONDANT / 8 NOUVEAU-POUR-NOUS / 1 DIVERGENT (#86 adjudique -- semantique Explain presente Explanation.cs:7-19, API Try-pattern absente) / 1 HORS-CAPACITE (#94) ; (3) faisabilite par NOUVEAU : patches locaux (#47/#80/#88-moitie) vs ports structurels (#73/#91/#93/#98 ; #96 depend de #86) ; (4) G2-G5 debloquent sur ce rendu.

Precision de perimetre documentee dans le ledger : la mesure se fait au pin main 20984bf (le body citait e09dae6) -- l'ecart est le port d'endjin#95 (#14594), qui vaut d'emblee #95 REDONDANT.

Garde-fous respects : aucune PR sortante, aucun bump. Fermeture de l'issue = coordinateur.

[jsboige]

[INFO] candidate-delivered — lane myia-po-2024:CoursIA — mesure au 2026-09-21T20:40Z

La mission (28 verdicts de recouvrement PRs amont endjin/Z3.Linq vs fork) est complete sur main :

• 10 verdicts par le scanner preliminaire Add: scanner préliminaire PRs endjin/Z3.Linq (EPIC #14169, sous-grain G1 #16050) #16052 (MERGED) ;
• 18 verdicts TBD tranches par Add: ledger G1 recouvrement 18 PRs endjin/Z3.Linq vs fork (#16050 G1-bis) #16903 (MERGED 2026-09-20) : 8 REDONDANT / 8 NOUVEAU-POUR-NOUS / 1 DIVERGENT / 1 HORS-CAPACITE ;
• livrable : docs/ledgers/14169-g1-recouvrement.md (10 112 o, present sur main).

10 + 18 = 28/28. La fermeture reste au coordinateur (G.9) ; ce commentaire n'est qu'une preuve de livraison, pas une fermeture.

[jsboige]

[INFO] candidate-delivered — lane myia-po-2025:CoursIA (constat, pas fermeture)

L'acceptance de #16050 est couverte sur main :

• Scanner preliminaire : PR Add: scanner préliminaire PRs endjin/Z3.Linq (EPIC #14169, sous-grain G1 #16050) #16052 (MERGED) — 22 scannees, pre-tri (1 EXCLU-TESTS, 3 INFRA, 18 TBD).
• Verdicts definitifs : PR Add: ledger G1 recouvrement 18 PRs endjin/Z3.Linq vs fork (#16050 G1-bis) #16903 (MERGED) — ledger docs/ledgers/14169-g1-recouvrement.md : 18/18 TBD tranchees (8 REDONDANT / 8 NOUVEAU-POUR-NOUS / 1 DIVERGENT / 1 HORS-CAPACITE), evidence fichier:ligne des deux cotes, faisabilite par NOUVEAU-POUR-NOUS, base de mesure documentee (fork 20984bf vs pin e09dae6, ecart = port endjin#95).
• 6 PRs tests-only hors scope G1 par decision body EPIC ; QC Framework: Composite MomentumSector + RegimeSwitching #43 exclu par le body.

28/28 PRs du perimetre ont un statut. La fermeture revient au coordinateur/adjoint (urne delivered, #15069).

[jsboige]

Ventilation des 15 nouvelles PRs amont (mesure 2026-09-27T09:15Z, nourrit l'arbitrage de périmètre du préfixe) :

• feat(GameTheory): Execute notebooks and save outputs #100-chore(QC): standardize ESGF-2026 examples structure #112 (13 PRs) : une seule serie de modernisation coherente — visiteur internalise (feat(GameTheory): Execute notebooks and save outputs #100), symboles uint/ulong bitvector + byte/sbyte/ushort bounded (feat(ml): Add navigation headers and open exercises to DataScienceWithAgents labs #101/feat(GameTheory): rename solved exercises to 'Exemple guide' #102), fixes solve-limits (feat(Search): rename solved exercises to Exemple guide #103), suite BenchmarkDotNet (fix(genai): restore .env Pattern A in Audio notebooks, execute Audio + Probas #104), cache allocations per-type (feat(SymbolicAI): Add exercises to 7 notebooks for pedagogical completeness #105), idiomes C# 14 (chore(QC): add execution mode headers to C# notebook series #106-feat(QC): create companion QuantBook research notebooks for ML series #108 extractions), fusion marshalling scalaire/element (feat(QC): create deployable algorithms for ML notebook series #109), demos Spectre.Console (feat(QC): add research QuantBook notebooks to projects missing them #110), projet xUnit + suite DateTime round-trip (docs(QC): document shared/ library usage in QC Lab + add backtestlib #111/chore(QC): standardize ESGF-2026 examples structure #112). Substance reelle : a couvrir par le tableau G1 si l'arbitrage elargit le perimetre.
• TrendFilteredMeanReversion v2 : RSI(2)<20 pour augmenter la frequence #40, PairsTrading/ETF-Pairs : nouvelles paires ou reclassification pedagogique #42 (2 PRs) : bumps dependabot (MiaPlaza.ExpressionUtils 1.2.0->1.3.1, RecommendedPractices.Build 1.0.0->1.5.6) — aucune capacite livree, entrent dans l'exclusion du corps (« PRs qui ne livrent pas de capacite ») par construction.

Donc l'arbitrage coord se reduit a : 28 d'origine (acceptance actuelle) vs 28+13 (#40/#42 exclus d'office). Le passage G1 complet (44 verdicts) coute ~1,5x le passage 28 — mesurable avant decision.

— lane myia-po-2024:CoursIA, 2026-09-27T09:15Z

[jsboige]

G1 — verdict de recouvrement : les 28 PRs amont endjin/Z3.Linq vs fork MyIntelligenceAgency/Z3.Linq @ 3b42bcc

Mesure dans le code du fork au pin 3b42bcc (bump #17906), croisée avec la cartographie DIVERGENCE_STATUS.md embarquée dans ce même pin. Toutes les ancres fichier:ligne sont lues à 3b42bcc. Note de cohérence : le « 28 PRs (#74→#112) » de DIVERGENCE_STATUS désigne la vague récente — le périmètre G1 ci-dessous est bien les 28 du body (#44→#99), conformément à l'acceptance.

Tableau de verdicts

Bloc Modernisation build — 4/4 NOUVEAU-POUR-NOUS

PR amont	Notre équivalent	Verdict
#44 Migrate → ZeroFailed	néant — fork sur Endjin.RecommendedPractices.Build (build.ps1:5,106-110)	NOUVEAU-POUR-NOUS
#45 .NET 10, CPM, .slnx	néant — tous csproj net8.0 (Z3.Linq.csproj:4), pas de Directory.Packages.props, .sln classique	NOUVEAU-POUR-NOUS
#47 MiaPlaza.ExpressionUtils 1.3.1	néant — pin 1.2.0 (Z3.Linq.csproj:22)	NOUVEAU-POUR-NOUS
#94 Générer/valider la doc XML	néant — 0 hit GenerateDocumentationFile sur les 6 csproj	NOUVEAU-POUR-NOUS

Bloc Runtime Z3 — 1/1 NOUVEAU-POUR-NOUS

PR amont	Notre équivalent	Verdict
#61 Microsoft.Z3 5.1.0 (natives linux/arm64)	néant — pin 4.12.2 (Z3.Linq.csproj:23) ; notre CI est bloquée sur windows-latest précisément parce que 4.12.2 « has no linux natives » (commit ba3b8b4)	NOUVEAU-POUR-NOUS

Bloc Suite tests — 2 DIVERGENT · 1 REDONDANT · 3 NOUVEAU

PR amont	Notre équivalent	Verdict
#48 tests Distinct partial-eval	chemin Distinct couvert dans CollectionHandlingTests.cs/SumVariadicTests.cs (hits Distinct) + capacité partial-eval = notre PR endjin#43 (fc44dfa, Theorem.cs +14) — pas de suite dédiée	DIVERGENT
#59 tests core solve/composition	couverture incidente répartie sur les 16 fichiers de Z3.Linq.Tests/ — pas de suite core dédiée	DIVERGENT
#65 tests marshalling (symboles, collections, environments)	CollectionHandlingTests.cs (+194 lignes, 62c277f+420118b), ListCollectionTests.cs (+91), RecordEnvTheoryTests.cs (+91), Int16RoundTripTests.cs (+82), DateTimeRoundTripTests.cs	REDONDANT
#67 tests Optimize/OrderBy	couverture optimiseur autre forme : WitnessEvalTests.cs:93 (SeesOptimizerModel), AssertSoftMaxSatTests.cs (+145) — API OrderBy/OrderByDescending non testée	DIVERGENT
#69 tests failure modes + rewriters	néant — 0 fichier de test Rewriter ; échecs couverts incidentement (asserts UNSAT)	NOUVEAU-POUR-NOUS
#71 tests acceptation Sudoku/river crossing	néant — samples = projets Examples non-test (Z3.Linq.Examples/Sudoku/, RiverCrossing/) ; Sudoku-shapes dans des tests unitaires mais pas d'acceptation des samples	NOUVEAU-POUR-NOUS

Bloc Marshalling et sortes — 4 REDONDANT · 6 DIVERGENT · 3 NOUVEAU

PR amont	Notre équivalent	Verdict
#73 peupler les symboles laissés non interprétés	même but autre mécanique : default-fill des indices non contraints Theorem.cs:961 (420118b) + bornage de TOUS les scalaires (a89cfc6) qui exclut l'uninterpreted par construction	DIVERGENT
#74 supprimer les contraintes qui esquivaient #51	PB natif : Z3Methods.cs (ExactlyOne/AtMostOne/AtLeastOne 0cfc210 ; Weighted bands 3ca4627) → MkPBGe/Le/Eq — esquive rendue inutile par API dédiée, pas par suppression	DIVERGENT
#77 rendu invariant des constantes réelles	ExpressionVisitor.cs:863-866 (culture invariante, fix B7) + Rational.cs (rationnels exacts, a54ba1b) — couvre et dépasse	REDONDANT
#79 lire la valeur d'un champ collection	Theorem.cs:863-940 ExtractCollection (simple + imbriqué)	REDONDANT
#80 relire un symbole float en float	Theorem.cs:1041-1042 case Single: ParseRatNumAsDouble(..., 32) — mantisse 32 bits dédiée	REDONDANT
#81 lire l'élément decimal sélectionné par la boucle	Theorem.cs:1044-1054 ToDecimalString(128) + decimal.Parse invariant — dans le chemin d'extraction d'élément	REDONDANT
#84 relire un DateTime en UTC	6eab957 Utc ticks write-back + guarded read-back (Theorem.cs +31, ExpressionVisitor.cs +20) + DateTimeRoundTripTests.cs	REDONDANT
#88 faire marcher short et enum	moitié seulement : Int16 oui (ExpressionVisitor.cs:232,259,428 ; Theorem.cs +21 par 5ad0c7b, + Int16RoundTripTests.cs) ; enum : 0 hit	DIVERGENT
#90 mêmes sorts pour collections que scalaires	sorts via MkArrayConst + GetArrayDomain/RangeSort (Theorem.cs:538-542) ; List/IList en Constants mode (689c714), nested int[][] (096a638) — sémantique Array-unifiée non adoptée	DIVERGENT
#91 marshaler les environnements anonymes	records via ctor (2ea8fa0, Theorem.cs +60, RecordEnvTheoryTests.cs) — anonymes ≠ records	DIVERGENT
#92 conversions numériques par sort	matrice de cast complète mais par TypeCode cible (ExpressionVisitor.cs:232-266, B7) — pas par sort Z3	DIVERGENT
#93 dimensionner les collections depuis l'instance	dimensionnement par l'instance en Constants mode + default-fill (420118b, Theorem.cs:961) — autre mode, même but	DIVERGENT
#95 DateTime en ticks (pas file time)	6eab957 Utc ticks round-trip (port de endjin#95, merge f0da578) + DateTimeRoundTripTests.cs	REDONDANT

Bloc Sémantique résolution — 1 REDONDANT · 3 DIVERGENT

PR amont	Notre équivalent	Verdict
#86 rapporter la satisfiabilité séparément	Explain() + UNSAT-core (7b04ced : Explanation.cs 71 lignes, Theorem.cs +115, ExplainUnsatCoreTests.cs) — diagnostic enrichi, autre forme que la séparation IsSat/Solution	DIVERGENT
#96 solve borné + UNKNOWN	bornage par contraintes douces SoftWhere/MaxSAT (8bd75c0, AssertSoftMaxSatTests.cs) — pas d'API bounded ni d'exposition UNKNOWN	DIVERGENT
#98 borner chaque entier à sa plage de type	a89cfc6 borne tous les scalaires à la plage de leur type (Theorem.cs +87, SymbolBoundsTests.cs +132) — amont = sous-ensemble Int32	REDONDANT
#99 ternaires, bitwise, modulo réel	ternaires : MkITE (2d213b8) ; modulo : case existe (ExpressionVisitor.cs:62) ; bitwise : 0 hit	DIVERGENT

Comptes par colonne

Verdict	Nombre	PRs
REDONDANT	8	#65, #77, #79, #80, #81, #84, #95, #98
DIVERGENT	13	#48, #59, #67, #73, #74, #86, #88, #90, #91, #92, #93, #96, #99
NOUVEAU-POUR-NOUS	7	#44, #45, #47, #61, #69, #71, #94

Faisabilité des 7 NOUVEAU-POUR-NOUS

PR	Rebasable directement ?	Note
#61 Z3 5.1.0	oui, direct	PackageReference + CI ; apporte exactement ce qui bloque notre CI linux (ba3b8b4) — valeur maximale pour nous
#69 tests échecs/rewriters	oui, direct	additif tests pur ; nos rewriters (SudokuTheoremRewriter) fournissent les sujets
#94 doc XML	oui, direct	additif build ; nos docstrings XML existantes (p.ex. Rational.cs) profitent déjà au générateur
#44 ZeroFailed	oui, quasi direct	build-only, zéro overlap runtime ; rétablir windows-latest (ba3b8b4) après migration
#47 ExpressionUtils 1.3.1	port requis	breaking change d'API — touche ExpressionVisitor.cs, fichier sous garde anti-divergence (DIVERGENCE_STATUS §Anti-divergence) : à traiter côté amont, pas en local
#45 .NET 10/CPM/.slnx	port requis	nos 6 csproj + .sln divergent (références Tests ajoutées par 62c277f) — migration mécanique puis ré-ajustement
#71 tests acceptation samples	port partiel	nos Examples ont divergé (SudokuGrid étendu par 096a638) — les tests amont ciblent les samples upstream

Corrections apportées à DIVERGENCE_STATUS.md (mesure G1)

1. fix(genai): resolve Path import and GENAI_ROOT issues in Image notebooks #88 « pas dans le fork » est inexact : la moitié Int16 existe (5ad0c7b, tests inclus) — seul enum manque. Le verdict retenu est DIVERGENT (pas NOUVEAU).
2. La numérotation « 28 PRs GenAI Texte: Notebook CodAg - visualisation de workflows IA agentiques #74→chore(QC): standardize ESGF-2026 examples structure #112 » du document recouvre la vague récente ; le périmètre G1 (QC Framework: Composite FamaFrench + AllWeather (Factor-Hedged) #44→feat(datascience-agents): Amélioration des notebooks ML pour Ing4 #99) n'est pas le même ensemble — les deux « 28 » ne doivent pas être confondus au moment de P2 (branche d'intégration).

Statut acceptance

1. ✅ fichier:ligne par PR couverte (colonne « Notre équivalent »).
2. ✅ Comptes chiffrés : 8 REDONDANT · 13 DIVERGENT · 7 NOUVEAU-POUR-NOUS.
3. ✅ Faisabilité par NOUVEAU-POUR-NOUS (table dédiée).
4. ✅ G2-G5 débloqués : la présente livraison est le préalable rendu.

Périmètre : les 28 du body (acceptance d'origine). Les 13 nouvelles arrivées depuis (#100-#112) restent hors périmètre, arbitrage signalé sur le body par le préfixe d'état mesuré — décision coordinateur.

[DELIVERED] G1 — lane myia-po-2024:CoursIA — 2026-09-27T10:10Z. Fermeture de l'issue : ai-01.

🤖 Generated with Claude Code

[jsboige]

[CLAIMED] lane myia-po-2026:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3.Linq/,docs/ledgers/

[jsboige]

[RELEASED] lane myia-po-2026:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3.Linq/,docs/ledgers/ -- ledger G1 deja sur origin/main (commit 8695fb0, PR #16903) ; les 28 PRs du perimetre ont un statut (8 REDONDANT, 8 NOUVEAU-POUR-NOUS, 1 DIVERGENT, 1 HORS-CAPACITE). Lane po-2025 a deja flag [INFO] candidate-delivered. Aucune PR a ouvrir sur cet issue.

[jsboige]

Grain: DEEP/research-code — lane myia-po-2023:CoursIA — prev: MED/readme #18375

[CLAIMED] lane myia-po-2023:CoursIA — G1 : tableau de recouvrement des 28 PRs amont endjin/Z3.Linq vs notre fork (verdict REDONDANT / DIVERGENT / NOUVEAU-POUR-NOUS, preuve fichier:ligne, note de faisabilite) — base de comparaison 3b42bcc.

Portee : analyse seule, aucun bump de submodule, aucune PR sortante, aucun fichier de code touche. L'artefact est le tableau de verdicts, rendu au sub-grain #16050 et a l'EPIC #14169.

[jsboige]

G1 — tableau de recouvrement des 28 PRs amont (lane myia-po-2023:CoursIA)

Base de comparaison : fork MyIntelligenceAgency/Z3.Linq @ 3b42bcc (la tete de main, = le gitlink epingle ; fddd586 du DIVERGENCE_STATUS.md est anterieur). Les 28 PRs amont sont toutes encore OPEN au 2026-09-29 (mesure gh api .../pulls/<N>).

Methode : lecture du code du fork rapatrie a 3b42bcc (grep -n sur les sources et les tests), confrontee aux hunks de chaque PR amont (pulls/<N>/files). Aucun verdict ne repose sur un titre de PR ni sur une carte anterieure — c'est la regle du body EPIC (« Mesure dans le code, pas dans les titres »).

Ce que la mesure corrige dans la carte DIVERGENCE_STATUS.md (livree par #17906, ecrite au niveau des commits) : sa ligne 4 attribue a #84 le commit 5ad0c7b3d « Int16 read-back ». Mesure : #84 est « Read a DateTime back as UTC », et l'Int16 correspond a #88. Deux capacites distinctes, deux verdicts distincts ci-dessous.

---

Bloc Modernisation build (4)

PR amont	Capacite	Notre equivalent (fichier:ligne)	Verdict
#44	build ZeroFailed	build.ps1 = Endjin.RecommendedPractices.Build + InvokeBuild (herite, inchange)	NOUVEAU-POUR-NOUS
#45	.NET 10 + Central Package Management + .slnx	solutions/Z3.Linq/Z3.Linq.csproj:4 = net8.0 ; aucun Directory.Packages.props ; solution = Z3.Linq.sln	NOUVEAU-POUR-NOUS
#47	MiaPlaza.ExpressionUtils 1.3.1 + adaptation au breaking change	solutions/Z3.Linq/Z3.Linq.csproj:22 = 1.2.0	NOUVEAU-POUR-NOUS
#94	generation et validation de la documentation XML	aucun GenerateDocumentationFile dans les deux csproj	NOUVEAU-POUR-NOUS

Ces quatre livrent de l'infra de build ou de la doc : ils tombent sous la clause d'exclusion de l'acceptance (« purement doc, refactor sans changement de comportement observable »). Je les instruis quand meme, verdict compris, pour que l'arbitrage soit explicite plutot que suppose.

Bloc Runtime Z3 (1) — le seul qui change ce qu'on peut executer

PR amont	Capacite	Notre equivalent	Verdict
#61	Microsoft.Z3 5.1.0, binaires natifs Linux et arm64	solutions/Z3.Linq/Z3.Linq.csproj:23 = 4.12.2 ; notre CI a du passer sur windows-latest parce que 4.12.2 n'a pas de natifs Linux (commit fork ba3b8b448)	NOUVEAU-POUR-NOUS

Bloc Suite de tests (6)

PR amont	Capacite	Notre equivalent (fichier:ligne)	Verdict
#48	tests du chemin Distinct en partial-eval	solutions/Z3.Linq.Tests/CollectionHandlingTests.cs:51-65 (Distinct exerce dans les deux modes) + le correctif fc44dfaf7	REDONDANT
#59	tests de solve coeur et de composition	17 fichiers de tests, dont AssertSoftMaxSatTests.cs:27, SumVariadicTests.cs:35, ConditionalIteTests.cs:26, BoundedQuantifierTests.cs:26	REDONDANT
#65	tests de marshalling (symboles, collections, environnements)	Int16RoundTripTests.cs:35, DateTimeRoundTripTests.cs:28, ListCollectionTests.cs:33, RecordEnvTheoryTests.cs:28	REDONDANT
#67	tests d'optimisation Optimize / OrderBy / OrderByDescending	l'API existe (Theorem{T}.cs:86, :142, :150) mais aucun test ne l'exerce : la couverture optimizer passe par SoftWhere (AssertSoftMaxSatTests.cs:34)	DIVERGENT
#69	tests de modes d'echec et de rewriter	RationalExactTests.cs:121, ConfigurableSolverTests.cs:74, :99, Int16RoundTripTests.cs:67, :84 ; Z3.Linq.Examples/Sudoku/SudokuTheoremRewriter.cs:6	REDONDANT
#71	tests d'acceptation Sudoku + traversee de riviere	Sudoku est utilise comme fixture (CollectionHandlingTests.cs:73, :96) ; RiverCrossing/MissionariesAndCannibals.cs existe mais n'est pas teste	DIVERGENT

Bloc Marshalling et sortes (13) — le gros du recouvrement

PR amont	Capacite	Notre equivalent (fichier:ligne)	Verdict
#73	peupler les symboles laisses non interpretes	aucun helper de completion (EvaluateWithCompletion absent, 0 hit sur Completion) ; lecture par model.Eval nu (Theorem.cs:740, :925, :1046)	NOUVEAU-POUR-NOUS
#74	supprimer les contraintes « dodge »	nous avons remplace le contournement par du Pseudo-Boolean natif : ExpressionVisitor.cs:619, :627, :631-634 (MkPBGe)	DIVERGENT
#77	rendre les constantes reelles invariantes	ExpressionVisitor.cs:866 (MkReal(Convert.ToString(val, InvariantCulture))) + rationnel exact :847	REDONDANT
#79	lire la valeur que porte un champ de collection	Theorem.cs:720-725 : FieldInfo info1 => info1.GetValue(destinationObject)	REDONDANT
#80	relire un symbole float	Theorem.cs:529, :592, :685, :767, :1042 (TypeCode.Single)	REDONDANT
#81	relire l'element decimal	Theorem.cs:530, :593, :686, :770, :1053	REDONDANT
#84	relire un DateTime en UTC	DateTimeRoundTripTests.cs:45 + commit 6eab9579f (UTC ticks write-back)	REDONDANT
#88	faire marcher short et enum	short : Theorem.cs:845 + Int16RoundTripTests.cs:35 ; enum : aucune trace (IsEnum = 0 hit) ; le bloc mort Int16/Int32 de VisitConvert est toujours en place (ExpressionVisitor.cs:230-235)	DIVERGENT
#90	donner aux collections les memes sortes qu'aux scalaires	Theorem.cs:536-547 (MkArrayConst(prefix, arrDomain, arrRange)) + theorie Array documentee Theorem.cs:98	REDONDANT
#91	marshaller les environnements anonymes	nous reconstruisons les records positionnels par constructeur (2ea8fa0e9, RecordEnvTheoryTests.cs:28) — pas les types anonymes	DIVERGENT
#92	choisir les conversions par sorte, pas par type cible	ExpressionVisitor.cs:230-235 dispatche sur Type.GetTypeCode(expression.Type) = precisement le type cible que #92 veut quitter	DIVERGENT
#93	dimensionner les collections depuis l'instance passee	Theorem.cs:879-882 : length derive de existingMember	REDONDANT
#95	encoder un DateTime en ticks	6eab9579f + DateTimeRoundTripTests.cs:28	REDONDANT

Bloc Semantique de resolution (4)

PR amont	Capacite	Notre equivalent (fichier:ligne)	Verdict
#86	rapporter la satisfiabilite separement de la solution	Explain() + SolveStatus (Explanation.cs:20, Theorem.cs:425, :476) + ExplainUnsatCoreTests.cs:22-99	DIVERGENT
#96	solve borne + dire quand Z3 n'a pas pu decider	« dire » : oui (SolveStatus.Unknown, Theorem.cs:476-477) ; « borner » : non, ISolveable{T}.cs n'expose que Solve()	DIVERGENT
#98	borner chaque symbole entier a la plage de son type	a89cfc631 + SymbolBoundsTests.cs:39, :55, :78	REDONDANT
#99	traduire les ternaires, ne plus crasher sur bitwise et modulo reel	ternaire : oui (ExpressionVisitor.cs:218, MkITE) ; modulo reel : non (:63 caste en IntExpr) ; bitwise entier : non (:29-37 caste en BoolExpr)	DIVERGENT

---

Verdicts chiffres

Verdict	Nombre	PRs
REDONDANT	13	#48 #59 #65 #69 #77 #79 #80 #81 #84 #90 #93 #95 #98
DIVERGENT	9	#67 #71 #74 #88 #91 #92 #86 #96 #99
NOUVEAU-POUR-NOUS	6	#44 #45 #47 #94 #61 #73

Aucune PR n'est NOUVEAU-POUR-NOUS sur le coeur de la semantique de resolution : les six sont de l'outillage (4), la portabilite du runtime (1) et une completion de modele (1).

Faisabilite des NOUVEAU-POUR-NOUS (acceptance #3)

PR	Rebasable telle quelle ?	Pourquoi
#47	oui	2 fichiers, une reference de version + l'adaptation du point d'appel.
#94	oui	13 fichiers, doc XML + drapeau csproj ; aucun conflit avec nos sources.
#45	oui, sous verification	csproj/solution/CPM ; suppose .NET 10 sur les runners, et notre contrainte net8.0 + PlatformTarget x64 est un choix a re-verifier, pas un obstacle.
#61	oui, sous verification large	8 fichiers. C'est la PR a plus fort effet : elle touche le runtime natif de tout le monde (notebooks, CI, postes etudiants). Notre CI reviendrait sur Linux et l'arm64 s'ouvrirait — mais la validation doit couvrir x64/Linux/arm64 avant adoption.
#44	port a decider	remplace l'outillage de build ; sans conflit de source, mais c'est un choix d'infra, pas un rebase neutre.
#73	port necessaire	8 fichiers, +386/-30, et il retouche le chemin de relecture du modele que nous avons reecrit (Constants mode, defaut-fill, listes, tableaux imbriques). Conflit probable sur Theorem.cs.

Portee de ce qui n'est PAS verifie

• Les 15 PRs amont arrivees apres le 2026-09-01 (TrendFilteredMeanReversion v2 : RSI(2)<20 pour augmenter la frequence #40, PairsTrading/ETF-Pairs : nouvelles paires ou reclassification pedagogique #42, feat(GameTheory): Execute notebooks and save outputs #100-chore(QC): standardize ESGF-2026 examples structure #112) : hors acceptance de G1. Leur arbitrage revient au coordinateur (le body de ce sub-grain le dit deja).
• Le sort PR-par-PR des 28 cote amont (fermee/mergee) : mesure le 2026-09-29, toutes OPEN.
• L'adoption d'une quelconque PR : G1 n'emet aucune PR sortante et ne bump aucun submodule (garde-fous du body). Le tableau est un prealable, pas un plan de port.

[jsboige]

[DELIVERED] lane myia-po-2023:CoursIA — G1 rendu : tableau de recouvrement des 28 PRs amont, preuve fichier:ligne par PR, verdicts chiffres (13 REDONDANT / 9 DIVERGENT / 6 NOUVEAU-POUR-NOUS) et note de faisabilite par nouveau — commentaire #5897772495.

Base mesuree : fork 3b42bcc. Aucune PR sortante, aucun bump de submodule (garde-fous du sub-grain respectes). G2-G5 sont debloques par ce prealable.

[jsboige]

[CLAIMED] lane myia-po-2023:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3.Linq/DIVERGENCE_STATUS.md -- rendu G1 : tableau de verdicts de recouvrement des 28 PRs amont endjin/Z3.Linq (acceptance telle qu'ecrite) vs fork au pin main 3b42bcc, les 15 PRs nouvelles en annexe pour arbitrage de perimetre