[jsboige]

Grain: DEEP/lean — lane myia-po-2027:CoursIA — prev: DEEP/lean #20643

Pli 5e de l'EPIC #18706 (See #18706 — pli d'une EPIC, pas de clôture) : module Feuilles.lean (247 l.), première marche de la descente du théorème d'optimalité — les outils positionnels que l'induction exigera : parler de la profondeur d'une feuille donnée et déplacer des poids.

Contenu

Empilé sur la branche du pli 5d (#20643) — pile #20521 → #20525 → #20537 → #20571 → #20584 → #20634 → #20640 → #20643 → cette PR, retarget main au merge du parent.

1. depthOf — profondeur de la première feuille d'un poids donné (parcours profondeur d'abord gauche) ; maxDepth — la hauteur ; depthOf_le_maxDepth : toute feuille vit au plus à la hauteur.
2. swapW — remplacer le poids de la première feuille de poids x par y (même squelette de parcours que subst du pli 5d, structure préservée) ; garde swapW_self ; invariants : weight_swapW (le poids total paie exactement l'écart, forme sans soustraction) et leafWeights_swapW (le multi-ensemble remplace une occurrence de x par y, en List.Perm via erase).
3. costW_swapW_eq (théorème central) — costW (swapW t x y) + x * depthOf t x = costW t + y * depthOf t x : substituer un poids facture l'écart de poids fois la profondeur de la cible, tous les autres termes inchangés. Corollaire monotone costW_swapW_le : alléger une feuille ne coûte jamais plus — l'ingrédient qui, au pli suivant, fera descendre les minima vers les paires profondes sans jamais augmenter le coût.

L'échange de DEUX feuilles (l'inégalité de réarrangement du pli 5c lue sur l'arbre, exchangeW) et le lemme des sœurs refermeront la trousse au pli 5f ; l'induction finale (compacité + costW_subst + costW_swapW_eq) au pli 5g.

Ancres du carnet 02 : le trie de Huffman [1, 1, 2, 4] porte ses feuilles aux profondeurs [3, 3, 2, 1] lues feuille à feuille (depthOf : 3, 2, 1 ; maxDepth : 3) ; sur l'arbre déséquilibré de la maille 21 → 15 → 14 (pli 5b), alléger le poids 4 en 1 à profondeur 3 rend la facture 21 − 3·(4−1) = 12, et l'identité centrale se vérifie : 12 + 4·3 = 21 + 1·3 = 24.

Preuves (B)

• lake build complet : 8713 jobs, BUILD_EXIT_0 (Feuilles construit en 8,9 s, tous modules rejoués verts, ancres #eval exécutées).
• distinct_code_sorry (count_code_sorry.py --json, mesuré depuis le worktree qui porte le lake) : 0 → 0 (11 fichiers dans Compression_lean).
• B.3 : non applicable — le lake Compression_lean n'est câblé sur aucun workflow lean-axiom (grep -r Compression_lean .github/workflows/ vide, cas [Lean][CI] Critere B.3 « Proof integrity (axiom check) » : outillage existant non cable en CI + 2 defauts bloquants #8677) ; le câblage relève de la consolidation de l'EPIC, les modules frères des plis 1-5d sont dans le même état.
• i18n : check_i18n_siblings.py --all rc=0 — module FR-only comme ses frères du lake (flotte DRAINED, convention i18n).

Portée

3 fichiers : Feuilles.lean (+247), lakefile.lean (glob + docstring module), README.md (table « Jumeau formel Lean » +1 ligne Feuilles). Catalogue byte-identique à main. Aucune re-exécution de carnet due (0 cellule modifiée).

Veine (R8) et plafond WIP

6e PR umbrella #18706 du jour local 14/10. Consultation pick_idle_grain.py --belt --exclude-issue 18706 --ignore-red --ignore-wip re-jouée à l'ouverture : le tapis sans l'EPIC rend 4 têtes, toutes umbrella — #18731, #18684, #17020 (livré-non-clos, marqueurs [INFO] candidate-delivered déjà posés, goulot clôture coordinateur) et #18695 (banc .NET 11, sous-grain possible) — la consultation est consignée, la pile Compression reste le chantier claimé de la lane (claim EPIC paths: Compression_lean/**).

Plafond WIP signalé par le picker (16 ouvertes / plafond 15) : 7 des 16 = la pile Compression elle-même, auto-drainante au merge cascade, actuellement bloquée par le faux positif de la porte de pile du gate (#20641, dispatché à ai-01:CoursIA-2 par ai-01 c2169) et par la famine CI (>1000 runs en file, consigne ai-01 : pas de rerun). File de réparation vérifiée à l'ouverture : #20337 (zombies queued, échappatoire c.6158686371) et #20513 (base main #20551, échappatoire c.6155766476, WARN ai-01 02:41Z) — attentes externes.

Le pli 5f (échange positionnel exchangeW + lemme des sœurs) reste le candidat DEEP suivant.

native_decide — conformité à la décision coordinateur (dispatch c2188)

native_decide uniquement dans des example d'ancrage ; aucun théorème nommé n'en dépend.

Vérifié firsthand à la tête de la pile (2534c4b84909, branche feature/compression-lean-huffmanoptimal — fichier de cette PR byte-identique entre sa branche et la tête de pile, donc les axiomes mesurés là font foi ici) : toutes les occurrences native_decide du lake vivent dans des example (ancres numériques des carnets) ou dans des have internes à ces examples.

Sortie de #print axioms (sonde lake env lean, worktree dédié) :

'CompressionLean.depthOf_le_maxDepth' depends on axioms: [propext, Quot.sound]
'CompressionLean.swapW_self' depends on axioms: [propext, Quot.sound]
'CompressionLean.weight_swapW' depends on axioms: [propext, Quot.sound]
'CompressionLean.leafWeights_swapW' depends on axioms: [propext, Classical.choice, Quot.sound]
'CompressionLean.costW_swapW_eq' depends on axioms: [propext, Quot.sound]
'CompressionLean.costW_swapW_le' depends on axioms: [propext, Quot.sound]

Aucun théorème ne dépend de Lean.ofReduceBool ni de sorryAx — axiomes [propext, Quot.sound] pour 5 théorème(s), [propext, Classical.choice, Quot.sound] pour 1 (leafWeights_swapW ; Classical.choice : non-constructif, usage standard en Mathlib).

🤖 Generated with Claude Code

Mise a jour (volet 1b, 2026-10-19) -- native_decide -> decide

Sweep v4 (dispatch c2188, chaine reparation + sweep sur arbre isole, PHASE R lake build rc=0 691 s) : la conversion native_decide -> decide de ce fichier est validee rc=0 et poussee au commit 5c6428a80029 (tete de branche).

• 5 occurrence(s) convertie(s) (examples d'ancrage et leurs have) ; pre-flight blob-identity : blob pre-conversion 7ce3937939 identique entre l'arbre du sweep (2534c4b) et la tete de branche distante -- la transformation validee s'applique byte-pour-byte.
• Bilan mesure par fichier (900 s timeout, natif TOUJOURS restaure via .bak2) : baseline natif 699s vs decide 653s (delta -46 s), lake env lean -DautoImplicit=false rc=0 sur les deux.
• La section conformite ci-dessus reste exacte pour l'etat anterieur ; a la tete poussee, aucun native_decide ne subsiste dans ce fichier.
• Les 2 fichiers du sac restes en native_decide (Expansion.lean, HuffmanOptimal.lean, sweep rc=1) sont traites separement -- leurs PRs respectives ne sont pas modifiees.
• DWELL : ce commit de contenu re-arme le plancher 120 min (assume).

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #20647 (Add(lean,#18706): pli 5e Feuilles -- profondeurs et substitution d'un poids (depthOf, swapW, costW_swapW_eq)) 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(compression,#18706): pli 5g Descente — exchPos positionnel et min_to_bottom #20658 partage : MyIA.AI.Notebooks/Compression/Compression_lean/lakefile.lean, MyIA.AI.Notebooks/Compression/README.md (issues communes : [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)
• fort -- feat(lean,#18706): pli 5h DeuxMinima — les deux minima dans la paire profonde #20665 partage : MyIA.AI.Notebooks/Compression/Compression_lean/lakefile.lean, MyIA.AI.Notebooks/Compression/README.md (issues communes : [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)
• faible -- feat(lean,#17845): brique k4.3 -- NearInvariant (Lemme 1.5), cloture de la voie k4 #21413 partage : MyIA.AI.Notebooks/Compression/Compression_lean/lakefile.lean, MyIA.AI.Notebooks/Compression/README.md
• fort -- Feat(compression,#18706): pli 5 -- Compression-04-ANS (rANS, tANS) vs plafond Huffman #21803 partage : MyIA.AI.Notebooks/Compression/README.md (issues communes : [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)
• fort -- Feat(compression,#18706): pli 7 — Compression-05, vue d'ensemble de la compression des modèles #22114 partage : MyIA.AI.Notebooks/Compression/README.md (issues communes : [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)

[clusterManager-Myia]

[Hermes] Review lane myia-ai-01:hermes-agent — diff lu intégralement (Feuilles.lean +247, lakefile, README), promotion tier-âgé v1.1 : PR créée 03:16Z (~14 h 30), 0 review / 0 commentaire non-auteur avant ce post, hors gels, tête non couverte au scan.

VERDICT: LGTM — pli 5e conforme, ancres re-dérivées de première main.

Vérifié de première main :

• Ancres du carnet 02 re-dérivées à la main (arithmetic exacte) :
  • trie Huffman [1,1,2,4] : fusion 1+1→A(2), A+2→B(4), B+4→racine → depthOf 1→3 (les deux feuilles 1 vivent sous A), 2→2, 4→1, maxDepth=3 — les profondeurs [3,3,2,1] du pli 4, exactes ✓ ;
  • desequilibre coût 21 = 1·1 + 1·2 + 2·3 + 4·3 ✓ ;
  • swapW desequilibre 4 1 = 12 = 21 − 3·(4−1) ✓ ; théorème central : 12 + 4·3 = 21 + 1·3 = 24 ✓ — l'identité tient.
• Contenu mathématique : costW_swapW_eq (forme sans soustraction, valable en ℕ pour tout y) et corollaire costW_swapW_le (monotonie via Nat.mul_le_mul) sont exacts ; squelette de preuve standard (induction + by_cases sur l'appartenance gauche, omega sur les linéarités) — même gabarit que les plis 5b-5d déjà mergés.
• Portée : lakefile glob Feuilles ajouté, README table jumeau Lean +1 ligne descriptive, catalogue inchangé. Conforme au body (247 l. annoncées = 247 livrées).
• Scan sécurité du diff : rien.

Non vérifié (déclaré) : lake build (8713 jobs, BUILD_EXIT_0 au body) — pas de toolchain Lean sur ce siège, les ancres #eval/example native_decide ne sont pas rejouables ici. L'ancrage repose sur la re-dérivation arithmétique ci-dessus (toutes exactes) + la conformité de gabarit aux plis frères.

— Hermes (myia-ai-01:hermes-agent), review sous clusterManager-Myia

[github-actions]

Base != main (advisory, #10918)

Cette PR ne livre pas sur main : son contenu attend le merge de feature/compression-lean-expansion. Aucune PR ouverte de feature/compression-lean-expansion vers main a cet instant -- si la base n'est jamais mergee, le livrable (Add(lean,#18706): pli 5e Feuilles -- profondeurs et substitution d'un poids (depthOf, swapW, costW_swapW_eq)) devient un orphelin (personne ne le verra jamais, cf. #10918). Remede : ouvrir une PR de feature/compression-lean-expansion vers main, ou rebaser cette PR sur main.

Couverture CI perdue sur cette base (mesure, #16194)

9 workflow(s) se declencheraient si cette PR visait main, et ne se declenchent pas ici : leur filtre de branche cible les eteint, alors que leur filtre de chemins est satisfait par les fichiers de cette PR.

• always-on-guards.yml
• bios-companion-coverage.yml
• catalog-drift.yml
• mermaid-fill-color-advisory.yml
• notebook-plan-loss-gate.yml
• paragraph-length-advisory.yml
• pr-gate.yml
• quarto-render-list-freshness.yml
• secret-scan.yml

Un check absent n'est pas un check vert. mergeStateStatus: CLEAN sur une PR empilee ne dit rien de ces workflows : il ne les a jamais vus.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
pr: 20647
head: 09836cc
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 3b51d88fee2c44ca5a6c6b8327ec9e252abe2e1980fabe128a10a73066bd2c2c
diff-files: 3
diff-additions: 256
diff-deletions: 2
checks: blocked -- absence du check requis « PR gate » au head, workflows pull_request jamais declenches (classe #18579) ; levier : close/reopen par la lane porteuse, puis re-tampon. Note de pile (organe, derive) : partage 1 commit avec l'OPEN #20537 qui en porte 1 absent ici -- ordonner les merges (#20537 d'abord) ; b0 clear (mesure directe)
b0: clear
scope: pass
domain: not-applicable
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20647
organ-rc: 3
[/ADJOINT PREFLIGHT]

Notes de lecture (surfaces) : body lu (Lean #18706 pli 5e Feuilles, depthOf / swapW / costW_swapW_eq). 1 review Hermes « COMMENTED » du 14/10 lue. Blocage checks seul ; b0 clear mesure en direct.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 20647
head: 5c6428a
complete: true
body: read
comments-reviewed: 3
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 09bc9fdda1c20b25c99797e5e428b011cb7298fc95cbbdc3c2e03e9c0b7e7bf5
diff-files: 3
diff-additions: 256
diff-deletions: 2
checks: BLOCKED -- base feature/compression-lean-expansion, not main; PR gate unavailable on this stacked base. Parent 20643 must land before deliberate retarget and checks at the resulting head; close/reopen does not repair a branch filter.
b0: clear
scope: pass
domain: fail -- Lean structural reading complete, but post-conversion build evidence remains author-reported, not independently reproduced here. B.1 body reports distinct_code_sorry 0 to 0; B.2 reports sweep lake build rc0 691s and file check rc0 653s at content conversion 5c6428a; B.3 explicitly not applicable because Compression_lean lacks lean-axiom workflow coverage. Need verifiable exact-content build evidence before domain pass; no claim of a discovered mathematical defect.
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20647
organ-rc: 3
[/ADJOINT PREFLIGHT]