2.8c: la note de substitution attribue a 2.8b deux #check qui n'y sont pas (hoeffding_concentration, pac_finite_class_bound)

Découvert en levant la réserve du merge-gate de #13717 (mesuré firsthand sur la tête de PR, 2026-08-31).

Le défaut

2.8c porte une note de substitution (cellule markdown « Comment vérifier sur main ? ») qui remplace deux cellules Python retirées — celle qui vérifiait l'existence des théorèmes cités, et celle qui comptait les sorry. La note dit :

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, ...).

La moitié 2.8d est vraie (mesurée : #check PerceptronRun.novikoff_mistake_bound cellule [1] ec=1, #check witnessPts/tightnessRun_saturates cellule [8] ec=4, sorties réelles).

La moitié 2.8b est fausse pour les deux noms cités. Inventaire exhaustif des directives Lean exécutées dans 2.8b à la tête de #13717 :

[3]  ec=1  #check @PacLearning.{Distribution, Hypothesis, trueError, sampleProb,
                              sampleWeight, uniform_concentration}
[23] ec=10 #check @PacLearning.{sampleWeight_nonneg, sampleWeight_sum_one}
           #print axioms PacLearning.sampleWeight_sum_one
           #print axioms PacLearning.uniform_concentration

hoeffding_concentration n'apparaît dans 2.8b que dans une cellule markdown ; pac_finite_class_bound dans deux markdown et un commentaire Lean (-- Section 8 : la complexite d'echantillon de pac_finite_class_bound) au-dessus d'une cellule qui #eval une ré-implémentation sampleComplexity, jamais le théorème.

Les deux théorèmes existent bien dans le lake — ce n'est pas une citation fantôme :

PacLearning/Hoeffding.lean:318 — theorem hoeffding_concentration
PacLearning/PacFiniteBound.lean:377 — theorem pac_finite_class_bound

Ce qui manque est le chaînon exécuté entre la prose et eux. C'est la classe identity-check-does-not-verify-assertion : la référence existe, l'affirmation portée sur elle ne tient pas.

Pourquoi ce n'était pas bloquant pour #13717

La réserve que #13717 devait lever portait sur les cellules execution_count: null + outputs: [], et elle est levée (0 cellule vide sur les 3 notebooks au head, Voie 1 appliquée en 132bf5261). Le présent défaut a été découvert en vérifiant cette levée ; le retenir aurait déplacé les poteaux après coup. Il est tracé ici avant le merge, conformément à CLAUDE.md §B.0 (une issue ouverte et nommée AVANT le merge est l'une des trois voies de levée).

Acceptance — deux remèdes, le second préféré

(a) minimum — corriger la note de 2.8c pour nommer ce que 2.8b vérifie réellement : PacLearning.uniform_concentration (#check + #print axioms) et PacLearning.sampleWeight_sum_one. Prose seule, pas de ré-exécution.

(b) préféré — ajouter dans 2.8b #check @PacLearning.hoeffding_concentration et #check @PacLearning.pac_finite_class_bound (import à ajuster : PacLearning.Hoeffding, PacLearning.PacFiniteBound), ré-exécuter sous kernel lean4-wsl, committer avec les sorties réelles — puis la note de 2.8c devient vraie sans la réécrire. C'est le remède qui rétablit la substance perdue plutôt que d'ajuster la prose à la perte.

Si (b) est retenu, ajouter #print axioms sur les deux : c'est l'instrument qui couvre la classe forbidden entière (sorryAx, native_decide), pas seulement l'existence — celui que 2.8b applique déjà à uniform_concentration.

Preuve exigée : sortie de cellule réelle citée dans le body (pas « ré-exécuté OK »), et pour (b) execution_count != null sur les cellules touchées.

Contexte : EPIC #13504.

[CLAIMED] lane myia-po-2024:CoursIA-2 -- REPAIR 2.8c note de substitution: ajouter #check hoeffding_concentration + pac_finite_class_bound dans 2.8b sous kernel lean4-wsl + ré-exécuter + committer sorties réelles (acceptance b issue #13862)

(check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative. Release with [RELEASED] when your PR lands.)

[CLAIMED] lane myia-po-2024:CoursIA-2 -- [CLAIMED] REPAIR 2.8c note de substitution: ajouter #check hoeffding_concentration + pac_finite_class_bound dans 2.8b sous kernel lean4-wsl + ré-exécuter + committer sorties réelles (acceptance b issue #13862, ouvert par ai-01 post-#13717 merge)

(check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative. Release with [RELEASED] when your PR lands.)

[CLAIMED] lane myia-po-2024:CoursIA-2 -- paths: MyIA.AI.Notebooks/ML/02_Apprentissage-Statistique/2.8b-Theorie-PAC-Lean.ipynb -- acceptance (b) préférée par ai-01 : ajouter #check @PacLearning.hoeffding_concentration et #check @PacLearning.pac_finite_class_bound + #print axioms sur les deux + ré-exécution kernel lean4-wsl + committer sorties réelles. Cible : rendre vraie la note de 2.8c sans réécrire la prose.