fix(2.8c,#13862): corrige la note de substitution -- hoeffding/pac_finite_class_bound cites mais non #check

[jsboige]

Summary

Le cellule markdown "Comment vérifier sur main ?" (cellule 14) du notebook
2.8c-Borne-Temoin-Concentration.ipynb nommait deux théorèmes Lean
(hoeffding_concentration dans Hoeffding.lean:318, pac_finite_class_bound dans
PacFiniteBound.lean:377) comme vérifiés par les #check de 2.8b. L'inventaire
exhaustif des directives Lean exécutées dans 2.8b à la tête de #13717 montre
aucun #check @PacLearning.hoeffding_concentration ni
#check @PacLearning.pac_finite_class_bound. Les deux théorèmes existent dans le
lake (cf. grep -n "theorem hoeffding_concentration\|theorem pac_finite_class_bound"
sur les fichiers .lean), mais ne sont pas interrogés nativement par les cellules
actuelles de 2.8b.

C'est la classe identity-check-does-not-verify-assertion : la référence existe,
l'affirmation portée sur elle ne tient pas (issue #13862 verbatim).

Voie (a) retenue — correction markdown

L'issue #13862 proposait deux remèdes :

Voie	Definition	Statut
(a) minimum	Corriger la note de 2.8c pour nommer ce que 2.8b vérifie réellement	Cette PR
(b) préférée	Ajouter #check @PacLearning.hoeffding_concentration + #check @PacLearning.pac_finite_class_bound + #print axioms dans 2.8b, ré-exécuter sous kernel lean4-wsl, committer avec les sorties réelles	Follow-up séparé

Cette PR applique la voie (a) : la note de 2.8c nomme maintenant explicitement
ce que 2.8b vérifie réellement (PacLearning.uniform_concentration,
PacLearning.sampleWeight_sum_one, PacLearning.sampleWeight_nonneg — les 3
modules noirs de Sample.lean et UniformConcentration.lean interrogés nativement
par #check + #print axioms en Section 10 de 2.8b), et ajoute une note
explicative (Note (issue #13862)) qui distingue "existence dans le lake" et
"interrogation par #check".

Pourquoi voie (a) plutôt que voie (b) dans cette PR

La voie (b) requiert un environnement learning_theory_lean compilé localement
(lake build au moins sur les 3 modules PacLearning.UniformConcentration,
PacLearning.Hoeffding, PacLearning.PacFiniteBound). Sur la machine worker
myia-po-2026, le lake n'est pas compilé (pas de .lake/build/ dans le
worktree ; vérifié : find /c/dev/CoursIA-cycle-33 -name "*.lake" -type d retourne
vide ; find /c/dev/CoursIA-cycle-33 -name "PacLearning.olean" retourne vide).

Test direct via nbclient + kernel lean4-wsl sur la cellule 3 (qui marchait à
l'origine) :

import PacLearning.UniformConcentration
#check @PacLearning.uniform_concentration
        ─────────────────────────────────▶ ❌ Unknown identifier `PacLearning.uniform_concentration`

Le kernel lean4-wsl sur worktree frais ne charge pas PacLearning.* — il pointe
vers le mauvais Lake project root ou le cache Lake partagé est dans un état
incohérent. La voie (b) doit donc être reprise par ai-01 ou po-2023 (machines
où learning_theory_lean a été compilé au moins une fois) — voir issue #13862
acceptance pour le plan exact.

Modification

1 fichier, markdown-only (exception C.2 : aucune cellule code touchée, 15/15
execution_count intacts, outputs inchangés — vérifié par git diff + par le
validateur pre-commit H.3 + par #13326 + par validate_pr_notebooks.py).

- "- **Existence des théorèmes** : vérifiée par les `#check` explicites dans [2.8d](...) (`PerceptronRun.novikoff_mistake_bound`, `tightnessRun_saturates`, ...) et [2.8b](...) (`hoeffding_concentration`, `pac_finite_class_bound`, ...)."
+ "- **Existence des théorèmes cités dans ce notebook** : vérifiée par les `#check` explicites dans [2.8d](...) (`PerceptronRun.novikoff_mistake_bound`, `tightnessRun_saturates`, ...) et [2.8b](...) (`PacLearning.uniform_concentration`, `PacLearning.sampleWeight_sum_one`, `PacLearning.sampleWeight_nonneg`). Ces trois modules sont interrogés nativement par `#check` (signature) + `#print axioms` (certificat) — voir Section 10 de 2.8b. **Note (issue #13862)** : les théorèmes `hoeffding_concentration` (Hoeffding.lean) et `pac_finite_class_bound` (PacFiniteBound.lean) **existent** dans le lake mais ne sont **pas interrogés** par les cellules actuelles de 2.8b ; ils sont atteints par les Sections 5 (Monte-Carlo sur `hoeffding_upper_tail`) et 8 (`#eval` d'une version jouable de `pac_finite_class_bound`) du même 2.8b, ce qui prouve la **disponibilité de la chaîne computationnelle** mais ne rend pas la signature native du théorème via `#check`."

Acceptance issue #13862

• Voie (a) choisie (correction de la note markdown), avec la raison écrite
  dans le body PR : la voie (b) requiert un lake compilé localement, pas
  disponible sur myia-po-2026 (worktree frais). Voie (b) documentée pour
  follow-up par ai-01/po-2023.
• Si (a) : la note nomme ce que 2.8b vérifie réellement
  (uniform_concentration, sampleWeight_sum_one, sampleWeight_nonneg) —
  vérifié firsthand par lecture de 2.8b (cellules 3 et 23 contiennent ces
  #check et #print axioms).
• Note explicative (issue 2.8c: la note de substitution attribue a 2.8b deux #check qui n'y sont pas (hoeffding_concentration, pac_finite_class_bound) #13862) ajoutée pour distinguer "existence dans
  le lake" (vrai pour les deux) et "interrogation par #check" (faux pour
  les deux dans 2.8b actuel).

Preuves firsthand (inventaire 2.8b à la tête de #13717)

$ grep -nE "^\s*#check|^\s*#print axioms" MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8b-Theorie-PAC-Lean.ipynb
#cell 3  (ec=1)  #check @PacLearning.{Distribution, Hypothesis, trueError, sampleProb, sampleWeight, uniform_concentration}
#cell 23 (ec=10) #check @PacLearning.{sampleWeight_nonneg, sampleWeight_sum_one}
                 #print axioms PacLearning.{sampleWeight_sum_one, uniform_concentration}
#cell 24 (ec=11) -- code numerique (no #check, only #eval tailBound)

Aucun #check sur hoeffding_concentration ni pac_finite_class_bound dans 2.8b.
Les deux théorèmes sont atteints mais pas vérifiés :

Théorème	Atteint via	Vérifié via #check ?
hoeffding_concentration (Hoeffding.lean:318)	Section 5 (cell 14, #eval Monte-Carlo sur hoeffding_upper_tail)	Non
pac_finite_class_bound (PacFiniteBound.lean:377)	Section 8 (cell 20, #eval sampleComplexity jouable)	Non
uniform_concentration (UniformConcentration.lean)	Section 10 (cell 3, #check + cell 23, #print axioms)	Oui
sampleWeight_sum_one (Sample.lean)	Section 10 (cell 23, #check + #print axioms)	Oui
sampleWeight_nonneg (Sample.lean)	Section 10 (cell 23, #check)	Oui

La note de 2.8c, après correction, reflète exactement ce tableau.

Pre-commit (10/10 hooks PASSED)

Secret scanner (gitleaks)..........................................Passed
Strip .NET probeAddresses banner from staged notebooks............Passed
Strip .NET 'Loading extensions from <NuGet cache>' leak...........Passed
Scrub absolute papermill input/output paths from staged notebooks.Passed
Auto-fix decorative '---' cell openers............................Passed
Block NEW oversized markdown-rendering defects (frontmatter).....Passed
Auto-fix source-list-missing-newlines defects in staged notebooks.Passed
H.3 — refuse un-executed notebooks (execution_count=null + empty).Passed
Refuse NEW text=True without encoding= (subprocess, cp1252)......Skipped (no .py files)
#13326 — refuse un-compilable cell source.........................Passed
validate_pr_notebooks.py: 5/5 cells passed (coursia-ml-training kernel)

Lien avec cycles precedents

• 2.8c: la note de substitution attribue a 2.8b deux #check qui n'y sont pas (hoeffding_concentration, pac_finite_class_bound) #13862 (cette PR) : voie (a), note de 2.8c corrigée.
• 2.8c: la note de substitution attribue a 2.8b deux #check qui n'y sont pas (hoeffding_concentration, pac_finite_class_bound) #13862 voie (b) : à reprendre par ai-01 ou po-2023 (lake compilé requis).
• fix(notebook,#13504): 2.8c carte transversale — Sections 1-3 absorbees par 2.8b/d #13717 : PR qui a ajouté la note de substitution fautive (cell 14 ajoutée
  lors du merge de 2.8c dans le trio 2.8b/2.8c/2.8d).
• [EPIC] DataScienceWithAgents : la zone la plus chaude du depot n'a aucune umbrella — parite expansion/consolidation #13504 : EPIC DSA, parent de la triade 2.8b/2.8c/2.8d.

Grain: LIGHT/lean - lane myia-po-2026:CoursIA - prev: tooling #13871 cycle 32.
paths: MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8c-Borne-Temoin-Concentration.ipynb

Closes #13862

🤖 Generated with Claude Code

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.4s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.4s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.2s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	5.2s
Search-1-StateSpace.ipynb	✅ SUCCESS	4.0s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.9s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	28.3s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.5s

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

[github-actions]

⚠️ Detector abstained (merge-base introuvable, shallow fetch or unanchored branch).

c.415 (#11873): scope = notebooks CHANGED in this PR, not the whole corpus.
See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 pathologie.

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 5
• 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]

Path-collision (organ #13359/#13615)

Cette PR #13893 (fix(2.8c,#13862): corrige la note de substitution -- hoeffding/pac_finite_class_bound cites mais non #check) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• fort -- fix(notebook,#13862): 2.8c 'Comment vérifier' cite les vrais #check de 2.8b #13942 partage : MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8c-Borne-Temoin-Concentration.ipynb (issues communes : 2.8c: la note de substitution attribue a 2.8b deux #check qui n'y sont pas (hoeffding_concentration, pac_finite_class_bound) #13862)

[jsboige]

Superseded by #13862 fix on main (commit dcb33bf, PR #13942). hoeffding/pac_finite_class_bound #check citation already corrected. Cycle 95 G-VAR recovery.