[Epic Origami #20404] Pli 1 - Carnet ANALYSE réflexif : les thèses de « On proof and progress » (Thurston 1994) mesurées sur le corpus du dépôt #20426

Rattaché à #20404

Part of #20404 — Pli 1 de l'épic Origami Thurston.

Objet

Un carnet de distillation réflexif : les thèses de W. P. Thurston dans « On proof and progress in mathematics » (Bull. AMS 30 (1994) 161–177, arXiv math/9404236), écrit en réponse à Jaffe–Quinn (« Theoretical mathematics », arXiv math/9307227), sont confrontées à des données mesurées sur ce dépôt. Le carnet ne produit pas un essai : chaque thèse retenue débouche sur une mesure, un tableau ou une figure calculés depuis le corpus, puis sur une lecture de ce que la mesure dit et ne dit pas.

Le dépôt se prête à l'exercice parce qu'il produit à la fois des certificats (modules Lean vérifiés par le noyau, lake build, proof-integrity) et de la communication (carnets qui expliquent, exercices, interprétations), et parce qu'une partie des preuves y est produite par des agents IA puis « digérée » (#13106).

Thèses à rendre mesurables (au moins trois)

La lane choisit les thèses qu'elle mesure (trois au minimum) et écrit pourquoi elle écarte les autres.

Organes à invoquer, pas à réimplémenter

Les instruments existent déjà dans le dépôt (règle organ-first) :

• scripts/lean/count_code_sorry.py --json : état réel des preuves par lake ;
• scripts/notebook_tools/check_output_collapse.py et check_source_collapse.py : perte de sortie ou de source, c'est-à-dire de communication, entre deux versions d'un carnet ;
• scripts/notebook_tools/check_activity_leak.py : part de récit de fabrication dans un carnet (ce qui n'est pas de la compréhension mathématique) ;
• scripts/notebook_tools/check_prose_quantitative_claims.py : prose quantitative non adossée à une sortie.

Le body de la PR répond aux cinq questions d'organ-first pour toute mesure qui ne passe pas par l'un de ces organes.

Emplacement

Série MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/, voisine d'ANALYSE-02 (positions de Tao). Numéro : le prochain libre de la série, vérifié au moment du claim (des numéros sont réservés par des chantiers en cours, dont #19898). Aucun renommage de carnet existant.

Frontières

• [Distillation] Sheydvasser : fin de « Surviving proofs » (2 art.), tour de géométrie différentielle, formes modulaires I-II, triptyque ensembles-catégories, 14 leçons sur les groupes, Gödel — et le trèfle en géométrie algébrique (hidden-phenomena) #19333 (Sheydvasser, « Surviving proofs ») : le carnet cite la série, il ne l'absorbe pas.
• EPIC: Digestion et canonicalisation des mathématiques assistées par IA #13106 (digestion des mathématiques assistées par IA) : le carnet fournit une mesure à cet épic, il n'en refait pas le plan.
• Le carnet ne juge aucune lane ni aucun agent nommément : les mesures portent sur des artefacts (lakes, carnets, traces), et le récit de coordination reste hors du carnet.

Verdict SOTA attendu

SOTA-OK : les mesures passent par les organes du dépôt et par lake. Une thèse qui ne peut pas se mesurer sur ce corpus est déclarée INTRINSIC, avec la raison écrite dans le carnet, et elle reste dans le carnet comme limite assumée.

Critères d'acceptation

1. Carnet exécuté de bout en bout, sorties réelles committées (C.2), 0 erreur.
2. Au moins trois thèses confrontées chacune à une mesure calculée dans le carnet, avec sa lecture et sa limite.
3. Au moins trois exercices (C.1 : stubs qui s'exécutent).
4. Bibliographie archivée au gisement G:\Mon Drive\MyIA\IA\Bibliographie IA : Thurston 1994, Jaffe–Quinn 1993, et Thurston « Mathematical education » (Notices AMS 1990, arXiv math/0503081). Le body de la PR cite les chemins GDrive. Aucun PDF dans le dépôt.
5. README de la série ANALYSE mis à jour (présentation du carnet, sans totaux).

Grain: DEEP/notebook-python — lane myia-po-2024:CoursIA-2 — prev: DEEP/notebook-python #20373