diff --git a/MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8c-Borne-Temoin-Concentration.ipynb b/MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8c-Borne-Temoin-Concentration.ipynb index dc1ee1b499..4a36794a39 100644 --- a/MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8c-Borne-Temoin-Concentration.ipynb +++ b/MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.8c-Borne-Temoin-Concentration.ipynb @@ -24,7 +24,7 @@ "\n", "**Compagnon formel** : `MyIA.AI.Notebooks/ML/learning_theory_lean/`\n", "\n", - "---\n", + "***\n", "\n", "## Concept\n", "\n", @@ -525,7 +525,7 @@ "\n", "Les vérifications mécaniques étaient historiquement dans ce notebook : existence des théorèmes cités et `sorry = 0` dans le lake. Elles sont désormais portées par les instruments suivants :\n", "\n", - "- **Existence des théorèmes** : vérifiée par les `#check` explicites dans [2.8d](2.8d-Lean-Novikoff-Convergence.ipynb) (`PerceptronRun.novikoff_mistake_bound`, `tightnessRun_saturates`, ...) et [2.8b](2.8b-Theorie-PAC-Lean.ipynb) (`hoeffding_concentration`, `pac_finite_class_bound`, ...).\n", + "- **Existence des théorèmes** : vérifiée par les `#check` explicites dans [2.8d](2.8d-Lean-Novikoff-Convergence.ipynb) (`PerceptronRun.novikoff_mistake_bound`, `tightnessRun_saturates`, ...) et [2.8b](2.8b-Theorie-PAC-Lean.ipynb) (`PacLearning.uniform_concentration`, `PacLearning.sampleWeight_nonneg`, `PacLearning.sampleWeight_sum_one`, ...). Les théorèmes `hoeffding_concentration` et `pac_finite_class_bound` existent dans le lake (PacLearning/Hoeffding.lean:318, PacLearning/PacFiniteBound.lean:377) mais ne sont **pas** interrogés par les `#check` du notebook 2.8b — la note antérieure les attribuait par erreur (#13862). Vérification native : `#print axioms PacLearning.sampleWeight_sum_one` + `#print axioms PacLearning.uniform_concentration`.\n", "- **Zéro `sorry` réel dans le lake** : porté par l'organe `python scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`), mesuré en CI par le job `proof-integrity`. **Pas de `grep -c sorry`** : il sur-compte la prose (docstrings, commentaires).\n", "- **Pas de `native_decide` / `sorryAx` dans le chemin des théorèmes cités** : porté par le job CI `lean-axiom.yml` (catégorie `forbidden`, pas seulement `sorry`).\n", "\n",