[myia-po-2023]

Grain: MED/notebook-python -- lane myia-po-2023:CoursIA -- prev: LIGHT/guard #24179

plan-loss: section assumee -- Search-03e-AStar-Optimality.ipynb section: La chaîne, honnêtement : sous-section de l'ancienne Conclusion, renommée et fusionnée dans « À retenir » ; ses trois affirmations (forme abstraite #4048, hStar borne inférieure, réalisabilité restée abstraite) y sont reprises ; aucun contenu pédagogique perdu

Sous-grain de l'EPIC #19297 (finition de série), tranche Search/Part1-Foundations.

Ce que fait la PR

Search-03e-AStar-Optimality terminait par un ## Conclusion — une variante reconnue par check_series_finish (classe « à renommer ») — et n'avait ni bloc « Vérifiez votre compréhension » ni « Pour aller plus loin ». La cellule markdown finale est restructurée en trois blocs canoniques :

• ## À retenir : 4 points (modèle WeightedGraph/pathCost, prédicats Admissible/Consistent avec le pont Dijkstra, théorème phare admissible_le_suffix_cost, télescopage consistent_implies_path_bound/consistent_implies_f_monotone), suivis de la limite honnête conservée dans son sens : « A* renvoie un chemin optimal » n'est pas un théorème du lake (file de priorité non modélisée, Search-3 : le « théorème » admissible ⇒ optimal (c38/c39) est réfuté par l'implémentation du notebook lui-même — sa cellule 15 énonce pourtant la bonne condition #14824), le lake prouve la forme abstraite ([Lean][Search] Créer astar_lean — A* : admissibilité ⇒ optimalité #4048).
• ## Vérifiez votre compréhension : 4 questions tirées du contenu réel du carnet (lues avant rédaction), réponses repliées en <details>.
• ## Pour aller plus loin : Hart/Nilsson/Raphael (1968), Russell & Norvig §3.5, le lake search_lean, les lakes [EPIC] Roadmap Lean — nouveaux lakes à créer par série (1 théorème-phare/série, modèle Gittins) #4038 et leurs compagnons Lean-N — références déjà présentes, remises sous le titre canonique.

La queue de navigation (**Navigation** + paragraphe « Le pont ») est préservée byte-identique.

Vérification

• python scripts/notebook_tools/check_series_finish.py --series Search : 10 -> 11 carnets finis sur 165 ; Search-03e sort de la liste des carnets manquants.
• nbformat.validate OK ; 24 cellules avant et après ; diff cellule par cellule = seule la cellule 23 diffère.
• Aucune cellule de code touchée, aucun output re-sérialisé, metadata.papermill présent avant et après (C.2/C.3 : markdown seul, pas de ré-exécution due).
• Chaîne de navigation intacte (organe nav-chain : **Navigation** présent).
• detect_notebook_plan_loss.py : 3 sections sur 4 absorbées par la mesure de substance ; la quatrième (« La chaîne, honnêtement ») est déclarée ci-dessus en tête de body, avec sa raison.
• Relance du gate plan-loss (05/11) : le rouge du 03/11 20:03 datait d'avant le marqueur ; un gh run rerun rejoue le payload d'origine (body sans marqueur, cf PLAN_LOSS_PR_BODY dans le log) et re-échoue pour cette seule raison — cette édition edited fournit au gate le body courant, celui qui porte le marqueur.

Hors scope

Les carnets voisins restent pour les tranches suivantes : Search-04 (paire), 05b, 07, 09 sont libres ; 02b, 03c, 03d, 03f, 05, 06 sont sous PR ouverte et n'ont pas été touchés.

See #19297

🤖 Generated with Claude Code

[github-actions]

prev: genre mot-clé fermant (#10093) — LEVÉ (2026-11-05T01:00:50Z).

aucun genre mots-clé fermant dans le body ni les commits ; prev: accepté(s) : #24179

Run vert du garde : ce commentaire bloquant est obsolète. Réécrit en place (#15372) plutôt que laissé affiché faux — le marqueur reste porté pour le prochain upsert. Historique : runs Always-on guards de la PR.

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 11
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[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]

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]

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-11-03) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=2 genre=4 cap=2)
• 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=2 genre=4 cap=2)
• 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.

[clusterManager-Myia]

[Hermes]
VERDICT: APPROVE — toutes les affirmations du body sont reproductibles, exécutées.

Vérifié par exécution du head dde81a76

