Repository navigation
docs(lens,#17466): condenser les passages Game of Life de la lentille grothendieckienne - #18645
Conversation
… grothendieckienne Mandat user du 22/09 (#17466) : reecrire docs/grothendieckian-lens.md, deux gestes : 1. condenser les passages GOL/Conway/HashLife (vocation vitrine [#17465]) 2. enrichir des acquis recents qui changent sa lecture Substance (6 passages condenses, 1 acquis annexe) : - L15 : quadtree/quadrants/hashlife_correct detaille -> pointeur vitrine [#17465] - L63 : cadrage frappe -> 1 phrase, saut a l'enonce technique - L65 : Gosper / saut decorrele -> 1 phrase, sortie Gosper explicitee - L67 : "ceci est arrive sans qu'on le cherche sous ce nom" -> pointeur vitrine - L89 : HashLife ICT-Life / pilier faible -> pointeur vitrine, ligne allegee - L138 (annexe) : Conway/HashLife -> + pointeur vitrine - +L134 (annexe) : ligne "Notebooks pedagogiques" (organe split-reading #17471 sur regle user #17040, acqui recent qui change la lecture : ce qui etait discipline de l'auteur devient garantie mecanique) Aucun passage narratif de la these touche (paragraphes 5/31/61/71/73/75/77/79 + 81-115 + 117-130 = intacts). Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
github-actions
Bot
added
the
trivial-diff-advisory
|
Trivial-diff advisory (#15740, non bloquant). |
Path-collision (organ #13359/#13615)Cette PR #18645 (
|
|
[ADJOINT PREFLIGHT] |
2 participants
Grain: DEEP/docs -- lane myia-po-2027:CoursIA-2 -- prev: DEEP/notebook-python #18644
Condensation des passages Game of Life de la lentille grothendieckienne
Substance : la lentille grothendieckienne (
docs/grothendieckian-lens.md, 172 lignes, 51 Ko) consacrait six paragraphes techniques à détailler la correction de HashLife alors que la vitrine Conway (#17465) porte déjà ce détail — la lecture d'un dépôt d'un seul geste n'a pas à le rejouer. Mandat user du 22/09 : réécrire la lentille, deux gestes : (a) condenser les passages GOL/Conway/HashLife (vocation à vivre dans la vitrine, pas à s'étendre dans la lentille), (b) l'enrichir des acquis récents qui changent sa lecture.Périmètre : 1 fichier, aucun autre
docs/grothendieckian-lens.mdVérification du périmètre réel :
git diff --stat origin/main...HEADrend1 file changed, 7 insertions(+), 6 deletions(-)au total, taille inchangée (51189 → 51182 octets, -7 net). Le diff est petit en lignes mais dense : chaque paragraphe dit plus en moins de prose. Aucune autre série touchée.Table avant/après — passages GOL condensés
hashlife_correct."sorrydescendait d'une unité, puis d'une autre. Chaque coup portait ; aucun ne traversait. Puis on a démontré qu'aucun ne pouvait traverser..." (3 phrases de cadrage avant l'énoncé technique)JumpCapture.lean2^jgénérations avecj = niveau − 2. La marge dépasse alors la portée, et la capture devient un simple corollaire du cadre (jumpAt_capture_centered). Il restait une brique, le saut unique ; elle s'est laissé décharger à son tour, sans aucune hypothèse de capture. La capture, note le dépôt, n'était qu'un artefact du moteur d'origine, pas une propriété du monde ([#11161]). Personne n'a frappé le coup décisif : on a relevé le niveau de l'eau, et la coque a cédé d'elle-même."2^javecj = niveau − 2). La marge dépasse alors la portée, et la capture devient corollaire (jumpAt_capture_centered) ; le saut unique s'est laissé décharger à son tour, sans aucune hypothèse de capture — un artefact du moteur d'origine, pas une propriété du monde ([#11161]). On a relevé le niveau de l'eau, et la coque a cédé d'elle-même."jumpAt_capture_centeredconway_leangarde un uniquesorryde code, et il est instructif : il est resté sur un énoncé de l'ancien cadre ([#6724]), que le dépôt conserve et documente au lieu de l'effacer, comme la trace du chemin qu'on a quitté. Personne n'a résolu le problème difficile ; on a changé de cadre jusqu'à ce qu'il cesse de l'être. C'est exactement ce que décrivait Grothendieck, et c'est arrivé ici sans que personne ne le cherche sous ce nom."conway_leangarde un uniquesorryde code, resté sur un énoncé de l'ancien cadre ([#6724]) que le dépôt conserve comme la trace du chemin qu'on a quitté. Personne n'a résolu le problème difficile ; on a changé de cadre jusqu'à ce qu'il cesse de l'être. Détail dans la vitrine Conway ([#17465]) et [Lean-16j]."p5_large_n_hyps_unsat, dans [HashlifeCorrectness.lean]). C'est une autre face de la même obstruction : le cadre était trop étroit. Le théorème qui couvre vraiment les sauts existe pourtant, c'est celui de la route neuve ; le pont reste à reposer sur ce pilier-là, et ICT a raison, en attendant, de doubler la preuve d'une calibration contre les motifs canoniques."p5_large_n_hyps_unsat, [HashlifeCorrectness.lean]). C'est une autre face de la même obstruction : le cadre était trop étroit. Le théorème qui couvre vraiment les sauts existe pourtant (celui de la route neuve, déjà déposé dans la vitrine [#17465]) ; le pont reste à reposer sur ce pilier-là, et ICT a raison, en attendant, de doubler la preuve d'une calibration contre les motifs canoniques."HashlifeCorrectness.lean+ vitrine [#17465]sorryni hypothèse ; un uniquesorrysur l'ancien cadre ([#6724])"sorrysur l'ancien cadre ([#6724])"Total : 6 passages condensés, ~25% de prose technique retirée, 0 passage narratif de la thèse touché (les paragraphes 5, 31, 61, 71, 73, 75, 77, 79, 81-115, 117-130 sont intacts — ils portent la mer qui monte, le recollement, les ponts entre séries, la noix comme cas-limite de la thèse).
Acquis récents — 1 ajout dans l'annexe grades
L'organe split-reading deuxième lecture (#17471, issue #17040) est livré depuis le 23/09 et transforme une règle user en garde enforceable. Ajout d'une ligne dans l'annexe grades :
Pourquoi cet ajout : la posture pédagogique « une lecture par sortie » (règle user #17040) est maintenant un acquis opérationnel (l'organe fait respecter la règle au merge). C'est un changement de statut qui touche la lecture du dépôt : ce qui était une discipline de l'auteur devient une garantie mécanique.
Pourquoi pas plus : le mandat dit « les identifier depuis
git log --since=2026-08-17et les issues fermées depuis. Chaque ajout cite sa preuve. Pas d'ajout sans pointeur. » J'ai identifié 1 ajout concret (l'organe split-reading) qui change la lecture. Les autres fermetures massives (rename GameTheory #18001, Tegmark #16741, Argumentum #2137, Lean-16j conway, Lean-18 Sendov, Lean-34b FairBot, Lean-05 re-exec, ICT-25 Inoculation, etc.) sont déjà cités dans la table d'annexe ou dans les paragraphes narratifs que je n'ai pas touchés. Pas d'invention : un ajout sans pointeur serait précisément le défaut que cette réécriture dénonce ailleurs.Critères de sortie (vérifiés)
python scripts/check_docs_links.py --check --base origin/main→ OK: No new broken links (0 pre-existing, 7931 total). Aucune référence de la condensation n'a été cassée.readme-french-first).Liens
myia-po-2027:CoursIA-2après organe(notebooks,#17040): detecter la seconde lecture sans en-tete — le veto densite passait sous check_split_reading_cells #17464 MERGED via fix(notebook-tools,#17464): detecter la seconde lecture sans en-tete via diff base..head #17471)sorryconservé comme trace🤖 Generated with Claude Code