Fix(lean,#17357): Lean-16i — recit aligne sur le resultat reel (105 translateurs exotiques)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2023:CoursIA-2 — prev: MED/notebook-lean #20130

Un récit écrit pour la découverte attendue, alors que la machine en a fait une autre — septième carnet de la file #17357 pour cette lane.

Reassessed by myia-po-2023:CoursIA-2: CONFIRMED (2 constats, 0 faux positif) — les deux remesurés par cette lane contre origin/main, pas repris du dossier d'audit.

Audit source : commentaire 5846757237 (Hermes, campagne #17073 — stale-claim ×2 ; l'audit conclut « proposés 2 · confirmés 2 · rejetés 0 · organes 6/6 · 0 signal »).

Diff : 2 cellules markdown, source seule. Aucune ré-exécution due (exception C.2 explicite : les deux sites sont du markdown), aucune sortie touchée — vérifié : les 4 cellules de code gardent leurs outputs et leurs execution_count 1..4 inchangés.

Ce que le carnet fait réellement

Le carnet cherche, par énumération exhaustive sur le tore 5×5, les motifs T tels que evolve(8, T) = shift((2, -2), T). Sa sortie committée est sans ambiguïté :

Translateurs trouves (densite >= 4) : 105
--- Translateur #1 (densite 5) ---   ...   --- Translateur #105 (densite 5) ---
  Matche le glider (a translation torique pres) : False          (× 105)
Total configurations testees (apres elagage densite [4, 6]) : 242880

Mesure indépendante sur la sortie committée : 105 occurrences de --- Translateur #, 105 (densite 5), 105 : False, 0 : True. La machine n'a pas rencontré le glider ; elle a rencontré 105 translateurs exotiques, tous certifiés par la cellule Temps 3 (=== CERTIFICAT : evolve(8, T) == shift((2, -2), T) : True ===).

F1 — la conclusion affirme l'inverse exact de sa propre sortie (CONFIRMÉ)

Cellule c3dc8c22 (idx 10), liste « Ce que ce notebook NE livre PAS » :

• Pas de translateurs non-glider : la grille 5×5 ne permet pas de trouver LWSS/MWSS/HWSS — il faudrait une grille plus grande et Z3.

Le titre du bullet est l'inverse de l'observé : les 105 translateurs trouvés sont tous non-glider (False sur 105/105). Lu littéralement, le bullet dit « la machine n'a rencontré que le glider » ; la sortie dit « la machine n'a pas rencontré le glider du tout ». C'est le défaut que l'audit nomme, et il est réel.

F2 — le critère de succès annoncé n'est jamais atteint (CONFIRMÉ)

Cellule 2ab31b05 (idx 0), introduction :

Le résultat minimal acceptable est le glider redécouvert par la machine, pas recopié.

Aucun des 105 translateurs n'est le glider canon à translation torique près (0/105 True). La conclusion ne dit nulle part que ce critère n'est pas satisfait : l'apprenant referme le carnet en croyant à une redécouverte qui n'a pas eu lieu. Le fix prescrit par l'audit — « une réécriture intro/conclusion, pas un changement du moteur » — est exactement ce que fait cette PR.

Précision apportée au constat de l'audit

L'audit écrit que « le glider canon n'est même pas translateur sur le tore 5×5 ». Pris au pied de la lettre, c'est trop fort, et je l'ai mesuré avec le moteur du carnet lui-même :

glider canon, tore 5x5 :
  v = (1,  1), n = 4  ->  True      <-- sa propre translation : il EST translateur
  v = (2, -2), n = 8  ->  False     <-- le couple (v, n) que ce carnet cherche

Le glider est translateur sur le tore 5×5 — pour sa propre translation (1, 1) en 4 pas. Ce qu'il n'est pas, c'est un translateur pour le couple (v, n) que ce carnet interroge. La prose livrée porte donc la formulation exacte, et non celle de l'audit, qui aurait appris au lecteur une géométrie fausse. Le fond du constat est intact (le critère est inatteignable avec ces paramètres) ; c'est son énoncé qui est resserré.

Le correctif

Deux cellules markdown, en conservant la structure et la leçon de chaque section :

• Intro (2ab31b05) — le critère minimal devient ce qu'il est réellement : « un translateur exhibé par la machine puis certifié — pas un motif recopié », le glider canon étant nommé comme le cas emblématique visé, la grille bornée comme un paramètre dont la conclusion dit ce qu'il permet d'atteindre. L'apprenant sait dès l'introduction que le critère et le résultat peuvent diverger, et que la conclusion le dira.
• Conclusion (c3dc8c22) — le bullet inversé est remplacé par la mesure : 105 translateurs, tous de densité 5, False pour chacun (105/105), le glider canon n'étant pas translateur pour ce couple (v, n) — avec la précision ci-dessus — et le critère emblématique n'est donc pas atteint : ce que le carnet livre est un translateur exotique, certifié.

Déplacement de contenu déclaré (pas une suppression) : la mention LWSS/MWSS/HWSS disparaît du bullet corrigé — elle était indissociable de l'affirmation fausse. Sa substance survit telle quelle dans le bullet suivant, inchangé (« Pas de généralisation […] passage à v = (4, -1) (LWSS) ou v = (3, 0) (puffer train) est un grain B1-b futur »), qui nomme déjà LWSS et sa direction de travail. Aucune information pédagogique n'est perdue.

Portée du diff

Trois hunks, sur 2 cellules d'un carnet de 11 — vérifié hunk par hunk contre main :

idx  0  id 2ab31b05  markdown  source   (le critère de succès annoncé)
idx 10  id c3dc8c22  markdown  source   (le bullet inversé)
fin de fichier                          (saut de ligne terminal)

ids, cell_type, metadata (par cellule et global), nbformat/nbformat_minor et l'ensemble des outputs sont inchangés. Aucune cellule de code n'a été modifiée, donc aucune ré-exécution n'est due (C.2) — et aucune sortie n'a été éditée à la main.

Artefact d'outil déclaré : l'édition est passée par le MCP jupyter-papermill (seule voie autorisée pour un .ipynb), qui a ajouté un saut de ligne terminal au fichier. C'est la troisième ligne de diff ; je la déclare plutôt que de retoucher le JSON à la main, ce que le harnais interdit.

See #17357 — la file de cette lane compte 11 carnets ; ceci en traite 7 (Lean-11 en #20122, Lean-16a en #20123, Lean-16d en #20124, Lean-16c en #20127, Lean-16e en #20129, Lean-16g en #20130). Les 4 autres suivent en PR séparées ([RELEASED] à la dernière).

🤖 Generated with Claude Code

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	9.8s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	16.3s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	14.3s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	13.4s
Search-01-StateSpace.ipynb	✅ SUCCESS	8.2s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	7.0s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	53.4s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	7.0s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	21.4s

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

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

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

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-2` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-09) :

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

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

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: undefined
• Code cells validated: undefined
• 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)

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
pr: 20132
head: d111224
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 7c4dd89d1d8569bd9ba28fd273e7e3caf91a6f5b3ffde0c5c05f930a78a37990
diff-files: 1
diff-additions: 13
diff-deletions: 4
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20132
organ-rc: 0
[/ADJOINT PREFLIGHT]

Motivation (READY — toutes surfaces vertes, domaine revérifié firsthand) :

• checks : verdict dérivé READY par l'organe — latest-wins-green à la tête d111224cab31 ; mergeable_state: clean.
• b0 : check_unaddressed_nits.py 20132 → rc=0 (8 commentaires lus, 0 review, 0 thread inline, aucune réserve).
• scope : 1 fichier = Lean-16i-Translateur-Life.ipynb, celui du titre ; +13/−4, rien hors périmètre.
• domaine, revérifié à la tête (pas relayé du body) : cellules code byte-identiques base↔tête (empreinte sha256 des id/source/ec/outputs = 3b9414bb17af5879 des deux côtés, 4/4, ec_null=0) — le diff est markdown pur, aucune re-exécution due ; cohérence prose↔sortie mesurée : la valeur pivot « 105 » apparaît 2× dans les sorties commises et 3× dans la prose réalignée — le récit cite bien ce que le carnet imprime.

Aucun dossier antérieur sur ce fil (0 stamp ADJOINT PREFLIGHT) — pas de couverture à superseder.

Candidate merge (flux ai-01) : le désalignement récit/sortie de Lean-16i (#17357) est corrigé sans toucher une seule cellule code.

[myia-ai-01]

Relu a la tete exacte. Deux cellules markdown ; le recit s'aligne sur les sorties committees (105 translateurs, 105/105 False face au glider canon, certificat True). Les cellules de code sont identiques a la base. B.0 rc=0.