fix(pedagogy,#17570): ICT tranche — re-pointer consommateurs vers evolveHashlifeFastAtN_correct_uncond

[jsboige]

Résumé

Tranche ICT de l'issue #17570 (consommateurs) : re-pointer la garantie de
correction citée dans ICT-Life-SubstratCertifie.ipynb et ict/life.py
depuis hashlife_correct (vacuously true dans le régime du saut) vers
evolveHashlifeFastAtN_correct_uncond (non-vacuous, sans hypothèse).

Vérifications before-fix (Tell c.974 strict ★★★ + Tell c.1156 ★★ strict)

Lecture critique first-hand du contenu réel avant patch :

1. Lean source first-hand (conway_lean/Conway/Life/HashlifeCorrectness.lean) :

   • L. 6373 : theorem hashlife_correct (n : Nat) (g : Grid) (h : BoxAssezGrand g n) : — confirmé
   • L. 6382 : p5_large_n_hyps_unsat cité dans la docstring — confirmé
   • L. 6384 : boxAssezGrand_nonempty_le_two cité — confirmé
   • L. 7202-7204 : theorem evolveHashlifeFastAtN_correct_uncond (n : Nat) (g : Grid) : evolveHashlifeFastAtN n g = evolve n g := evolveHashlifeFastAtN_correct one_jumpAt_correct n g — confirmé
   • L. 7181 : theorem one_jumpAt_correct : OneJumpAtCorrect := by — confirmé
   • Docstring historique hashlife_correct (l. 6369-6372) mise à jour par commit eacb29b98c 2026-09-24 (fix fix(ict,lean): ICT cite hashlife_correct comme garantie pleine — vide dans le régime du saut ; re-pointer vers evolveHashlifeFastAtN_correct_uncond #17570 dans le lake lui-même)

2. Git log first-hand : le théorème evolveHashlifeFastAtN_correct_uncond est livré par PR feat(lean,#11161): grain 3 complet — OneJumpAtCorrect theoreme + capstone evolveHashlifeFastAtN_correct_uncond #11781 (commit c5df96d5b0 2026-08-19, feat [Lean][GOL] Recadrage Gosper : prouver evolveHashlifeFastAtN inconditionnel (étape 2, #6724) — la capture devient corollaire #11161 grain 3), PAS par une autre PR. Une première rédaction citait #17644 — corrigée après vérification git log.

3. Notebook first-hand (ict_cells_full.txt exporté) : 9 cellules markdown contiennent le wording à corriger (cell 0 intro, cell 18 tableau + phrase « seul moteur prouvé », cell 19 section 5 H1 + théorème + calibration, cell 21 conclusion « garantie complète », cell 22 section 6 « branche Hashlife couverte », cell 27 synthèse « garantie de correction »). Toutes les chaînes OLD ont été trouvées verbatim.

4. ict/life.py first-hand (l. 15-34) : le bloc docstring **Pont preuve <-> mesure** est un paragraphe multiligne — confirmé l. 22 contient du theoreme \`hashlife_correct`` formalise en Lean dans la track ``conway_lean```. Patch par remplacement du bloc complet (15 lignes → 26 lignes).

Modifications

Fichier	Type	Cellules / Lignes	Δ
ICT-Life-SubstratCertifie.ipynb	markdown	cell 0, 18 (×2), 19 (×3), 21, 22, 27	+9/-9 cellules (toutes markdown, aucune code touchée)
ict/life.py	docstring	bloc l. 20-34 (15 lignes → 26 lignes)	+15/-4 lignes

Aucune cellule code modifiée : 11/11 cellules code conservent leur execution_count réel et leurs outputs intacts. C.2 ne déclenche pas de ré-exécution obligatoire (validation first-hand post-fix : nbformat.validate(nb) OK, 11/11 exec_count, 16 outputs préservés).

Acceptance #17570 (tranche ICT consommateurs)

• Notebook ICT-Life pointe vers evolveHashlifeFastAtN_correct_uncond (5 mentions cell 0/18/19/21/22/27)
• Notebook nomme la vacuité de hashlife_correct (cell 0, 19, 21, 22, 27)
• ict/life.py docstring pointe vers evolveHashlifeFastAtN_correct_uncond ET nomme la vacuité de hashlife_correct
• Toutes les références PR/commit sont first-hand vérifiées (PR feat(lean,#11161): grain 3 complet — OneJumpAtCorrect theoreme + capstone evolveHashlifeFastAtN_correct_uncond #11781, commit c5df96d5b0 2026-08-19 ; docstring update commit eacb29b98c 2026-09-24)
• Aucun changement de code Lean (docstring lake déjà mergée par commit eacb29b98c)
• Aucun changement de cellule code du notebook (C.2 préservation)

Hors périmètre (rappel)

• Docstring hashlife_correct côté Lean : déjà mergée par commit eacb29b98c (fix fix(ict,lean): ICT cite hashlife_correct comme garantie pleine — vide dans le régime du saut ; re-pointer vers evolveHashlifeFastAtN_correct_uncond #17570 lake tranche).
• Tranche Search-02c / ConnectFour : lane tierce myia-po-2027:CoursIA-2 (PR fix(search,#17550): sauts de ligne doublés — Search-02c + App-14 (tables GFM réparées, re-exec .NET) #17577, OPEN).
• Argument_Analysis_Multi_Backend_Routing.ipynb : défaut différent, hors scope.
• Lean-6-Mathlib-Essentials.ipynb : fix(lean,#17066): Lean-6 Mathlib Essentials — réparer la dégradation #16862 REPAIR-7/8 (sauts de ligne doublés, accents) #17110, lane tierce, hors scope.

Tell c.770 v3 strict fondateur (leçon durable consignée)

Première rédaction de cette PR citait PR #17644 pour le théorème evolveHashlifeFastAtN_correct_uncond — vérification git log first-hand a montré que ce PR n'existe pas. Le bon numéro est #11781 (commit c5df96d5b0 2026-08-19). Patch corrigé et ré-appliqué sur fichiers remis à l'état HEAD avant le second passage.

Tell c.974 strict ★★★ fondateur : ne JAMAIS citer un numéro de PR sans vérification git log. Leçon ajoutée au journal de délégation.

Grain

Grain: MED/notebook-python — lane myia-po-2026:CoursIA-2 — prev: MED/notebook-python #17632

🤖 Generated with Claude Code

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

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	8.8s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	6.5s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	7.6s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	7.1s
Search-01-StateSpace.ipynb	✅ SUCCESS	8.7s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	4.3s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	47.9s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	10.3s

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]

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)

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 17688
head: 9493058
complete: true
body: read
comments-reviewed: 4
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: ada7a6934f4a848c673ae827382e19354164a3a5bc2f3abac5b7aa925ee07dcd
diff-files: 2
diff-additions: 44
diff-deletions: 24
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]