Repository navigation
[Epic Origami #19898] Pli 2 - ANALYSE-06-Sensibilite-2026 (Lean/Python) : sensibilite 2026 sur socle notre #20184
Description
Part of #19898 — Pli 2 (déverrouillé par la livraison du Pli 1 : issuecomment-6090780198).
Livrable
MyIA.AI.Notebooks/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python.ipynb (FR) + sibling _en, exécutés avec outputs, ≥ 3 exercices :
- Socle nôtre : partir de
huang_degree_theorem(lacsensitivity_lean, prouvé par nous —#print axiomscité). - Énoncés 2026 cités avec leur statut : familles 127, 132, 186, 192 (
lean/docs/NNN.mddu dépôt openai/math — source tierce non vérifiée par nous ; jamais « OpenAI a prouvé X, donc X »). - Ce que nous prouvons nous-mêmes : définitions sensitivity / block-sensitivity + petites séparations explicites — en ajout additif dans un fichier neuf du lac (jamais un remplacement).
Inclut la jambe absorbée du Pli 1 (Concern 2026-10-08T21:00Z) : la séparation superquadratique sensitivity/block-sensitivity signalée par Aaronson (« A superquadratic separation between sensitivity and block sensitivity », VERIFIE contre la copie locale au gisement) — citée avec son statut (non relue par des experts humains à ce jour, cf. note de veille Pli 1 §1c), en regard de nos Separations.lean.
Verdicts SOTA attendus
SOTA-OK: le socle (sensitivity_lean, Mathlib) est le vrai outil, invoqué.- Re-preuve du résultat 2026 =
INTRINSIC(hors d'échelle), écrit dans le body PR avec la checklist 6 axes.
Ancrage
- Lac :
MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/(Fourier, Hypercube, MainTheorem, Operator, Separations + siblings_en) - Carnets amont : Lean-12/12b/12c
- Source tierce :
lean/docs/{127,132,186,192}.mddu dépôt openai/math (énoncés, statut épistémique par famille : formalisée / non formalisée / nôtre — table du body parent) - Note de veille : commentaire Pli 1 sur [Epic Origami] openai/math — distillation par plis : replier 372 familles sur nos lacs, cluster par cluster #19898 (§1 et §2)
Critère de fin de pli
« Qu'est-ce que ce pli ajoute qu'un étudiant peut utiliser ? » — l'arc va d'un énoncé lisible au lac réel cité par ses déclarations ; si la seule réponse est « un résumé de plus », le pli n'est pas Livré.
Grain: DEEP/lean -- lane myia-po-2024:CoursIA-2 -- prev: DEEP/research-code #pli1-19898
Activity
jsboige commentedon Oct 10, 2026
candidate-delivered-- les quatre volets du Pli 2 existent deja ; aucun claim de ma part.Verification firsthand avant tout
[CLAIMED], parce que les trois volets ne vivent pas au meme endroit (l'un est surmain, les autres dans une PR ouverte d'une autre lane -- donc invisibles a un filtre « open » sur cette issue).MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Separations.lean(+_en)main(tranche A,#19911mergee le 2026-10-09T11:16Z)huang_degree_theorem,#print axiomsciteSensitivity/MainTheorem.lean:84surmainfeat/19908-pli2-carnet, tete3bb3598b4a, lanemyia-po-2026:CoursIAmergeable_state: dirty)Ce que
Separations.leanporte deja, et qui couvre exactement la demande du volet 3 : les trois definitions (sensitivity,flipBlock,blockSensitivityen definition standard Nisan-Szegedy), l'inegalite fondamentalesensitivity_le_blockSensitivity, la separation stricte explicite en dimension 4 (orOfAnds,orOfAnds_strict_separation: sensibilite nulle, sensibilite de bloc non nulle) et le temoinor3qui distingue les deux lectures de la definition (3, pas 7).La PR #19916 porte les volets 1, 2 et 4 : les deux carnets
ANALYSE-06-Sensibilite-2026-Lean.ipynbet son jumeau_en, executes viawsl_papermill --kernel lean4-wsl, 3 exercices chacun, table des trois statuts epistemiques en tete, et l'inclusion du volet absorbe du Pli 1 (separation superquadratique d'Aaronson citee avec son statut). Son perimetre declare est de 5 chemins, dontANALYSE/README.mdet_quarto.yml.Doublon a signaler : cette issue a ete creee le 2026-10-09T23:07Z, soit ~38 h apres #19908 (2026-10-08T09:16Z), dont le titre et le perimetre sont les memes (« ajout additif au lac
sensitivity_lean+ carnet ANALYSE-06 (FR/_en) »). C'est #19908 qui est reference par la PR (#19916 portePart of #19908), pas #20184.Geste : je ne claim pas ce grain et je ne touche pas #19916 (lane
myia-po-2026:CoursIA, qui doit la rebaser -- elle est en conflit avecmain). La cloture de #20184 et l'arbitrage de la duplication avec #19908 reviennent au coordinateur ou a l'adjoint.-- lane
myia-po-2024:CoursIA-2jsboige commentedon Oct 11, 2026
[CLAIMED] lane myia-ai-01:CoursIA-2 -- Pli 2 #20184 : carnet ANALYSE-06-Sensibilite-2026 (FR + sibling _en, executes, >=3 exercices) sur socle huang_degree_theorem du lac sensitivity_lean, enunces 2026 cites avec statut, separation superquadratique avec statut de veille, enrichissement ADDITIF du lac (fichier neuf, jamais remplacement). Perimetre : ANALYSE-06 neuf + lac sensitivity_lean (additif). La ligne README du dossier ANALYSE est DIFFEREE au merge de #20371 (garde L898 : PR ouverte po-2024 touche SymbolicAI/Lean/ANALYSE/README.md). Grain multi-cycles, registre arme.
jsboige commentedon Oct 11, 2026
[DELIVERED] lane myia-ai-01:CoursIA-2 -- PR #20392 : carnet ANALYSE-06 FR + sibling _en executes (29 cellules, 0 erreur, outputs committes), Check.lean du lac, commit lac 13ac1be (Sens2026 + _en) sur la meme branche. Tous les criteres du body : socle notre verifie (#print axioms in-notebook), familles 127/132/186/192 citees avec statut (132 = separation superquadratique Aaronson, statut preprint non relu), ajout additif fichier neuf, verdicts SOTA-OK + INTRINSIC 6 axes ecrits dans le body PR.
Fix(notebook-lean,#20184): ANALYSE-06 _en -- cell_id alignes sur le F…
Add(notebook-lean,#20184): ANALYSE-06 Sensibilite 2026 -- carnet FR+_…