check_series_finish.py --series Search rejoué sur les deux rives (worktree sparse, fetch pull/24503/head) :

• base (origin/main) : carnet_finis = 10 / 165, et Search-03e est dans carnets_manquants avec missing: ['a_retenir','verifiez','aller_plus_loin'].
• head (pr24503) : carnet_finis = 11 / 165, et Search-03e disparaît de la liste (154 manquants contre 155).
  Le 10 → 11 du body et la sortie de Search-03e de la liste sont donc exacts, mesurés, pas recopiés.

Structure : 24 cellules avant et après, nbformat.validate OK, diff cellule à cellule = seule la cellule 23 (markdown) diffère. 11 cellules code, execution_count [1..11] identique, sources de code byte-identiques, outputs byte-identiques (comparaison JSON triée) — donc aucune ré-exécution due, et metadata.papermill présent avant et après (input_path/output_path inchangés).

Plan-loss : detect_notebook_plan_loss --base origin/main --check rend bien 4 findings sur la cellule 23 — 3 SUBSTANCE_FOUND_TOKEN_MATCH (Conclusion, Ce qui est prouvé, Où aller ensuite) et 1 LOST_SECTION: La chaîne, honnêtement. C'est exactement la section déclarée en tête de body, avec sa raison. La déclaration est donc conforme à la mesure, pas approximative.

Navigation : **Navigation** + le paragraphe **Le pont** sont byte-identiques base ↔ head (comparé sur la chaîne exacte à partir de **Navigation**) : le body le revendique et c'est vrai.

Les 4 réponses de « Vérifiez votre compréhension » tiennent contre les sources Lean

J'ai lu les .lean du lake plutôt que de juger la prose sur elle-même :

• Q1 → admissible_le_suffix_cost existe bien (Astar/Optimality.lean l.80) et son propre docstring dit « la borne en f en chaque nœud », exactement la formulation de la réponse. La limite « ne prouve pas qu'A* renvoie un chemin optimal » est aussi dans le docstring (**Portée — ce que ce théorème ne dit pas.**), avec #14824 cité : la réponse ne fait que répéter la source.
• Q2 → zero_admissible existe (Heuristic.lean l.71) et sa preuve est fun _ => zero_le — donc « parce que 0 ≤ hStar n » décrit littéralement le terme de preuve. Le pont Dijkstra est celui que la source nomme.
• Q3 → consistent_implies_path_bound (Consistency.lean l.55) et consistent_implies_f_monotone (l.123) existent tous deux ; la réponse les distingue correctement, et la « non-ré-expansion » est bien la lecture du docstring de f_monotone (« aucun nœud n'est jamais ré-expansé »).
• Q4 → réponse « non, choix assumé, file de priorité non modélisée (#14824) » : conforme au docstring de admissible_le_suffix_cost.

Aucune des quatre réponses n'énonce un lemme qui n'existe pas, et aucune ne transforme une borne en théorème d'algorithme — c'est précisément l'erreur que ce carnet est fait pour éviter.

Deux remarques de forme, sans conséquence

La réponse 1 écrit « borné par le coût d'un chemin optimal passant par le nœud » ; le lemme borne par pathCost (p.drop i) pour un p donné allant au but — « chemin optimal » est une lecture plus forte que l'énoncé. La phrase reste défendable parce que hStar est la borne inférieure du vrai coût restant, donc l'inégalité vaut a fortiori pour le chemin optimal, mais le lemme lui-même ne quantifie pas sur l'optimalité. Comme le carnet insiste ailleurs sur « la forme abstraite, pas la garantie », un mot de moins ici serait plus cohérent avec le reste.

Le compteur de la ligne 3.9b-style « 4 points / 4 questions » est cohérent (4 et 4). ## À retenir en contient 5 puces et non 4 comme annoncé dans le body (« 4 points ») — le contenu réel est meilleur que le décompte, c'est le décompte qui est en retard d'une puce (la cinquième, « La limite, dite franchement », est celle qui porte la nuance). Cosmétique.

Périmètre

Je n'ai pas rejoué le lake Lean (pas de toolchain lake sur ce siège) : je vérifie l'existence et l'énoncé des lemmes cités dans les sources committées, pas leur compilation. Rien dans le diff ne touche de .lean, donc ce n'est pas un risque introduit ici.

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Verdict calcule ce tour (cle 64fc422429f2bf98) — aucune entree de cache ne correspondait.

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.7s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.6s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.3s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.9s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.2s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.6s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	61.8s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.3s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	16.9s

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