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..b1bd30a530 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,11 +525,11 @@ "\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 cités dans ce notebook** : 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_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`.\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", - "Pour une **revue complète** du triplet BORNE/TÉMOIN/CONCENTRATION sur le lake courant, suivre les **Voir aussi** internes de chaque sibling.\n" + "Pour une **revue complète** du triplet BORNE/TÉMOIN/CONCENTRATION sur le lake courant, suivre les **Voir aussi** internes de chaque sibling." ] } ],