Skip to content

Reorg(lean,#19522): Discrepancy-02 annexe unique dans wrapper thematique #19577

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
jsboige merged 2 commits into from
Oct 7, 2026
Merged

Reorg(lean,#19522): Discrepancy-02 annexe unique dans wrapper thematique #19577

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9d1fbe8
Reorg(lean,#19522): Discrepancy-02 annexe unique dans wrapper thematique
jsboige Oct 6, 2026
a8386c2
Merge remote-tracking branch 'origin/main' into feature/19522-discrep…
jsboige Oct 7, 2026
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
115 changes: 67 additions & 48 deletions MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09e-Komlos-Lean.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2174,11 +2174,73 @@
"#check Discrepancy.KomlosBansalJiangWeak"
]
},
{
"cell_type": "markdown",
"id": "499ec9fe",
"metadata": {
"papermill": {
"duration": 0.002247,
"end_time": "2026-09-03T05:22:17.142906+00:00",
"exception": false,
"start_time": "2026-09-03T05:22:17.140659+00:00",
"status": "completed"
},
"tags": []
},
"source": [
"## 8. Ce que ce compagnon a rendu visible\n",
"\n",
"Avant ce notebook, le module `Discrepancy/Komlos.lean` était **noir** : aucune de ses trois\n",
"déclarations — `KomlosConjecture`, `BansalJiangLargeDegree`, `KomlosBansalJiangWeak` — n'était citée\n",
"par le moindre notebook du corpus (mesure `scan_lake_notebook_visibility.py`). Puis la section 6\n",
"a ouvert la moitié restante du lake : `Kernel`, `Partial`, `Progress`, `BeckFiala` (b1–b4) et\n",
"`ErdosSpencer` (p1a–p4) — dont les deux sommets **prouvés**, `beck_fiala_classic` et\n",
"`erdos_spencer_lb_explicit`, désormais chargés avec leur certificat d'axiomes.\n",
"\n",
"Ce compagnon l'exécute : les trois `Prop` rendues avec leurs signatures complètes, la condition\n",
"unitaire **décidée** sur des témoins pythagoriciens et hadamardiens, la discrépance optimale\n",
"**calculée par énumération exhaustive dans le noyau** (`1/5` puis `1`), les théorèmes P0 relus\n",
"avec leur témoin, et la machinerie prouvée interrogée boute par boute. Relié au corpus :\n",
"\n",
"- [Search-09c](../Part1-Foundations/Search-09c-CombinatorialDiscrepancy.ipynb) mesure les **mêmes objets en numérique**\n",
" (numpy, arrondi Beck–Fiala, oracle CP-SAT) — la discrépance exacte qu'il approche par solver,\n",
" ce compagnon l'énumère in-kernel sur des petits témoins, et sa borne `2k − 1` est maintenant\n",
" le théorème exécuté de la section 6 ;\n",
"- [Search-03c](../Part1-Foundations/Search-03c-LimitedDiscrepancySearch.ipynb) rappelle que « discrepancy » a aussi une\n",
" vie d'heuristique de parcours — sans rapport ;\n",
"- le lake [discrepancy_lean](../discrepancy_lean/README.md) garde ses conjectures en `Prop` nommée :\n",
" quand l'étage SDP existera en Mathlib, la preuve remplacera la déclaration sans changer\n",
" l'énoncé — et ce notebook montrera le basculement. L'annonce de septembre 2026 (résolution à\n",
" constante universelle, preprint non revu) ne change pas ce contrat : sa route exige un autre\n",
" étage absent de Mathlib, et les `Prop` attendent toujours une preuve formelle."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Annexes -- approfondissements optionnels\n",
"\n",
"Une annexe issue du chantier de visibilite des modules noirs\n",
"du lake Discrepancy (#11703) : la machinerie des moments de\n",
"l'inegalite d'Erdos-Spencer, deja rendue visible dans le\n",
"#11703 mais releguee en queue du carnet. Le regroupement\n",
"prevoit un chapitre dedie malgre une seule annexe, pour\n",
"conserver la coherence du nouveau format avec Lean-15c.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Annexe — ErdosSpencer/Moments : la machinerie des moments (#11703)\n",
"### Annexe A -- ErdosSpencer/Moments : la machinerie des moments (#11703)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### A.1 -- ErdosSpencer/Moments : la machinerie des moments\n",
"\n",
"Le scan de visibilite (`scan_lake_notebook_visibility.py`) comptait\n",
"`ErdosSpencer/Moments.lean` comme le **dernier module noir** du lake\n",
Expand All @@ -2194,7 +2256,7 @@
"\n",
"L'import vit seul dans sa cellule : le REPL lean4 ne commit reellement\n",
"l'environnement que si la commande ne contient que des imports (convention du\n",
"kernel, cf la cellule d'import d'ouverture)."
"kernel, cf la cellule d'import d'ouverture).\n"
]
},
{
Expand Down Expand Up @@ -2443,9 +2505,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"### Lecture de la sortie — le triptyque des moments, et un lake sans module noir\n",
"\n",
"Les six `#check` affichent les signatures completes. Le triptyque des moments\n",
"**Lecture de la sortie** -- Les six `#check` affichent les signatures completes. Le triptyque des moments\n",
"se lit comme un escalier : moment 1 nul (pas de biais), moment 2 = energie\n",
"(variance), moment 4 = le terme qui discrimine — son controle sous\n",
"`IsColoring c` est ce qui rend la queue de `rademacherSum c ·` assez fine pour\n",
Expand All @@ -2456,48 +2516,7 @@
"\n",
"Avec ce module expose, le lake `discrepancy_lean` n'a **plus aucun module\n",
"noir** : les deux jambees de la borne — Komlos deterministe, Erdos-Spencer\n",
"probabiliste — sont desormais lisibles depuis ce compagnon."
]
},
{
"cell_type": "markdown",
"id": "499ec9fe",
"metadata": {
"papermill": {
"duration": 0.002247,
"end_time": "2026-09-03T05:22:17.142906+00:00",
"exception": false,
"start_time": "2026-09-03T05:22:17.140659+00:00",
"status": "completed"
},
"tags": []
},
"source": [
"## 8. Ce que ce compagnon a rendu visible\n",
"\n",
"Avant ce notebook, le module `Discrepancy/Komlos.lean` était **noir** : aucune de ses trois\n",
"déclarations — `KomlosConjecture`, `BansalJiangLargeDegree`, `KomlosBansalJiangWeak` — n'était citée\n",
"par le moindre notebook du corpus (mesure `scan_lake_notebook_visibility.py`). Puis la section 6\n",
"a ouvert la moitié restante du lake : `Kernel`, `Partial`, `Progress`, `BeckFiala` (b1–b4) et\n",
"`ErdosSpencer` (p1a–p4) — dont les deux sommets **prouvés**, `beck_fiala_classic` et\n",
"`erdos_spencer_lb_explicit`, désormais chargés avec leur certificat d'axiomes.\n",
"\n",
"Ce compagnon l'exécute : les trois `Prop` rendues avec leurs signatures complètes, la condition\n",
"unitaire **décidée** sur des témoins pythagoriciens et hadamardiens, la discrépance optimale\n",
"**calculée par énumération exhaustive dans le noyau** (`1/5` puis `1`), les théorèmes P0 relus\n",
"avec leur témoin, et la machinerie prouvée interrogée boute par boute. Relié au corpus :\n",
"\n",
"- [Search-09c](../Part1-Foundations/Search-09c-CombinatorialDiscrepancy.ipynb) mesure les **mêmes objets en numérique**\n",
" (numpy, arrondi Beck–Fiala, oracle CP-SAT) — la discrépance exacte qu'il approche par solver,\n",
" ce compagnon l'énumère in-kernel sur des petits témoins, et sa borne `2k − 1` est maintenant\n",
" le théorème exécuté de la section 6 ;\n",
"- [Search-03c](../Part1-Foundations/Search-03c-LimitedDiscrepancySearch.ipynb) rappelle que « discrepancy » a aussi une\n",
" vie d'heuristique de parcours — sans rapport ;\n",
"- le lake [discrepancy_lean](../discrepancy_lean/README.md) garde ses conjectures en `Prop` nommée :\n",
" quand l'étage SDP existera en Mathlib, la preuve remplacera la déclaration sans changer\n",
" l'énoncé — et ce notebook montrera le basculement. L'annonce de septembre 2026 (résolution à\n",
" constante universelle, preprint non revu) ne change pas ce contrat : sa route exige un autre\n",
" étage absent de Mathlib, et les `Prop` attendent toujours une preuve formelle."
"probabiliste — sont desormais lisibles depuis ce compagnon.\n"
]
}
],
Expand All @@ -2516,4 +2535,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
Loading