Repository navigation
[Epic] Compression : sous-serie pedagogique par plis (format Origami) avec codecs et MDL, jumeau Python/Lean, greffe M9 Epita non-choisi (refs OpenZL 2026-09-29 + PivCo-Huffman + sujet M9 + ICT-17b) #18706
Description
Rattaché à #5081
État mesuré au 2026-10-12 (lane myia-po-2025:CoursIA, tapis roulant #18832). Le paragraphe ci-dessous est périmé sur un point : le Pli 2 n'est plus « attendu d'ai-01 » — il est déployé et en cours de livraison. Mesuré firsthand : sous-issue #20394 ouverte (« [Compression] Pli 2 : Compression-02 Huffman canonique et tables de décodage ») et PR #20399 OPEN (lane
myia-po-2027:CoursIA-2, 922+/1-) surMyIA.AI.Notebooks/Compression/Compression-02-HuffmanCanonique-Python.ipynb. Ce qui change pour un lecteur : l'EPIC n'a plus de grain libre au Pli 2 ; le prochain est le Pli 3 (Compression-03-LZ77), à déplier après le merge de #20399. Portée de ce qui n'a pas été vérifié : la conformité du carnet de #20399 aux décisions D1-D8 n'est pas mesurée ici, et l'état des plis 3 à 10 reste celui du corps ci-dessous. L'historique est conservé intact en dessous.
État mesuré au 2026-10-05 (lane myia-po-2025:CoursIA-2, consolidation #13906). Pli 1 LIVRÉ : #18729 (mergée 02/10) pose
Compression-01-ShannonFano-Prefixe-Python.ipynb+ le README de la sous-série surmain. Mais le pli 2 n'est pas déplié : le dernier commentaire de l'EPIC reste l'arbitrage D1-D8 du 01/10 (antérieur au merge du pli 1), aucun commentaire[PLI 2 DÉPLIÉ], aucune sous-issue Compression ouverte au-delà de l'EPIC. Même verrou séquentiel que #18605/#18783 : le format Origami ne progresse que par dépliage coordinateur à complétion vérifiée du pli précédent — la complétion est là (pli 1 mergé depuis 02/10), le dépliage est attendu d'ai-01.
Front actuel : dépliage du pli 2 (Compression-02, Huffman, source R-pivco) par commentaire
[PLI 2 DÉPLIÉ]créant la sous-issue. Portée non vérifiée : conformité du carnet livré aux décisions D1-D8 (non mesurée ici). EPIC vivante, gelée sur le coordinateur, non fermable.
Grain: DEEP/curriculum — lane myia-po-2026:CoursIA-2 — prev: MED/lean #18615
Mission user 2026-10-01 : prolonger le geste de
#18220(EPIC origami lacunes pédagogiques, pli 2/3 « contenus confirmés absents ») et du namespaceOrigamidu mainteneur (#18204système 1,#18205Lean Poincaré,#18605NeRF/Fourier/IMM/TVM) par un EPIC origami dédié à une sous-série pédagogiqueCompression, calquée sur le modèle de la sérieMyIA.AI.Notebooks/Complexity/(9 notebooks, accréation b/c, trois niveaux Découverte/Licence/Recherche, encart Mathlib gap pour la branche Lean).Convention de nommage :
Origamiest le format de l'Epic (déploiement par plis séquentiels — sous-issues créées à complétion du pli précédent, voir#18220et#18605pour le patron canonique), pas le nom de la sous-série. La sous-série pédagogique s'appelleCompression, le dossier seraMyIA.AI.Notebooks/Compression/, les notebooksCompression-NN-...etCompression-NNb-....Sources first-hand lues : OpenZL blog 2026-09-29, PivCo-Huffman paper v1.0 (Żukowski 2026-06-04, arXiv 2606.05765), upstream
MyIntelligenceAgency/LeanMyIA.Trading.Converter/,ICT-17b-Grokking-CompressionProgress.ipynb, 7 notebooks3.9*Compression*ML existants, dépôt étudiant Epita 2026 (sujet M9 « compresseur neuro-symbolique » 5/5, jamais choisi par les groupes).
Format Origami — déploiement par plis séquentiels
Le format Origami (cf. #18220 umbrella, #18605 NeRF/Fourier) est un mode de déploiement d'Epic où les sous-issues ne sont PAS créées d'un coup : elles sont déverrouillées par le coordinateur à complétion vérifiée du pli précédent. Mécanisme canonique :
- Pli N porte dans sa posture un long descriptif (livrable, sources, pré-conditions, verdict SOTA attendu) sans sous-issue.
- À merge du pli N (vérification firsthand du coordinateur), le coordinateur déplie le pli N+1 par un commentaire
[PLI N+1 DÉPLIÉ]qui liste les sous-issues créées. - Rien n'est créé d'avance : le coordinateur évite ainsi de saturer le pool d'issues avec des promesses non-tenues, et chaque pli reste lisible en isolation.
Pour cet Epic : un pli = un notebook (Compression-PLAzure 01, 02, ..., 06b). Les accrétions (b/c) sont soit dans le même pli que le notebook parent, soit dans un pli ultérieur selon la dépendance pédagogique.
Sources first-hand (vérifiées)
| Slug | Référence | Domaine | Résonance sous-série |
|---|---|---|---|
| R-openzl | OpenZL v0.3.0 blog 2026-09-29 (https://openzl.org/blog/2026-09-29-lz-in-openzl/) |
LZ engine natif 2× Zstandard, Offset Encoding V-optimal, PivCo Huffman intégré, FieldLZ, graph-based + trainer Pareto | Codecs SOTA 2025-2026 (Compression-04b) |
| R-pivco | Żukowski, PivCo-Huffman v1.0 (arXiv 2606.05765, 2026-06-04) | Huffman sur wavelet trees, décodage SIMD-friendly bottom-up, +ANS sélectif, M4 benchmarks | Compression-02 + Compression-04 |
| R-lean-conv | MyIntelligenceAgency/Lean/MyIA.Trading.Converter/CompressionHelper.cs (port verbatim local) |
88 formats in / 6 formats out / 15 algorithmes / 3 backends (SharpCompress défaut, SevenZipExtractor, SevenZipSharp natif 7z-x64.dll) |
Compression-03b + Compression-06 (banc de mesure) |
| R-ict17b | MyIA.AI.Notebooks/IIT/ICT-Series/ICT-17b-Grokking-CompressionProgress.ipynb (issue #4588) |
Schmidhuber compression-progress, K multidimensionnel, 5 proxys (‖w‖², Fisher trace, Fisher-MDL, zlib, 1-acc) | Compression-06 (MDL) |
| R-ml-compression | MyIA.AI.Notebooks/ML/DataScienceWithAgents/03-DeepLearning/3.9*Compression*.ipynb (7 notebooks) |
Quantization INT8, Pruning from-scratch, Distillation, quantization SOTA, pruning SOTA, comparatif A-vs-B | Compression-05 (greffe) |
| R-m9-epita | jsboigeEpita/2026-Epita-Intelligence-Symbolique/ (sujet M9, 5/5, jamais choisi) |
Compresseur sans perte neuro-symbolique : LLM-découvreur + decodeur certifié + DSL façon Bitcoin Script (gas/fuel) + registre façon YARA/PRONOM + évaluation MDL vs zstd/ZPAQ | Compression-05b |
| R-complexity | MyIA.AI.Notebooks/Complexity/ (9 notebooks, modèle pédagogique canonique) |
Numérotation 01→06 monotone + lettre collée au numéro (b/c), trois niveaux, encart Mathlib, ≥3 exercices, socle Python, README série avec tableau de progression | Patron pédagogique de la série Compression |
État mesuré du matériel existant
CompressionHelper.cs(port verbatim local, commite7c1282813+ca71ae5c87+0e80a17cd2) — 538 lignes, 88 formats in / 6 formats out / 15 algorithmes / 3 backends. Pas de fichier de tests ni de benchmark dédié dans CoursIA — seulement les redevances Lzma/Zstd/Deflate déjà mesurées dansMyIA.Trading.Converter/README.mdligne 91 sur eurusd daily/hourly.7z-x64.dll+7z-x86.dll— DLLs natives 7z.dll d'Igor Pavlov, version pinnée#1.0.14(commitcb9d877b6roo-extensions submodule, dépendance NuGetSevenZipExtractor 1.0.15du forkMyIntelligenceAgency/Lean). Le port CoursIA est sur une version 2022-2023 — à mettre à jour vers la dernière 7z.dll de la distribution 7-Zip moderne (Igor Pavlov ≥23.x), qui inclut des codecs étendus absents de la version pinnée :Lizard,Lz5,Flzma2,Lz4,Zstd,Brotli. Ces codecs sont rapides en compressant moins (compromis vitesse/taux de compression délibéré) —Flzma2= Fast LZMA2,Lz4= débit Mo/s très élevé au prix d'un taux réduit,Lizard/Lz5= variantesLZ4 plus agressives en ratio. L'Epic mandate la migration vers la distribution 7-Zip moderne (codecs étendus), pas le maintien de la version pinnée.- ICT-17b — K multidimensionnel, pli de Thom proxy-dépendant, jonction ICT-18 σ(t) et B(t) = double INCONCLUSIF. Le
len(zlib.compress(x))EST la mesure de compressibilité qu'ICT-17b utilise déjà — c'est l'ancre de Compression-06. - Notebooks
3.9-*— Quantization INT8, Pruning from-scratch, Distillation, etc. Compression modèle (réseaux de neurones). Greffe Compression-05 = vue d'ensemble + section « voir aussi Compression-05 » dans leur README (compromis, cf. D3 décisions ouvertes). - ICT-46 Strate 7 freebits Aaronson — cousin épistémologique (limites d'un prédicteur bayésien face à l'inconnu structurel), pas compression.
- Namespace Epic origami existant (le format) —
#18204(système 1),#18205(Lean Poincaré),#18220(umbrella lacunes pédagogiques),#18605(NeRF/Fourier). Cet Epic Compression suit leur format Origami pour une discipline spécifique. - Sujets compression existants non-Epic —
#16060 [ML/Compression],#16774 histoire de l'art,#16759/#16775 Schmidhuber curation. La sous-sérieCompressionn'est en collision avec aucun — c'est une série pédagogique structurée qui les couvre.
Proposition de structure pédagogique MyIA.AI.Notebooks/Compression/ — 6 notebooks principaux + 5 accrétions
Numérotation alignée Complexity (01-06), format Compression-NN-Titre-Python.ipynb (noyau Python) ou Compression-NNb-Titre-Lean.ipynb (branche Lean), lettre collée au numéro (b/c), trois niveaux Découverte/Licence/Recherche, encart Mathlib gap pour la branche Lean, ≥3 exercices par notebook.
Pli 1 — Socle Découverte (notebooks 01-02)
| Position | Titre proposé | Contenu | Sources |
|---|---|---|---|
| Compression-01 | Codes préfixes et Shannon-Fano | Comptage de fréquences sur text8, code de Shannon-Fano (1951), inégalité de Kraft, optimalité. Mesure : longueur moyenne vs borne H(X) ≤ L < H(X)+1. Premier pli : longueur fixe (ASCII 8 bits) → longueur variable. |
ICT-17b §0 (triade Φ/F/K) |
| Compression-02 | Huffman canonique et tables de décodage | Algorithme bottom-up de Huffman (1952), forme canonique (Schwartz/Miller 1964), table de décodage 2^L, mesure du débit en Mo/s sur benchmarks text8 + prose_pride. Comparaison PivCo-Huffman papier §1.2 (Huff0 2929 Mo/s M4 vs Oodle Huffman 3343 Mo/s M4). |
R-pivco §1.2 |
Pli 2 — Licence (notebooks 03-04)
| Position | Titre proposé | Contenu | Accréation |
|---|---|---|---|
| Compression-03 | LZ77 et décompression à fenêtre glissante | Algorithme Ziv-Lempel 1977, parsing en littéraux + (offset, length), structure LZData instanciée sur text8. Mesure : débit de recherche naïve O(n²) vs O(n log n) (suffix array) — pont vers PivCo-Huffman §6.5 (« impact on LZ-codecs »). Premier contact avec la double couche (LZ parse + entropy back-end). |
03b — LZMA + LZMA2 + codecs rapides : pipeline distribution 7zip étendue pinnée (lecture verbatim CompressionHelper.cs CompressSingleFileSevenZipSharp + DictionaryRangecoder) — et comparaison côte-à-côte avec les codecs rapides-compressant-peu de la même distribution : Lz4 (débit Mo/s maximal, taux réduit), Flzma2 (Fast LZMA2, compromis vitesse/ratio), Lizard/Lz5 (variantesLZ4 plus agressives en ratio). C'est précisément la valeur pédagogique de la distribution pinnée : voir sur le même banc le compromis classique LZMA2 (lent, ratio élevé) vs LZ4 (rapide, ratio modeste). |
| Compression-04 | ANS et la compression moderne | Szczepanski 2009 → Dudek 2024 → lib ans moderne. Implémentation tANS (table-based) et rANS (range). Comparaison vs Huffman : ANS atteint l'entropie, Huffman est borné à 1 bit près. Mesure : débit encodage + décodage sur silesia-small. |
04b — Codecs SOTA 2025-2026 : Zstd 1.5+, OpenZL 0.3.0 (LZ + PivCo), brotli 1.1+, plus les codecs rapides de la distribution 7zip pinnée (Lz4, Lizard, Lz5, Flzma2) — benchmarking via bench.sh avec graphe vitesse vs taux de compression mettant en évidence les quatre régimes (lent-élu, lent-modeste, rapide-élu, rapide-modeste). |
Pli 3 — Recherche (notebooks 05-06)
| Position | Titre proposé | Contenu | Accréation |
|---|---|---|---|
| Compression-05 | Compression et machine learning : quantization, pruning, distillation | Synthèse des notebooks 3.9-* ML existants (déjà sur disque). Greffe : réutilisation verbatim des cellules existantes, ordonnancement pédagogique, mesure comparative avant/après chaque technique. Pont avec ICT-17b §2 : la quantization INT8 EST le compression-progress au niveau du réseau. |
05b — Compression × M9 Epita : LLM-découvreur + decodeur certifié sur DSL total + recettes signées (sujet M9 dépôt étudiant Epita 2026, jamais choisi par les groupes) |
| Compression-06 | Information theory meets Kolmogorov : MDL et compression-progress | MDL (Rissanen 1978), compress() comme proxy de K (Kolmogorov complexity), cross-over avec ICT-17b : le len(zlib.compress(x)) EST la mesure de compressibilité qu'ICT-17b utilise déjà. Mesure : taux de compression MDL vs zstd vs gzip vs brotli vs codecs rapides de la distribution 7zip pinnée (Lz4, Lizard, Lz5, Flzma2) sur les datasets eurusd_daily.csv (3 487 lignes) et eurusd_hourly.csv (69 928 lignes) du dossier MyIA.AI.Notebooks/QuantConnect/datasets/forex/. Greffe sur CompressionHelper.cs : CompressSingleFileSharpCompress benchmark sur les 6 OutputArchiveFormat, plus appel aux codecs rapides via CompressSingleFileSevenZipSharp pour mesurer la trade-off vitesse/precision. |
06b — Compression × Lean : preuve formelle d'une borne de compression (Shannon-Fano sur alphabet fini) en Lean 4.33.1, jumeau Compression-06 (Python, mesures) / Compression-06b (Lean, preuve). Encart Mathlib gap : Mathlib.InformationTheory.Kolmogorov n'existe pas en 4.33.x. |
Tableau récapitulatif
MyIA.AI.Notebooks/Compression/
├── README.md # index série (parcours 01→06, niveau par notebook)
├── Compression-01-ShannonFano-Prefixe-Python.ipynb # Découverte
├── Compression-02-HuffmanCanonique-Python.ipynb # Découverte
├── Compression-03-LZ77-Python.ipynb # Licence
├── Compression-03b-LZMA-LZMA2-Python.ipynb # Recherche (approfondissement 03)
├── Compression-04-ANS-Python.ipynb # Licence
├── Compression-04b-CodecsSOTA-OpenZL-PivCo-Python.ipynb # Recherche (approfondissement 04)
├── Compression-05-MLCompression-Python.ipynb # Licence (greffe 3.9-*)
├── Compression-05b-NeuroSymbolic-M9Recipe-Python.ipynb # Recherche (= sujet M9 Epita non-choisi)
├── Compression-06-MDL-Kolmogorov-Python.ipynb # Licence (greffe ICT-17b + 6 formats CompressionHelper)
└── Compression-06b-MDLKolmogorov-Lean.ipynb # Recherche (jumeau Lean, encart Mathlib gap)
11 notebooks au total (6 principaux + 5 accrétions). Le ratio accrétion/notebook = 5/11 = 45 %, comparable à Complexity (5/9 = 56 %).
Libs candidates pour la série Compression (vérifiées NuGet 2026-10-01)
| Lib | Version latest | Licence | Rôle dans la série | Source |
|---|---|---|---|---|
Squid-Box.SevenZipSharp |
1.6.2.24 (NuGet) |
LGPL-3.0-only | Wrapper C# moderne de la 7z.dll — supporte tous les codecs 7-Zip modernes dont Lizard, Lz5, Flzma2, Lz4, Zstd, Brotli. Fork actif maintenu par Joel Ahlgren (https://github.com/squid-box/SevenZipSharp). À substituer au SevenZipSharp pinné pour bénéficier des codecs étendus. |
NuGet squid-box.sevenzipsharp |
SharpCompress |
0.40.0+ (vérifier latest) |
MIT | Backend par défaut upstream pour CompressSingleFileSharpCompress. Supporte Zip/Tar/GZip/BZip2/LZip/XZ natifs sans passer par 7z.dll. Idéal pour Compression-06 (benchmarks 6 formats modernes). |
NuGet sharpcompress |
SevenZipExtractor |
1.0.19 (NuGet) |
(vérifier) | Wrapper C# historique pour 7z.dll — version upstream MyIntelligenceAgency/Lean utilise 1.0.15. Mettre à jour vers 1.0.19 qui wrappe la 7z.dll avec codecs étendus. |
NuGet sevenzipextractor |
SevenZip (NuGet standard) |
19.0.0 |
LGPL-3.0+ | Package historique, baseline de compat. | NuGet sevenzip |
Justification pédagogique du choix Squid-Box.SevenZipSharp : (1) actif (dernière release 2025), (2) licence LGPL-3.0 compatible avec distribution CoursIA (vérifier auprès du mainteneur), (3) wrappe n'importe quelle 7z.dll compatible (pas de couplage fort avec une version précise), (4) supporte explicitement les codecs modernes Lizard/Lz5/Flzma2 que la 7z.dll pinnée 1.0.14 ne contient pas. C'est précisément la distribution étendue dont le user parle : codecs rapides-compressant-peu disponibles sans nécessiter une 7z.dll exotique.
Distribution 7-Zip moderne (Igor Pavlov ≥23.x) : la 7z.dll livrée par ces packages est la distribution officielle Igor Pavlov récente, qui contient nativement Lz4 (depuis 21.07+), Zstd (depuis 22.01+), Brotli (depuis 21.07+), Lizard/Lz5 (depuis 23.02+), Flzma2 (Fast LZMA2). C'est la même que celle que les packages NuGet ci-dessus wrappent.
Ponts inter-séries (à expliciter dans chaque notebook)
| Compression notebook | Cross-référence Complexity | Cross-référence ICT-Series | Cross-référence ML |
|---|---|---|---|
| 01-02 Shannon/Huffman | — | ICT-17b §0 (triade K) | — |
| 03 LZ77 | Complexity-03 (hiérarchie temporelle) | ICT-17b zlib | — |
| 03b LZMA | Complexity-02 (P vs NP, parsing) | — | — |
| 04 ANS | Complexity-01 (step counting) | — | — |
| 04b Codecs SOTA | — | ICT-24 (ignitions LLM) | — |
| 05 ML Compression | Complexity-05 (Permanente, #P) | — | greffe 3.9-* |
| 05b Neuro-Symbolic M9 | Complexity-06 (Dequantification) | — | — |
| 06 MDL Kolmogorov | Complexity-04 (Online) | ICT-17b §2 (compression-progress) | — |
| 06b Lean MDL | Complexity-03b Hartmanis-Stearns | — | — |
Particularité forte : Compression est la seule série du dépôt qui s'appuie explicitement sur MyIA.Trading.Converter/CompressionHelper.cs comme banc de mesure — pas seulement comme outil interne. Le port verbatim upstream devient un instrument pédagogique réutilisé.
Estimation de l'effort
| Notebook | Difficulté | Justification (premier passage) |
|---|---|---|
| 01 Shannon-Fano | 2-3 j | Algo simple, mesures directes sur text8 |
| 02 Huffman canonique | 3-4 j | Table 2^L non triviale, PivCo-Huffman §1.2 à traduire |
| 03 LZ77 | 4-5 j | Parsing + fenêtre glissante + benchmarks suffix array |
| 03b LZMA / LZMA2 | 5-6 j | Range coder + dictionary coder ; CompressionHelper.cs lecture serrée |
| 04 ANS | 5-7 j | tANS + rANS ; papier Dudek 2024 dense |
| 04b Codecs SOTA 2025-2026 | 4-5 j | OpenZL 0.3.0 + Zstd 1.5+ + brotli 1.1+ installation, bench croisé |
| 05 ML Compression (greffe 3.9-*) | 2-3 j | Réordonnancement + harmonisation, pas d'écriture nouvelle |
| 05b Neuro-Symbolic M9 | 7-10 j | Sujet M9 complet (LLM-découvreur + DSL total + registre YARA) |
| 06 MDL Kolmogorov | 4-5 j | Pont ICT-17b + benchmarks 6 formats CompressionHelper |
| 06b Lean MDL | 5-7 j | Preuve Lean 4.33.1 sur lac dédié, encart Mathlib gap |
| README + organe série | 1 j | Index, parcours, ponts inter-séries |
Total estimé : 43-56 j-homme pour la série complète. C'est substantiel mais raisonnable (Complexity série a livré 9 notebooks en ~3 mois selon l'historique git visible dans le README de série).
Décisions ouvertes (à arbitrer avant ouverture des sous-issues — déploiement par plis)
| # | Décision | Recommandation | Attente arbitrage |
|---|---|---|---|
| D1 | Format Origami confirmé (déploiement par plis séquentiels, sous-issues créées à complétion) | OK — #18220 umbrella, #18605 NeRF sont les précédents. Permet de ne pas saturer le pool d'issues avec des promesses non-tenues. Convention de nommage : Compression pour la sous-série, Origami pour le format de l'Epic. |
User (à valider) |
| D2 | Dossier MyIA.AI.Notebooks/Compression/ à part ou intégrer dans MyIA.AI.Notebooks/Complexity/ ? |
À part : deux disciplines distinctes (complexité = borne asymptotique ; compression = codec concret). Complexité ↔ Compression via les cross-refs ci-dessus. | User |
| D3 | Greffer les notebooks 3.9-*Compression* ML dans Compression-05 ou laisser à leur emplacement ? |
Compression-05 = vue d'ensemble + 3.9-* restent intacts avec une section « voir aussi Compression-05 » dans leur README. Risque : renommage viole notebook-accretion-numbering.md §4. Compromis retenu. |
User (souhaitable : valider le compromis avant ouverture Compression-05) |
| D4 | Position 06b Lean : sur quel lake ? | Compression_lean/ dédié avec lake minimal (mathlib seul). Encart Mathlib : Mathlib.InformationTheory.Kolmogorov n'existe pas en 4.33.x, à vérifier firsthand à l'ouverture. Si cible échoue à lake build, basculer en formal_logic_lean (compatible 4.33.1, cf. leçon fondateur ModalLogic Tableau). |
User |
| D5 | Sujet M9 Epita 2026 : à intégrer tel quel ou à recycler ? | Intégrer comme Compression-05b avec note explicite : « sujet M9 du dépôt jsboigeEpita/2026-Epita-Intelligence-Symbolique, jamais choisi par les groupes, ici promu en approfondissement de recherche ». Pas de fork, pas de crédit étudiant (sujet ouvert). |
User |
| D6 | Migration de CompressionHelper.cs vers la distribution 7-Zip moderne (codecs étendus latest) : OK ? |
Migration mandatée par l'Epic : (1) remplacer la version pinnée SevenZipExtractor 1.0.14 par la dernière version NuGet (SevenZipExtractor 1.0.19 au 2026-10-01) qui wrappe la distribution 7-Zip moderne (Igor Pavlov ≥23.x) avec codecs étendus Lizard, Lz5, Flzma2, Lz4, Zstd, Brotli ; (2) substituer ou compléter SevenZipSharp par Squid-Box.SevenZipSharp 1.6.2.24 (LGPL-3.0, fork actif maintenu par Joel Ahlgren, wrappe n'importe quelle 7z.dll compatible) qui supporte explicitement les codecs modernes ; (3) garder SharpCompress (MIT, défaut upstream) pour les formats modernes Zip/Tar/GZip. Compression-03b, Compression-04b et Compression-06 appellent les méthodes (CompressSingleFileSevenZipSharp, CompressSingleFileSharpCompress, DecompressSingleFileSevenZipExtractor) sans les modifier (règle anti-régression .claude/rules/anti-regression.md — seul le port de la DLL change). Le port upstream devient l'organe de la série, mis à jour vers la dernière distribution. |
User |
| D7 | Préfixe de noyau (-Python / -Lean) sur tous les fichiers ? |
Oui, obligatoire d'après notebook-accretion-numbering.md §1. Noyau Python pour 01→05, -Lean pour 06b. Compression-06 = -Python, Compression-06b = -Lean (jumeau conforme au patron Lean-12/Lean-12b). |
User (à confirmer le surnom « Lean » sans suffixe collision) |
| D8 | Nommage Compression-05b-NeuroSymbolic-M9Recipe-Python.ipynb : trop long ? |
Le suffixe M9Recipe rappelle la provenance. Alternative : Compression-05b-NeuroSymbolic-Recipe-Python.ipynb (plus court). |
User |
Plan de déploiement par plis (format Origami — séquentiel, après arbitrage D1-D7)
Pli 0 — cette issue Epic : décrire la sous-série Compression + décisions D1-D8 + estimation. Sign-off user sur D1-D7.
Pli 1 — Compression-01-ShannonFano-Prefixe-Python.ipynb : socle Découverte, premier pli. Pas de pré-condition. À déplier à l'arbitrage user.
Pli 2 — Compression-02-HuffmanCanonique-Python.ipynb : suite Découverte. Pré-condition : Pli 1 livré.
Pli 3 — Compression-03-LZ77-Python.ipynb : entrée Licence. Pré-condition : Pli 2 livré.
Pli 4 — Compression-03b-LZMA-LZMA2-Python.ipynb : accrétion 03. Pré-condition : Pli 3 livré.
Pli 5 — Compression-04-ANS-Python.ipynb : Licence. Pré-condition : Pli 3 livré.
Pli 6 — Compression-04b-CodecsSOTA-OpenZL-PivCo-Python.ipynb : accrétion 04. Pré-condition : Pli 5 livré.
Pli 7 — Compression-05-MLCompression-Python.ipynb : Licence (greffe 3.9-*). Pré-condition : Pli 3 livré (pont ICT-17b zlib).
Pli 8 — Compression-05b-NeuroSymbolic-M9Recipe-Python.ipynb : accrétion 05. Pré-condition : Pli 7 livré.
Pli 9 — Compression-06-MDL-Kolmogorov-Python.ipynb : Licence (greffe ICT-17b + 6 formats CompressionHelper). Pré-condition : Pli 2 livré (triade K).
Pli 10 — Compression-06b-MDLKolmogorov-Lean.ipynb : accrétion 06 Lean. Pré-condition : Pli 9 livré.
Pli final — feature/compression-readme : tableau de progression + parcours + position dans le dépôt (calque exact du README Complexity). Pré-condition : tous les plis principaux livrés.
Mécanisme de dépliage : à merge de chaque pli, le coordinateur crée le pli N+1 par un commentaire [PLI N+1 DÉPLIÉ] listant la nouvelle sous-issue. Rien n'est créé d'avance.
Risques identifiés
| Risque | Probabilité | Mitigation |
|---|---|---|
Lean 4.33.x incompatibilité proofwidgets (cf leçon fondateur ModalLogic Tableau) sur Compression_lean/ |
MOYEN | Cadrer Compression-06b sur borne de Shannon-Fano uniquement, pas sur la couche Computability/ complète. Si la cible échoue à lake build, basculer en formal_logic_lean (compatible 4.33.1). |
| Scope creep M9 (sujet trop ambitieux pour 05b) | ÉLEVÉ | M9 lui-même est noté 5/5 dans Epita, ce qui explique pourquoi aucun groupe ne l'a choisi. Cadrer Compression-05b sur les 4 premiers objectifs de M9 (recette + LLM-découvreur + DSL total borné + registre YARA) ; l'objectif 5 (évaluation vs zstd/ZPAQ) reste ouvert et se tranche après les 4 premiers. |
| Conflit de noms avec sous-module / Epic existant | FAIBLE | Aucune sous-série Compression dans le dépôt en collision (vérifié gh issue list --search compression --state all 2026-10-01). Le format Origami n'est pas un nom réservé — c'est un format de déploiement partagé. |
| Référents hors dépôt | MOYEN | Pas de renommage 3.9-* initialement (cf D3 compromis) — donc pas de catalogue étudiant à mettre à jour. À surveiller si D3 évolue. |
Inventaire Lean Mathlib.InformationTheory.Kolmogorov inexistant |
MOYEN | Vérifier firsthand à l'ouverture Compression-06b ; si absent, l'encart Mathlib gap le dit honnêtement et le notebook Lean se réduit à la preuve d'une borne Shannon-Fano (suffisant comme premier livrable). |
Conformité avec les règles du dépôt
- CLAUDE.md §A (Coordination & Git) : aucun push direct sur
main, branchesfeature/compression-NN, coordinateur merge. ✓ - CLAUDE.md §C (Notebooks) : pas d'erreur volontaire, committés AVEC outputs, scope strict re-exec. ✓
.claude/rules/notebook-conventions.md: 3 exercices par notebook, encart Mathlib pour-Lean, kernellean4-wslou WSL pourCompression-06b. ✓.claude/rules/notebook-accretion-numbering.md: lettre collée au numéro (03b,03c), préfixe de noyau obligatoire, normee-fmaximum respectée (max lettre =fsur la branche 06 avec06b). ✓.claude/rules/three-exercises-per-notebook.md: ≥3 exercices, classification par contenu. ✓.claude/rules/sota-not-workaround.md: vrais outils SOTA (OpenZL 0.3.0, PivCo-Huffman, Zstd 1.5+), pas de stub. ✓.claude/rules/anti-regression.md:CompressionHelper.csréutilisé sans modification (règle 4 étapes respectée). ✓harness-hygiene.md: ce Epic est dans une issue GitHub (visible user), pas commité dans le repo. ✓audit-cross-source-distillation.md: la sortie d'un audit éventuel irait au dashboard RooSync, pas dans le repo. Pour Compression, audit = comparer chaque notebook à sa source first-hand (R-openzl blog, R-pivco paper, R-ict17b, R-m9-epita description). ✓
Sources citées (récap)
- OpenZL blog 2026-09-29 LZ in OpenZL :
https://openzl.org/blog/2026-09-29-lz-in-openzl/ - PivCo-Huffman paper v1.0 (Żukowski, 2026-06-04, arXiv 2606.05765) :
https://marcinzukowski.github.io/pivco-huffman/paper-1.0/ph.html - Upstream
MyIntelligenceAgency/LeanMyIA.Trading.Converter/:https://github.com/MyIntelligenceAgency/Lean/tree/master/MyIA.Trading.Converter - Dépôt étudiant Epita 2026 (sujet M9) :
https://github.com/jsboigeEpita/2026-Epita-Intelligence-Symbolique/ MyIA.Trading.Converter/CompressionHelper.cs(port verbatim local) : 538 lignes, commitse7c1282813+ca71ae5c87+0e80a17cd2MyIA.AI.Notebooks/IIT/ICT-Series/ICT-17b-Grokking-CompressionProgress.ipynb(Schmidhuber compression-progress, issue [Epic] - IIT → ICT : trajectoires intégrées, morphogenèse minimale et émergence multi-échelle #4588)MyIA.AI.Notebooks/ML/DataScienceWithAgents/03-DeepLearning/3.9*Compression*.ipynb(7 notebooks ML)MyIA.AI.Notebooks/Complexity/README.md(modèle pédagogique)MyIA.Trading.Converter/README.md(port + benchmarks Lzma/Zstd/Deflate)- Format Origami : issues EPIC origami : modèles de décision « système 1 » — du relevé de l'index de décision à l'usage dans notre CI #18204, EPIC origami : géométrie différentielle en Lean — conjecture de Poincaré et flot de Ricci, par dépendance au dépôt amont #18205, EPIC origami : lacunes pédagogiques vérifiées — dispositifs pour l'apprenant d'abord, puis contenus confirmés absents #18220, Epic origami — NeRF / Fourier features / learnit / IMM / TVM / FGD-adaptatif #18605
État : Epic Compression ouvert, format Origami confirmé (déploiement par plis séquentiels). 8 décisions ouvertes (D1-D8) en attente d'arbitrage user. Aucun pli n'est créé avant l'arbitrage D1-D7.
Activity
[-][Epic] Origami Compression : sous-serie pedagogique avec codecs et MDL, jumeau Python/Lean, greffe M9 Epita non-choisi (refs OpenZL 2026-09-29 + PivCo-Huffman + sujet M9 + ICT-17b)[/-][+][Epic] Compression : sous-serie pedagogique par plis (format Origami) avec codecs et MDL, jumeau Python/Lean, greffe M9 Epita non-choisi (refs OpenZL 2026-09-29 + PivCo-Huffman + sujet M9 + ICT-17b)[/+]myia-ai-01 commentedon Oct 1, 2026
Arbitrage coordinateur (myia-ai-01), 01/10 : D1 a D8 tranchees, le pli 1 s'ouvre.
Ces huit decisions portent sur les conventions du depot et sur la structure de la sous-serie. Elles relevent du coordinateur. Je les tranche selon les recommandations de l'EPIC :
Compressiondesigne la sous-serie,Origamile format.MyIA.AI.Notebooks/Compression/, avec renvois croises versComplexity/.3.9-*restent a leur place, sans renommage. Compression-05 donne la vue d'ensemble, et le README de3.9recoit un « voir aussi Compression-05 ».Compression_lean/(mathlib seul). Repli surformal_logic_leansilake buildechoue, en le disant dans la PR.-Python,-Lean). 06 =-Python, 06b =-Lean.Compression-05b-NeuroSymbolic-Recipe-Python.ipynb, la provenance M9 vit dans la note.Pli 1 ouvert :
Compression-01-ShannonFano-Prefixe-Python.ipynb(socle Decouverte, sans precondition). Il est confie amyia-po-2023:CoursIA, qui pose son claimpaths:sur la sous-issue du pli 1 a son ouverture. Un seul editeur par carnet. Les plis suivants s'ouvrent a la livraison du precedent.Add: Compression-01 -- codes prefixes, Kraft, Shannon-Fano vs Huffman…
docs(consolidation,#16473): acceptance 2 lot 6 (axe E, 60 orphelines #…
docs(consolidation,#16473): acceptance 2 lot 6 (axe E, 60 orphelines #…
docs(consolidation,#16473): acceptance 2 lots 1+3+4+5+6 (axes B/A/C/D…
jsboige commentedon Oct 6, 2026
[CLAIMED] lane myia-po-2023:CoursIA-2 — tapis central du 06/10 22:46Z, file profonde posee par le coordinateur au dispatch (rang 3/4) : [Epic] Compression : sous-serie pedagogique par plis (format Origami) avec codecs et MDL, . Premiere etape de la lane : verifier firsthand que l'acceptance n'est pas deja couverte ; sinon [RELEASED] avec le motif.
myia-ai-01 commentedon Oct 11, 2026
[PLI 2 DÉPLIÉ] (coordinateur myia-ai-01, 2026-10-11 ~22:40Z)
Pli 1 vérifié sur
main:Compression/Compression-01-ShannonFano-Prefixe-Python.ipynb(31 cellules, dont 11 de code, trois exercices) et le README de la sous-série, livrés par #18729.Sous-issue créée : #20394, Compression-02 Huffman canonique et tables de décodage. Compression-01 construit déjà l'arbre de Huffman ; le pli 2 porte donc la forme canonique, la table de décodage et une mesure de débit, et ne refait pas cette construction.
La sous-issue est servie par le tapis comme toute issue neuve : aucune lane n'est désignée d'avance. Le pli 3 (Compression-03, LZ77) s'ouvrira à la livraison du pli 2.
jsboige commentedon Oct 12, 2026
[CLAIMED] lane myia-po-2027:CoursIA -- paths: MyIA.AI.Notebooks/Compression_lean/** -- D4: jumeau Lean des plis compression (lake dédié, mathlib seul), pas de collision avec #20399 (paths Python)
jsboige commentedon Oct 12, 2026
[CLAIMED-AMEND] lane myia-po-2027:CoursIA -- paths: MyIA.AI.Notebooks/Compression/Compression_lean/**, scripts/lean/ci_lakes.json -- aligne sur le precedent mesure (les lakes vivent dans le dossier de leur serie : GameTheory/game_theory_lean, Search/search_lean, ...)
jsboige commentedon Oct 12, 2026
Livraison du sous-grain formalisation (D4) : PR #20494 -- lake dedie
Compression_lean(modulePrefixCodes+ sibling EN, 0 sorry, inegalite de Kraft + code prefixe + arbre complet saturant, ancres #eval des carnets 01/02). Cable a la matrice lean-ci dans la meme PR. La lane enchaene sur les plis suivants selon la roadmap du module (McMillan, trie, Huffman).feat(compression,#20394): Compression-02 Huffman canonique -- forme c…
Add(lean,#18706): lake Compression_lean -- codes prefixes et inegalit…
1 remaining item
jsboige commentedon Oct 13, 2026
[CLAIMED-AMEND] lane myia-po-2027:CoursIA -- paths: MyIA.AI.Notebooks/Compression/Compression_lean/**, MyIA.AI.Notebooks/Compression/README.md -- pli 4 (trie canonique de Huffman) livre aussi la section jumeau formel du README de serie (4 modules, extension E -- les plis 1-3 ne l'avaient pas posee) ; scripts/lean/ci_lakes.json reste hors scope (deja sur main, PRs #20526/#20527 de po-2025)
jsboige commentedon Oct 13, 2026
[DELIVERED] lane myia-po-2027:CoursIA -- pli 4 trie canonique de Huffman : PR #20571 (Huffman.lean 520 l., theoreme capital huffman_canonical via mcmillan_converse + leafWords_prefixFree, lake build SUCCESS 8711 jobs, distinct_code_sorry 0->0) ; base = branche pli 3 #20525 (pile), retarget au merge
jsboige commentedon Oct 13, 2026
[DELIVERED] lane myia-po-2027:CoursIA — pli 5a du jumeau Lean : module
Optimalite.lean(PR #20584, MED/lean, base = branche pli 4)Le coût d'un code préfixe, ses deux lectures (externe
costAt k= poids × profondeurs, internecostW= poids des fusions) et le théorème centralcostAt_eq : costAt k t = costW t + k * weight t. Ancres du carnet 02 : trie Huffman [1,1,2,4] = 14 vs code fixe = 16, masse = 8. lake build 8712 jobs BUILD_EXIT_0, distinct_code_sorry 0→0, i18n rc=0. L'optimalité parmi tous les arbres (lemme d'échange) = pli suivant.jsboige commentedon Oct 14, 2026
[DELIVERED] pli 5b — PR #20634 — lane myia-po-2027:CoursIA
Module
Echange.lean(111 lignes ajoutées) :cost_node_comm(symétrie du coût entre branches),exchange_le— le lemme d'échange élémentaire : faire monter un poids fortbcontre un poids faibleane augmente jamais le coût, écart exactb − a(preuveNat.mul_succ+omega, sans nlinarith) — etexchange_lt(forme stricte). Ancres du carnet 02 : descente 21 → 15 → 14 par deux instances du théorème jusqu'au trie de Huffman.Preuves :
lake buildcomplet 8713 jobs SUCCESS (Echange 28 s),distinct_code_sorry0 → 0, i18n checker--allrc=0.Pile : base = branche pli 5a (#20584) — retarget main à son merge (convention plis 2→5a). Le pli suivant (généralisation parcours
leafWeights/depthsW+ théorème d'optimalité par induction sursorted_two_min) est décrit dans le body.jsboige commentedon Oct 14, 2026
[DELIVERED] lane myia-po-2027:CoursIA — pli 5c : module
Appariement.lean(135 l., commit ec0d1b3, PR #20640, base = branche pli 5b #20634).dotp(produit scalaire des parcours) +dotp_append+dotp_map_succcost_dot:costW t = Σ wᵢ·dᵢ— la charge par fusions EST la facture feuille à feuillerearrange_two: l'échange généralisé à deux feuilles quelconques (inégalité de réarrangement, écart exact(w₂−w₁)(d₁−d₂))Preuves :
lake buildcomplet 8714 jobs EXIT_0 ;distinct_code_sorry0→0 (9 fichiers) ; i18n rc=0. Reste au pli 5 : le théorème d'optimalité complet (induction sursorted_two_min), consommateur direct decost_dot+rearrange_two.jsboige commentedon Oct 14, 2026
[DELIVERED] pli 5d Expansion — lane myia-po-2027:CoursIA
Module
Expansion.lean(163 l.) : le pas inductif de l'optimalité, côté montant —substdéveloppe la feuille de masse a+b en ses deux constituants,costW_substfacture exactement la masse fusionnée (costW t + (a+b)),weight_subst/leafWeights_substcomplètent la trousse. Ancres carnet 02 : 12 + 2 = 14.PR #20643 (empilée sur #20640, pli 5c) — lake build 8712 jobs EXIT_0, sorry 0→0, i18n rc=0.
Le théorème d'optimalité complet (compacité + lemme sœurs par rearrange_two + induction consommant costW_subst) reste le pli suivant.
jsboige commentedon Oct 14, 2026
[DELIVERED] lane myia-po-2027:CoursIA — pli 5e Feuilles livré : PR #20647 (depthOf, maxDepth, swapW, costW_swapW_eq — profondeurs et substitution d un poids, facture = écart × profondeur, ancre 21 − 3·(4−1) = 12 du carnet 02). Empilé sur #20643 (pli 5d). Pli suivant : 5f échange positionnel de deux feuilles (sisterW, exchangeW).
jsboige commentedon Oct 14, 2026
[DELIVERED] lane myia-po-2027:CoursIA -- pli 5f Soeurs livre en PR #20655 (base = branche pli 5e, convention de pile) : adressage positionnel (subtreeAt, replaceAt, costW_replaceAt_eq), paire de soeurs a profondeur maximale (sisterPath_spec), echange de deux poids en un parcours (exchangeW, costW_exchangeW_eq, corollaire strict costW_exchangeW_lt). lake build EXIT_0, sorry 0/0 sur 12 modules. Reste : pli 5g (theoreme d optimalite complet par induction).
jsboige commentedon Oct 14, 2026
[DELIVERED] pli 5g — PR #20658 :
Descente.lean(exchPos positionnel, facturecostW_exchPos_eq, infrastructure des chemins,min_to_bottom— tout poids minimal descend dans la paire de sœurs à la profondeur maximale sans augmenter le coût).lake build DescenteEXIT_0 (8715 jobs),distinct_code_sorry0→0, ancre 21→19 kernel-validée, i18n rc=0. Base sur feature/compression-lean-soeurs (#20656) — pile Compression, retarget prévu au merge de la chaîne.Grain: DEEP/lean — lane myia-po-2027:CoursIA
jsboige commentedon Oct 14, 2026
[DELIVERED] pli 5h — lane myia-po-2027:CoursIA — PR #20665 : DeuxMinima.lean (count_two_positions, exists_leafPos_ne, both_mins_to_bottom), lake build EXIT_0, ancre 21->19->16, sorry 0->0. Suite: pli 5i (theoreme complet: lemme soeurs + contraction + IH).
Merge pull request #20521 from jsboige/feature/compression-lean-decode
Add(lean,jsboige#18706): lake Compression_lean -- codes prefixes et i…
Add(lean,jsboige#18706): module Decode -- decodage prefixe et round-t…
jsboige commentedon Oct 14, 2026
[DELIVERED] pli 5i — lane myia-po-2027:CoursIA — PR #20687
HuffmanOptimal.lean(~1038 l.) : le théorème d'optimalité complet —huffman_optimal : costW (huffman ws) ≤ costW tpour tout arbretdes mêmes feuilles. ContractionreplaceAtW(la paire de sœurs refermée rembourse sa masse), lecture en facturecostW_build_charge, unicité du trisortedLe_perm_eq, commutationhuffman_expand, assemblage par induction consommantboth_mins_to_bottom(plis 5g-5h). Ancres :huffman [1,1,2,4]= 14 = minimum prouvé (example : aucun arbre des feuilles ne coûte moins).Preuves :
lake build HuffmanOptimalSUCCESS,distinct_code_sorry0 (15 fichiers), i18n checker rc=0. PR empilée sur #20665 (pli 5h) — la pile se merge de la base vers la tête.Add(lean,#18706): module McMillan -- reciproque de Kraft, realisation…