Skip to content

docs(lean,#17357): Lean-33 -- 2 constats d'audit corriges (prose seule) #20156

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 1 commit into from
Oct 11, 2026
Merged

docs(lean,#17357): Lean-33 -- 2 constats d'audit corriges (prose seule) #20156

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 15 additions & 9 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-33-Distribution-Spaces.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -298,8 +298,9 @@
"`k` indexe l'ordre de décroissance (`‖x‖^k`) et `n` l'ordre de dérivation\n",
"(`iteratedFDeriv ℝ n`). Un seul objet mesure donc les deux moitiés du contrat.\n",
"\n",
"Les quatre `#check` suivants sont les énoncés **ajoutés par le module** : la décroissance\n",
"brute avec une constante strictement positive, la seminorme comme majorant, la seminorme\n",
"Le module déclare **dix** théorèmes. Les quatre `#check` suivants en échantillonnent\n",
"quatre : la décroissance brute avec une constante strictement positive, la seminorme\n",
"comme majorant, la seminorme\n",
"comme *plus petit* majorant, et la décroissance polynômiale effective qui se déduit de\n",
"la seminorme. Aucun n'est déclaré `sorry` — ce sont des théorèmes clos.\n"
]
Expand Down Expand Up @@ -990,7 +991,7 @@
" légitimes, mais qui doivent être **nommés** pour être vus.\n",
"\n",
"Le module `Calibration.Distribution` annonce « aucun `sorry` ». La cellule suivante le\n",
"vérifie sur ses théorèmes publics — et la seule autorité est le compilateur.\n"
"vérifie sur **quatre de ses dix** théorèmes publics — et la seule autorité est le compilateur.\n"
]
},
{
Expand Down Expand Up @@ -1137,8 +1138,9 @@
"source": [
"### Lecture du résultat\n",
"\n",
"Aucun des quatre théorèmes ne consomme `sorryAx` ni `native_decide.*` : ce sont des\n",
"preuves réelles, pas des preuves vidées. C'est la vérification d'intégrité que la règle de\n",
"Aucun des quatre théorèmes **passés à `#print axioms` ci-dessus** ne consomme\n",
"`sorryAx` ni `native_decide.*` : ce sont des preuves réelles, pas des preuves vidées.\n",
"C'est la vérification d'intégrité que la règle de\n",
"revue Lean du dépôt exige (`count_code_sorry.py` compte les `sorry` du *code* ;\n",
"`#print axioms` compte ceux qui *subsistent transitivement*).\n",
"\n",
Expand Down Expand Up @@ -1688,10 +1690,14 @@
"échantillonnage sur grille finie ne prouve rien. Le seul juge du champ `decay'` reste une\n",
"preuve, et c'est ce que le module fournit.\n",
"\n",
"**Ce que la calibration vérifie.** Les théorèmes du module sont **clos** — `#print axioms`\n",
"de la section 5 ne montre ni `sorryAx` ni `native_decide.*`. Ce qui reste\n",
"(`propext`, `Classical.choice`, `Quot.sound`) est le socle fondationnel standard de\n",
"l'analyse réelle dans Lean 4.\n",
"**Ce que la calibration vérifie.** Les **quatre** théorèmes passés à `#print axioms`\n",
"en section 5 sont **clos** — la sortie ne montre ni `sorryAx` ni `native_decide.*`.\n",
"Ce qui reste (`propext`, `Classical.choice`, `Quot.sound`) est le socle fondationnel\n",
"standard de l'analyse réelle dans Lean 4. Les six autres théorèmes publics du module ne\n",
"passent pas par `#print axioms` ici : c'est la **source** que vérifie\n",
"`count_code_sorry.py` (`distinct_code_sorry = 0` sur le lake), et c'est la sortie de\n",
"`#print axioms` qui établit l'absence de `sorryAx` transitif — sur les quatre théorèmes\n",
"montrés.\n",
"\n",
"### Repères\n",
"\n",
Expand Down
Loading