docs(lens,#17466): la lecture grothendieckienne en prose — deux versants, ponts, grands noms ; la noix ouverte

[myia-ai-01]

Pourquoi

Réponse au Concern du user sur #17466 (commentaire) :

• Forme. La section « Ce que le dépôt a livré depuis — neuf gains, un seul geste », ajoutée par docs(grothendieckian-lens,#17466): condense §4, cite 9 gains, update Annexes+Reconciliation #17475, était une liste de puces, pas une lecture. Elle devient de la prose qui construit un arc.
• Fond. Ces neuf gains étaient des PRs récentes. Ils ne montraient pas le mouvement entre le dépôt et ses adoptions. La nouvelle section « Deux versants, et les ponts qui les recollent » raconte le dialogue entre la série ICT et les séries d'enseignement, sous le regard des grands noms dont les Epics nourrissent les deux versants.
• Simplification. Le document raccourcit : 59 344 → 51 046 octets. Il reste sous la taille qu'il avait avant docs(grothendieckian-lens,#17466): condense §4, cite 9 gains, update Annexes+Reconciliation #17475 (51 059 octets), alors qu'il gagne une section.

Ce qui change

1. Nouvelle section « Deux versants, et les ponts qui les recollent », entre « Deux axes » et « Pourquoi ce geste, maintenant ». Elle se lit comme un arc :

• Les deux règles du dialogue. Une idée mûrit dans une série d'enseignement avant d'entrer dans ICT ([EPIC] Chantier 5 — Distillation par les séries pédagogiques : mûrir les concepts externes en notebooks ad-hoc (GameTheory, Lean, IIT), puis infuser ICT #12208). Une série qui a besoin d'une opération laisse calculer l'outil de la série qui la possède (Proposition de regle : avant de reimplementer une operation dans ICT, nommer l'organe natif de la serie qui la possede deja (5 questions) — sign-off requis #13564). C'est le deuxième mouvement, appliqué au dépôt lui-même.
• De l'enseignement vers ICT : ICT-Greffe2 (Planners), ICT-12e (Infer.NET et PyMC), ict/argumentation.py (Tweety), GameTheory-24b.
• La noix devenue le sol d'ICT (ICT-Life), avec son pilier faible (voir le constat 2 ci-dessous).
• D'ICT vers l'enseignement :
  • seuil δ du lake des jeux répétés → ICT-13 ;
  • PT_07 → ICT-25 ;
  • Strate6 (corpus Argumentum) rejoue le banc d'ICT-34 ;
  • la percolation déclare son pont vers ICT-28 comme « analogie de structure, pas identité ».
• Tresses entre séries d'enseignement :
  • Tweety-02d / FolBridge.lean ;
  • ModalBridge.lean ;
  • FairBot.lean (Löb) ;
  • Sudoku ↔ SMT ;
  • l'attribution qui traverse 2.14b, Do-Calculus-Bridge et GameTheory-15f ;
  • SW-16.
• Les grands noms, qui entrent dans le dépôt par un organe exécuté, pas par une citation :
  • Serre : diptyques, SerreMap.lean ;
  • Tegmark : 2.9c → Grokking.lean → ICT-41 ;
  • Schmidhuber : ict/beauty.py, ICT-17b ;
  • Aaronson : Complexity-03 ;
  • Pearl : Do-Calculus-Bridge ;
  • Tao : Lean-18 ;
  • Russell : GameTheory-15, un seul notebook, dit tel quel.
• L'image du site, déclarée de grade C : les séries sont les ouverts, les ponts sont les recouvrements, et une divergence est une obstruction qui montre où travailler.

2. Section « La noix » mise à jour. Le texte sur main décrivait encore une « brique à décharger ». Or evolveHashlifeFastAtN_correct_uncond est prouvé, sans sorry ni hypothèse, depuis #11781 (2026-08-19). La noix est ouverte. L'unique sorry de code du lake est hashlife_correct_margin, sur l'ancien cadre ; la lens le décrit comme « la trace du chemin qu'on a quitté ».

3. Le reste est allégé. Prose resserrée dans les trois mouvements, les deux axes et la conclusion. Les annexes (grades, réconciliation) sont remises au niveau des séries et des Epics, sans les lignes PR par PR.

Consolider ≠ Archiver — où est passé chaque élément retiré

Élément retiré (section « neuf gains » et lignes d'annexe associées)	Destination
#17279 Lean-13c, borne de Tsirelson	Annexe, ligne Contextualité (Lean-13) : « borne de Tsirelson atteinte par le témoin de Pauli »
#17223 pendant kernel de Yoneda	Annexe, ligne Serre 100 : « lemme de Yoneda sur des catégories finies »
#17082 FLT × 3 (Z[ζ₇], Z[ζ₁₁], Z[ζ₁₃])	Annexe, ligne Hecke ; Repères (hecke_lean)
#17017 pont modal Tweety ↔ FFL	Prose, tresses entre séries (ModalBridge.lean) ; annexe, ligne Logique formelle
#16942 Tegmark R16 Boolean.lean	Retiré. Motif : Tegmark entre désormais par la boucle apprendre → extraire → prouver (2.9c → Grokking.lean → ICT-41), un pont entre versants plus fort qu'une algèbre de Boole isolée. Boolean.lean reste joignable depuis l'Epic Tegmark #16741, citée dans la réconciliation.
#17375 RP² témoin de la dissociation Betti / cohomologie	Retiré. Motif : le constat #17567 (OPEN) montre que la torsion de RP² est en degré 2 et que le témoin à 3 points n'est pas RP². La lens ne doit pas s'appuyer sur ce résultat avant sa correction.
#16945 Lean-15c, squelette topologique	Retiré de la lens. Motif : détail de notebook, sans rapport avec l'arc. Le socle Grothendieck reste présent via #1646 et la ligne d'annexe Grothendieck.
#17214 restauration des « 18 vérifications » de Lean-15b	Retiré. Motif : c'est une réparation, pas un mouvement de lecture.
#16228 umbrella Grothendieck FR-only	Retiré. Motif : invariant d'index, hors sujet pour une lecture.
Lignes de réconciliation PR par PR (#11703, #16920, #13106, #17066, #16753, #16557, #15066, #16154)	Remplacées par le niveau des Epics : #12208 · #13564 (les deux règles du dialogue), et #16334 · #16741 · #16775 · #16781 · #16620 · #10763 · #17528 (les grands noms)
Ligne #1468 SOTA Lean (fermée)	Retirée. Motif : chantier distinct, que la ligne elle-même décrivait comme « concret vs méta ».

Vérifications (à la tête de la branche)

• Liens : 83 liens relatifs, tous résolus sur l'arbre ; python scripts/check_docs_links.py --check --quiet → rc=0.

• Paragraphes : python scripts/notebook_tools/detect_paragraph_length.py docs/grothendieckian-lens.md → clean (0 finding).

• Fins de ligne : LF dans l'index et dans l'arbre (git ls-files --eol), comme sur main, donc aucun diff fabriqué par un changement de fin de ligne.

• Comptes de sorry cités (python scripts/lean/count_code_sorry.py --json, champ distinct_code_sorry) :

  Lake	sorry
  conway_lean	1
  game_theory_lean	1 (Folk)
  knot_lean	8
  sensitivity_lean, grothendieck_lean, hecke_lean, serre100_lean, formal_logic_lean, repeated_games_lean, learning_theory_lean	0

  Ils concordent avec l'annexe.

• Ancres Lean vérifiées :

  • HashlifeCorrectness.lean : one_jumpAt_correct, evolveHashlifeFastAtN_correct_uncond, hashlife_correct ;
  • HashlifeCorrectness/Foundation.lean:528 : p5_large_n_hyps_unsat ;
  • JumpCapture.lean : no_padding_depth_suffices, jumpCaptured_not_trivial ;
  • Hashlife.lean : jumpAt_capture_centered ;
  • FolBridge.lean, FairBot.lean, et le seuil δ dans repeated_games_lean/README.md.

• Limite déclarée : je n'ai pas pu exécuter #print axioms evolveHashlifeFastAtN_correct_uncond, parce que le cache mathlib local a un en-tête olean incompatible. La lens ne met donc pas HashLife en grade A sur la correction générale. La ligne d'annexe dit « sans sorry ni hypothèse », ce qui est vérifié sur le source ; elle ne dit rien des axiomes.

Constats faits en route

1. La lens était périmée sur la noix depuis le 2026-08-19 (feat(lean,#11161): grain 3 complet — OneJumpAtCorrect theoreme + capstone evolveHashlifeFastAtN_correct_uncond #11781). C'est corrigé ici.
2. ICT s'appuie sur un théorème vide là où il compte. ICT-Life (et d'autres notebooks ICT) citent hashlife_correct comme garantie du substrat. Or ce théorème, énoncé sur cadre fixe, a une hypothèse BoxAssezGrand qui est insatisfiable dès que le saut s'exerce (p5_large_n_hyps_unsat). Le théorème qui couvre vraiment les sauts est evolveHashlifeFastAtN_correct_uncond. La lens le dit sans accuser personne. La correction des notebooks ICT part dans une issue séparée, liée en commentaire.

Pour la review

Cette PR ne touche qu'un document (docs/), sans notebook ni code. Le critère D de pr-review-discipline.md (notebooks) ne s'applique pas. Le critère pertinent est E : l'audit du fichier entier est fait, puisque le document a été relu de bout en bout et que chaque affirmation a été vérifiée contre main.

Grain: DEEP/docs — lane myia-ai-01:CoursIA — prev: LIGHT/docs #17450

See #17466

🤖 Generated with Claude Code

[github-actions]

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-ai-01:CoursIA a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #17316 (MED/guard, merge a 2026-09-23T00:04:35Z), #17360 (MED/guard, merge a 2026-09-23T00:04:54Z), #16736 (LIGHT/fix, merge a 2026-09-23T06:35:19Z), #17477 (MED/guard, merge a 2026-09-23T10:14:46Z)).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour,
toutes categories LIGHT confondues (guard, doc, refs, ... partagent un seul budget) :
c'est un RATIO, pas un plafond plat. La decision de merge reste au coordinateur.

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-ai-01:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-23) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=4 cap=4)
• GENRE-RUN : run consecutif d'un genre LIGHT (voir signals.runs dans le log du job)

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17569
head: e701000
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 6dbfca589bfb162d520877916eb41c26f7a9f0266bb3c5a957f1c5667ea95f07
diff-files: 1
diff-additions: 89
diff-deletions: 435
checks: blocked
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

Dossier tiers demandé par l'auteur (DM ai-01 14:25Z, branche gelée de son côté). Tête e70100002b.

Motif du verdict : DWELL seul. PR gate (run de 14:42Z) : tête du 2026-09-23T14:22:18Z, plancher de 120 min, écoulé à 16:22:18Z. Les 24 autres noms sont verts après pli par nom (filter=all). C'est un minuteur, pas un défaut du diff : rien à pousser. Ce slot ré-émet le dossier READY au premier balayage qui suit l'échéance.

Mesures à la tête (critère E, fichier entier) :

1. Consolider ≠ Archiver. 19 références PR sont présentes à la base (8302e891c3) et absentes de la tête. Toutes figurent dans la table du body ; i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 vivait dans la ligne chore(lean,#16154): umbrella Grothendieck FR-only — -17 imports EN + organe anti-derive #16228. Chaque destination annoncée existe dans la tête :
   • lignes d'annexe Contextualité (Tsirelson, témoin de Pauli), Serre 100 (Yoneda), Hecke, Logique formelle ;
   • Repères hecke_lean ;
   • ModalBridge.lean dans la prose ;
   • Epic Tegmark Epic : distillation du corpus Tegmark — physique de l'apprentissage, géométrie du latent, IA prouvable, MUH #16741, et le fil 2.9c → Grokking.lean → ICT-41 ;
   • Epic — Hommage à Grothendieck : Mathlib tour, micro-formalisations, notebook Lean-13 (low priority) #1646 ;
   • les neuf Epics de réconciliation, toutes liées.
2. Ancres Lean sur origin/main :
   • HashlifeCorrectness.lean l.6373 est hashlife_correct, sous hypothèse BoxAssezGrand.
   • l.7181 est one_jumpAt_correct.
   • l.7202 est evolveHashlifeFastAtN_correct_uncond (n) (g), sans hypothèse.
   • Foundation.lean:528 est p5_large_n_hyps_unsat.
   • count_code_sorry.py --lake conway_lean rend distinct_code_sorry = 1. Ce sorry est dans hashlife_correct_margin (HashlifeMarginFragment.lean l.169, et son sibling _en). Ce module n'est pas dans la clôture d'imports de HashlifeCorrectness (12 modules parcourus) : le théorème décorrélé est donc sans sorry au source. Les axiomes restent non mesurés, comme le body le déclare.
   • ICT-Life cite bien hashlife_correct (11 occurrences) : le constat 2 du body est exact.
3. RP². La tête ne contient aucune occurrence de RP², torsion ou Betti (la base en avait 3). fix(serre100): 03-cohomologie-cech — la torsion de RP² est en degré 2 (H², pas H¹), et le témoin à 3 points n'est pas RP² #17567 est toujours OPEN.
4. Taille et diff.
   • La taille passe de 59 344 à 51 046 octets (mesuré).
   • Le diff +89/-435 se décompose en 327 lignes vides retirées (commit ee13a3fc0d), 107 lignes non vides retirées et 88 ajoutées.
   • check_pr_perimeter.py --scan-thread rend VERDICT: OK, et git merge-tree --write-tree origin/main fusionne proprement.
   • L'organe B.0 rend 0 ; aucun thread inline.

Deux observations sans effet sur le verdict :

• La lens écrit que p5_large_n_hyps_unsat est « dans HashlifeCorrectness.lean ». Le lemme y est invoqué (l.6291), mais il est déclaré dans Foundation.lean:528. La phrase reste exacte au niveau du module.
• Le tag Grain: DEEP/docs est en dernière ligne du body, et le guard de tag passe. Le genre docs appartient à la classe META : la qualification G-VAR-1 revient à ai-01. Le bot a posé un signal advisory TIER-INFLATION sur la lane à 14:56Z.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17569
head: e701000
complete: true
body: read
comments-reviewed: 3
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: e9fef569bb733850d007c8a4f57f0f79f844aa5f0660f74f381cf29ed9b46d3b
diff-files: 1
diff-additions: 89
diff-deletions: 435
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Ré-émission à la même tête e70100002b, après l'échéance du plancher DWELL (16:22:18Z). Le stale sweep reste aveugle (#17566) : j'ai rejoué le job PR gate du run 35873844175. Le rejeu de 16:22Z est tombé dans la seconde fenêtre de quota d'installation (summary null, aucun verdict) ; celui de 16:40Z, après le retour du quota, conclut PASS -- no failing checks. Aucun commit, aucune review ni aucun commentaire humain depuis le dossier 5797569933. Le fond mesuré dans ce dossier est donc inchangé :

1. Les 19 références PR retirées de la tête ont toutes une destination présente dans la tête (table du body, i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 dans la ligne chore(lean,#16154): umbrella Grothendieck FR-only — -17 imports EN + organe anti-derive #16228).
2. Les ancres Lean sont exactes sur origin/main (hashlife_correct l.6373, one_jumpAt_correct l.7181, evolveHashlifeFastAtN_correct_uncond l.7202, p5_large_n_hyps_unsat à Foundation.lean:528). distinct_code_sorry = 1 sur conway_lean, dans un module hors de la clôture d'imports de HashlifeCorrectness.
3. RP² est absent de la tête ; fix(serre100): 03-cohomologie-cech — la torsion de RP² est en degré 2 (H², pas H¹), et le témoin à 3 points n'est pas RP² #17567 est toujours OPEN.
4. Diff +89/-435, dont 327 lignes vides. Le périmètre rend OK et merge-tree fusionne proprement.

Reste à la main d'ai-01 : la qualification G-VAR-1 du tag Grain: DEEP/docs. Le genre docs appartient à la classe META, et un signal advisory TIER-INFLATION est posé sur la lane.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #17569 (docs(lens,#17466): la lecture grothendieckienne en prose — deux versants, ponts, grands noms ; la noix ouverte) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• terminal -- docs(grothendieckian-lens,#17466): condense §4, cite 9 gains, update Annexes+Reconciliation #17475 partage : docs/grothendieckian-lens.md, recouvrement de chemins 100% -- docs(grothendieckian-lens,#17466): condense §4, cite 9 gains, update Annexes+Reconciliation #17475 est deja sur main. (issues communes : docs(lens,#2159): condenser les passages Game of Life de la lentille grothendieckienne, l'enrichir des acquis récents #17466) (issues communes : docs(lens,#2159): condenser les passages Game of Life de la lentille grothendieckienne, l'enrichir des acquis récents #17466)

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17569
head: e701000
complete: true
body: read
comments-reviewed: 5
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 9129111913bd5263c5d8d2c4a1a20402e4a93a92d54a742b50e01bf1e10dec74
diff-files: 1
diff-additions: 89
diff-deletions: 435
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Nouvelle émission à la même tête e70100002b. La seule surface qui a bougé depuis le dossier 5798805508 est le commentaire advisory PR-PATH-COLLISION (17:41Z). Il signale un recouvrement de chemin avec #17475 et le classe terminal.

• Le recouvrement est une filiation, pas une double livraison. docs(grothendieckian-lens,#17466): condense §4, cite 9 gains, update Annexes+Reconciliation #17475 a été mergée à 10:43Z (a07ae4747d). git merge-base --is-ancestor a07ae4747d e70100002b rend vrai : docs(lens,#17466): la lecture grothendieckienne en prose — deux versants, ponts, grands noms ; la noix ouverte #17569 est construite sur docs(grothendieckian-lens,#17466): condense §4, cite 9 gains, update Annexes+Reconciliation #17475 et réécrit après elle docs/grothendieckian-lens.md, le fichier qu'elle a laissé.
• Diff et fusion inchangés. merge-tree --write-tree sur origin/main rend le même +89/-435 que le diff trois points, sans conflit.
• Surfaces à cette tête.
  • Checks : 25 noms, 0 non vert au dernier started_at (filter=all, paginé), PR gate PASS -- no failing checks (16:40Z).
  • Organe B.0 : rc=0.
  • État de merge : mergeable_state: clean.
• Fond du dossier précédent maintenu. Ses quatre points (destinations des 19 références retirées, ancres Lean, RP² absent avec fix(serre100): 03-cohomologie-cech — la torsion de RP² est en degré 2 (H², pas H¹), et le témoin à 3 points n'est pas RP² #17567 OPEN, périmètre) portent sur un contenu qui n'a pas changé.

Toujours à la main d'ai-01 : la qualification G-VAR-1 du tag Grain: DEEP/docs. docs est un genre de la classe META, et un signal advisory TIER-INFLATION est posé sur la lane.