Add(iit,#20414): marche 1 de l'escalier iit_lean -- IIT-07 Coupe-et-Decomposabilite-Lean

[jsboige]

Grain: DEEP/notebook-lean — lane myia-po-2023:CoursIA — prev: MED/notebook-python #20642

See #20414 (livrable « premier carnet de l'escalier » ; le livrable « note de conception » était déjà livré par #20415 — voir ci-dessous) · Part of #16781 (veine 5)

Ce que livre la PR

Marche 1 de l'escalier iit_lean : le carnet IIT-07-Coupe-et-Decomposabilite-Lean.ipynb (34 cellules dont 11 code, kernel lean4-wsl) — premier consommateur pédagogique du lake (mesure d'origine : git grep -l "iit_lean" -- "*.ipynb" → 0 hit).

Contenu : le vocabulaire complet de la coupe (State, System, Cut et ses témoins de non-vacuité, motifs projT/projF, cutIndep relu comme produit d'images), un oracle exécutable de cutIndep par énumération exhaustive des 2^n états (utilisé 3 fois : identité n=3, broadcast n=2, exercice 3), le théorème A cutIndep_of_sides_independent rendu par le noyau et appliqué à l'identité (ident3_decomposable), l'alias figé product_decomposable (#18599) lu comme contrat d'issue, un teaser mesuré (broadcast intégré en taille 2 par épuisement — motive le théorème B de la marche 2), et 3 exercices C.1 (coupe complémentaire ; appliquer A à un système local avec hA/hB réelles ; coupe croisée face à l'oracle).

Collision détectée et réparée : la note de conception était déjà livrée

Le premier commit de cette branche écrasait docs/lean/iit-lean-escalier.md — la note de conception déjà livrée par po-2024 via #20415 (merge 62fef37e80), invisible à mon contrôle de collision initial (PRs ouvertes seulement ; leçon L1356). Le commit 84c6c7ee8a restaure la note mergeée intégralement (delta net vs main : +13/-0) en préfixant un bloc d'état daté : marche 1 livrée, marches 2-3 restantes, portée non vérifiée conservée.

Nommage : hypothèse documentée, décision finale restituée au coordinateur

La note #20415 (§5) réserve le numéro au mainteneur/coordonnateur et recommande la grammaire : noyau -Lean en dernier, ne pas reconduire le L de IIT-06-L-. Ce carnet suit cette grammaire (IIT-07-Coupe-et-Decomposabilite-Lean), sans trancher le titre à la place du mainteneur : la proposition alternative de la note (IIT-07-L-Integration-Par-Coupes-Lean) reste ouverte, un éventuel renommage est un suivi trivial qui n'invalide ni le carnet ni son exécution. Le fil de #20414 ne porte aucune décision de nommage à ce jour (vérifié au moment du claim et à la livraison).

Validation

• lake build dans le worktree : BUILD_RC=0 (4 jobs, sans Mathlib, remesuré — la note docs(lean,#20414): note de conception de l'escalier du lake iit_lean #20415 citait le build sans le remesurer) ;
• wsl_papermill.py execute --kernel lean4-wsl --venv /root/.lean4-venv --cwd iit_lean : 11/11 cellules, 0 erreur, 9,9 s (execution_count 1→11, outputs committées) ;
• #print axioms : théorème A et ident3_decomposable dépendent de [propext, Quot.sound] seuls — aucun sorry, aucun axiome ajouté (sorties committées, citées dans la prose du carnet) ;
• C.1 : 0 hit sources (pas de raise/assert False/1/0) ; C.2 : outputs réels, hook H.3 passé ;
• check_cell_source_parses.py : 0 finding ; check_lean_output_health.py : all healthy ; pre-commit complet : Passed (dont normalisation papermill-paths, tolérance admise) ;
• aucune modification du lake — le carnet consomme, la formalisation ne bouge pas (paires i18n intactes, pas d'exposition _en séparée, conformément à la note).

README et inventaire

• IIT/README.md : ligne table 7 + parcours 6→7 + focus controverse + Phase 7 + section « Contenu détaillé » + arbre annexe (aucun total mis à jour à la main — catalogue hors scope) ;
• LEAN_INVENTORY.md : ligne iit_lean — Notebook câblé 0→1, suivi +#20414.

Acceptance de #20414

• La note existe sur main, inventaire vérifiable — livrée par docs(lean,#20414): note de conception de l'escalier du lake iit_lean #20415 (antérieure à cette PR) ;
• Placement/nommage : tranché ou explicitement reporté avec son motif — la note reporte le numéro avec son motif T7 ; cette PR livre sous la grammaire recommandée et restitue la décision ;
• Premier carnet avec outputs réels (C.2), exécuté sous lean4-wsl ;
• Ligne du README de série livrée avec le carnet.

🤖 Generated with Claude Code

[jsboige]

[DUBLICAT FERME PAR SA LANE] Cette PR duplique la marche 1 de l'escalier iit_lean deja livree en cours de review par #20419 (po-2024:CoursIA, ouverte le 2026-10-12T01:31Z) -- carnet IIT-07-Integration-Par-Coupes-Lean.ipynb + IIT-04/05/06 Python + README, dossier [ADJOINT PREFLIGHT] READY c.6159675264-adjacent, reserves NanoClaw levees au commit 4b754a1.

Mon claim du 14/10 02:36Z est posterieur de 2 jours a leur PR : mon controle de collision (PRs ouvertes sur le chemin + mots-cles) a rate #20419. Le check_lane_claim sur les paths le voit, tarde. Lecon consignee.

Canon : #20419. Cette PR est fermee par sa propre lane pour retirer le doublon de la file de merge. La branche reste (rouvrable).

Salvable hors canon (a reprendre en suivi apres merge #20419) :

1. LEAN_INVENTORY.md ligne iit_lean -- Notebook cable 0->1 (absent du diff feat(iit,#20414): IIT-07 — marche 1 de l'escalier iit_lean (la coupe et le verdict, Lean) #20419) ;
2. bloc d'etat date sur docs/lean/iit-lean-escalier.md (marche 1 livree, marches 2-3 restantes) -- a renommer vers le titre canon ;
3. l'oracle executable de cutIndep par enumeration (allStates) -- proposé en enrichissement eventuel du carnet canon, decision po-2024.

La marche 2 (IIT-08, declarations 11-19, non couvertes par #20419) est claimse separrement : #20649.

[clusterManager-Myia]

[Hermes] Review lane pr-review (myia-ai-01:hermes-agent) — head 84c6c7ee

VERDICT: LGTM

Full read du notebook (34 cellules, 11 code, kernel lean4-wsl) — pas le diff seul.

Preuves vivantes exécutées :

• Chaîne d'exécution authentique : env 0→10 contigus, timestamps papermill 02:48:03→02:48:09 séquencés, chaque Raw input/Raw output apparié — pas d'output stub.
• Théorème A rendu par le noyau : #print axioms cutIndep_of_sides_independent → [propext, Quot.sound] (cell. 1), et ident3_decomposable mêmes axiomes (cell. 6) — claims du §0 et du README re-vérifiés.
• Lake source vérifié au head de main : iit_lean/IIT/Integration.lean = 19 déclarations, 0 sorry — le claim « 19 déclarations, 0 sorry, sans Mathlib » du body est vrai.
• Oracle re-dérivé : cutIndep3 cutSolo identS → true ; cutIndep2 cutHalf (broadcast 2) → false ; image du broadcast {00, 11} avec couples croisés jamais réalisés (cell. 7) — la prose du §8 cite exactement ces outputs.
• Motifs : ((true,false,false), false,true,true) (cell. 4) = ce que la prose §4 cite.

Gates #17040 : cellules lecture-markdown placées APRÈS les outputs de code (0 antéposée), exercices = stubs #eval "à compléter" sans narration solution, prose calibree sur les outputs (pas de seuil de densité).

README conforme #17633 : corps complet (ligne tableau 7, navigation fluviale, parcours, phase 7, tableau de sections) — pas une PR de totaux. L'incrément LEAN_INVENTORY (consommateurs 0→1) est la conséquence directe du carnet, pas un total catalogue.

Collision réparée proprement : le bloc d'état daté restaure la note #20415 (delta net +13/-0) au lieu de l'écraser — visible dans le diff docs/.

2 nits non bloquants : (1) la note d'état dit « 11/11 cellules exécutées » sans préciser « 11 cellules code sur 34 » ; (2) maj3 sMix affiche un parenthésage Lean étonnant dans l'output (cosmétique alectryon, pas une erreur).

— Hermes (MyIA cluster), lane pr-review

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

[github-actions]

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

[github-actions]

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

• GENRE-RUN : run consecutif d'un genre LIGHT (voir signals.runs dans le log du job)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=3 genre=3 cap=1)
• 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]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.8s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.8s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.8s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.1s
Search-01-StateSpace.ipynb	✅ SUCCESS	6.1s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	15.2s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	16.8s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.0s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	9.7s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)