Repository navigation
Notebook(lean, #16781 veine 5) — carnet consommateur du lake iit_lean : note de conception puis escalier #20414
Description
Part of #16781 (Epic Aaronson, veine 5 — « l'objet qui a mordu IIT, en Lean »).
Constat mesuré
Le lake iit_lean a été livré par #18599 (veine 5, moitié formelle) : 220 lignes de Lean sans dépendance Mathlib, 0 sorry, paire i18n FR/EN (IIT/Integration.lean + IIT/Integration_en.lean), enregistré dans scripts/lean/ci_lakes.json.
Aucun carnet ne le consomme. Mesure du 2026-10-12 sur main : git grep -l "iit_lean" -- "*.ipynb" → 0 hit. Le carnet IIT-06-L-Objet-qui-a-Mordu-IIT.ipynb (33 cellules exécutées) porte la moitié empirique (Φ_DM sur F_p, grilles PyPhi) et n'importe pas le lake : la moitié formelle n'a pas de porte d'entrée pédagogique.
La carte Lean phase 1 le range explicitement hors de ses tranches : « Lakes sans carnet consommateur (differential_lean, iit_lean) : à traiter à part, hors carte » (#17545, c.6108479114). Son carnet d'exposition appartient donc à cet Epic (note de rattachement c.6108531719 sur #16781).
Ce que le mainteneur demande d'abord : la note de conception
Le mandat est posé par la carte (#17545, c.6108479114) : « Chaque tranche commence par une note de conception », structurée en quatre points —
- Inventaire du lake — pour chaque module et théorème notable : le carnet qui l'expose, ou « non exposé ».
- L'escalier — l'ordre des carnets et les marchepieds, avec ce que chaque marche ajoute.
- Le capstone — ce qu'il consomme des marches, ce qu'il montre, sa place dans la mère.
- Les modules non exposés — lesquels méritent un carnet (grain de contenu à part), lesquels restent internes, en le disant.
Ici l'inventaire est entièrement « non exposé » (19 déclarations — abbrev, structure, def et theorem —, zéro carnet), ce qui rend la note d'autant plus nécessaire : c'est elle qui décide la forme de l'escalier, l'ordre des marches, et la place du carnet dans la série.
Livrables
- Note de conception —
docs/lean/iit-lean-escalier.md, selon les quatre points ci-dessus (inventaire nominatif des 13 items du lake avec leur verdict d'exposition, ordre des marches, capstone, décisions de placement et de nommage). - Premier carnet de l'escalier (grain de contenu séparé, après la note) — noyau
lean4-wsl, la marche 1 telle que la note la définit. - Les marches suivantes et le capstone, en grains distincts.
Acceptance
- La note existe sur
main, avec l'inventaire nominatif vérifiable contreIIT/Integration.lean(chaque définition/théorème cité existe, et son verdict d'exposition est mesuré). - La question de placement et de nommage du carnet est tranchée ou explicitement reportée avec son motif (la numérotation
Lean-NNest sous renumérotation dans la tranche T7 de la carte : poser un numéro nu pendant T7 est un risque nommé). - Le premier carnet est livré avec outputs réels (C.2), exécuté sous
lean4-wsl. - La ligne du README de série qui présente le carnet est livrée avec lui (pas de total de notebooks mis à jour à la main — le catalogue relève de sa régénération).
Activity
jsboige commentedon Oct 12, 2026
[CLAIMED] lane myia-po-2027:CoursIA -- note de conception de l escalier iit_lean (livrable 1 de l issue)
Grain: MED/docs -- lane myia-po-2027:CoursIA -- prev: DEEP/research-code #20409
paths: docs/lean/iit-lean-escalier.md
Garde anti-collision passee avant claim :
gh pr list --state all --search 20414-> 0 PR,git worktree list-> aucun worktree nomme pour cette issue,git grep -l iit_lean -- "*.ipynb"-> 0 hit (constat du body reconfirme sur main au 2026-10-12).jsboige commentedon Oct 12, 2026
Livraison de l'etape 0 : PR #20415 —
docs/lean/iit-lean-escalier.md, la note de conception.Elle porte les quatre points du mandat : inventaire nominatif des 19 declarations de
IIT/Integration.lean(ligne, genre, enonce, verdict d'exposition — les 19 sont non exposees), l'escalier en trois marches, le capstone et son grade honnete, la table des modules non exposes.Deux choses y sont explicites plutot que tranchees en silence :
IIT/porte deja un cas hors grammaire (IIT-06-L-...fait lireLcomme une lettre d'accretion majuscule). La note proposeIIT-07-L-Integration-Par-Coupes-Lean.ipynbet renvoie la confirmation au mainteneur ou au coordinateur : le nommage est un acte pedagogique.lake buildn'a pas ete execute dans ce cycle ; le « build en secondes » est repris du README du lake, pas remesure.Correction factuelle sur le body ci-dessus : il annoncait « 13 definitions » dans la section des livrables 1 ; le recompte sur l'artefact en donne 19. Body corrige.
Suite : le carnet de la marche 1 (grain de contenu, noyau
lean4-wsl) des que le nom est confirme.Refs #20414.
jsboige commentedon Oct 12, 2026
[RELEASED] lane myia-po-2027:CoursIA — #20414
J'ai posé un claim sur ce grain à 00:53Z (commentaire précédent), après une garde anti-collision revenue vide :
gh pr list --state all --search 20414→ 0 PR,git worktree list→ aucun worktree nommé pour cette issue,git grep -l iit_lean -- "*.ipynb"→ 0 hit.La garde était en retard sur la réalité. La PR #20415 (lane
myia-po-2024:CoursIA, ouverte 2026-10-12T00:51:01Z) livre déjàdocs/lean/iit-lean-escalier.md— le livrable 1 de cette issue — sur la branchedocs/20414-iit-lean-escalier. Une PR de ma part serait un doublon du même livrable sur le même chemin : je ne la pousse pas, et je libère le claim.Le grain reste porté par #20415, qui a l'avance (ouverte, à la tête
d8e6a0e58721). Rien à reprendre de mon côté.Note d'instrument, pour le prochain tirage.
gh pr list --searchne voit pas une PR créée dans les ~2 minutes (indexation). Sur un grain neuf — issue ouverte 4 minutes avant la PR — la garde anti-collision doit interroger la branche envisagée (git ls-remote origin refs/heads/<nom>) avant de se fier à la recherche textuelle. C'est la seule des quatre ancres qui a répondu juste ici.🤖 Generated with Claude Code
jsboige commentedon Oct 12, 2026
[DELIVERED] lane myia-po-2024:CoursIA -- PR #20419 : livrable 2, premier carnet de l'escalier (marche 1 = items 1-10 de la note) -- execute lean4-wsl --cwd lake-root, 12/12 cellules 0 erreur, C.2 verifiee (12/12 exec_count non null + outputs), 3 exercices pattern Lean-13b, ligne README de serie livree avec le carnet. Hypothese de nommage sans lettre L consignee dans le body de la PR (amend du claim pose : voir #16781). Livrable 1 (note de conception) : #20415 en revue. Restent : marches 2 et 3 en grains distincts.
feat(iit,#20414): IIT-08 — marche 2 de l'escalier iit_lean (la parité…
jsboige commentedon Oct 12, 2026
[DELIVERED] marche 2 (livrable 2, partie parite) : PR #20423 -- IIT-08-Parite-De-Bout-En-Bout-Lean.ipynb, 12/12 executees 0 erreur, items 11-16 exposes, stackee sur #20419. Ligne README IIT deferree au reglement du couplage #20400/#20419 (c.6116385850 sur #20419, DM ai-01 01:57Z).
feat(iit,#20414): IIT-07 marche 1 escalier iit_lean -- la coupe et le…
Fix(iit,#20414): voie (b) -- rebrancher la chaine de navigation de la…
feat(iit,#20414): IIT-08 — marche 2 de l'escalier iit_lean (la parité…
docs(lean,#20414): note de conception de l'escalier du lake `iit_lean` (
Fix(iit,#20414): prose re-ancree sur les outputs reels (review NanoCl…
jsboige commentedon Oct 14, 2026
[CLAIMED] lane myia-po-2023:CoursIA -- paths: docs/lean/iit-lean-escalier.md, MyIA.AI.Notebooks/IIT/IIT-07-*.ipynb, MyIA.AI.Notebooks/IIT/README.md -- note de conception (4 points) puis marche 1 : carnet consommateur du lake iit_lean, kernel lean4-wsl
Fix(iit,#20414): restaurer la note de conception (#20415) intacte -- …
jsboige commentedon Oct 14, 2026
[DELIVERED] lane myia-po-2023:CoursIA -- marche 1 livree par PR #20645 (tete 84c6c7e) : carnet IIT-07-Coupe-et-Decomposabilite-Lean (34 cellules, 11/11 executees kernel lean4-wsl, 0 erreur, axioms [propext, Quot.sound] seuls) + README serie + inventaire (Notebook cable 0->1). Point d'attention : le premier commit ecrasait la note de conception livree par #20415 -- restauree integralement (delta net +13/-0, bloc d'etat date prefixe, commit 84c6c7e). Nommage du carnet : grammaire recommandee par la note (noyau -Lean dernier, sans L) ; le numero reste la decision reservee au mainteneur/coordonnateur, renommage = suivi trivial. Marches 2 (parite) et 3 (capstone) restent en grains distincts.
jsboige commentedon Oct 14, 2026
Correction de mon [DELIVERED] (c.6159838577) : la marche 1 etait deja en review par #20419 (po-2024:CoursIA, ouverte 12/10 01:31Z, dossier READY) -- mon claim du 14/10 02:36Z etait posterieur, mon controle de collision a rate la PR ouverte. Ma PR #20645 est fermee en doublon par ma lane ; le canon marche 1 = #20419. Livrable note (livrable 1) : inchange, merge par #20415. La marche 2 (declarations 11-19, non couvertes par #20419) suit sous #20649 — carnet d'abord, README apres merge #20419 (paths partages).
Merge pull request #20419 from jsboige/feature/20414-iit-lean-marche1
docs(iit,#20649): suivi post-merge 20419 -- ligne 8 README IIT-08 + i…
feat(iit,#20414): IIT-08 — marche 2 de l'escalier iit_lean (la parité…