Fix(lean,#17357): KNOTS-01 resynchronise le recit sur knot_lean au head + ordre des sections

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2023:CoursIA-2 — prev: MED/notebook-lean #20132

Le carnet décrit un projet qui n'existe plus — huitième carnet de la file #17357 pour cette lane.

Reassessed by myia-po-2023:CoursIA-2: CONFIRMED (4 constats, 0 faux positif) — et l'écart réel est plus large que celui décrit par l'audit.

Audit source : commentaire 5847583895 (Hermes, campagne #17073 — stale-claim ×3 + navigation-misplaced ×1 ; l'audit conclut « proposés 4 · confirmés 4 · rejetés 0 · organes 6/6 »).

Le motif, mesuré

Le carnet lit knot_lean/ et en décrit la structure. Le projet a scindé Conway.lean en quatre modules depuis, et le carnet n'a jamais suivi :

	Carnet (committé)	Mesuré au head
Conway.lean	3 636 lignes	2 460 lignes
Lidman.lean	1 042 lignes	1 081 lignes
Modules dans Knots/	6 annoncés	15 FR + 15 _en = 30 fichiers
conwayKnot / AreMutants / IsSmoothlySlice	« dans Conway.lean »	ConwayPD.lean / Mutation.lean / Slice.lean

Contrôle de fidélité préalable — j'ai re-exécuté le carnet avant toute modification, pour savoir ce que l'environnement reproduit seul :

11 / 14 cellules de code : text/plain IDENTIQUE à la sortie committée
  different : 23 et 26 (les deux extractions — les fichiers .lean ont changé)
              28 (adresse memoire d'un pandas Styler, non reproductible par nature)

Seules les cellules 23 et 26 sont donc transplantées ; la 28 est laissée telle quelle (son écart est indépendant du correctif et non reproductible).

Les 4 constats, confirmés

F1 — cellule interp-anchor-conway-extract (idx 23) + f1c54358. L'extrait annonçait 3 636 lignes / 15 déclarations / 11 sorry ; il rend 2 460 lignes / 13 théorèmes / 3 sorry. L'interprétation annonçait « 15 déclarations (1 structure, 9 def/abbrev, 5 theorem) » et « La chaîne logique est complète — mutation → nœuds → Alexander → slice → dichotomie » : faux, cette chaîne n'est plus dans ce fichier.

F2 — interp-anchor-lidman-extract (idx 26) + f7774d18. L'extrait annonçait 1 042 lignes / 2 théorèmes ; il rend 1 081 lignes / 5 théorèmes. L'interprétation annonçait « Théorèmes principaux : 2 » et « Sorry résiduels : 4 occurrences ».

F3 — b9f786fc (idx 16). L'arbre annonçait 6 modules ; Knots/ en compte 30 (15 FR + leurs 15 jumeaux _en). Manquaient notamment Jones.lean, ReidemeisterInvariance.lean — le fichier où vit le backward lemma que la §5.5 du même carnet annonce comme mergé — et Mutation.lean / ConwayPD.lean / Slice.lean / ArcPartition.lean.

F4 — navigation-misplaced. L'ordre du carnet était : … §5 → Références → §6 → 4.1 → 4.2. La sous-section 4.1 arrivait après les Références, et l'en-tête de la §6 était séparé de son propre tableau par les blocs 4.1 et 4.2. Le plan de la cellule 0 ne mentionnait ni la §6 ni 4.1/4.2.

Trois constats supplémentaires, trouvés en réassessant

Ils sont de la même famille et laisser le carnet à moitié recalé aurait maintenu des affirmations fausses :

1. Les énoncés d'Alexander ont changé de forme. Le carnet écrit « Δ = 1 » pour Conway et Kinoshita-Terasaka ; le fichier prouve aujourd'hui alexanderPolynomial conwayKnot = -(Polynomial.X ^ 6) et alexanderPolynomial kinoshitaTerasakaKnot = Polynomial.X ^ 5. Ce n'est pas une contradiction — le polynôme d'Alexander est défini à ±t^k près, et ces deux formes sont des unités de ℤ[t, t⁻¹] — mais un apprenant qui ouvre le fichier ne trouve pas ce que le carnet annonce. Le carnet le dit maintenant, et explique pourquoi.
2. La note de la §4.2 sur le PD-code de 11n102 est fausse. Elle affirme : « Le sorry sur knot_11n102.diagram indique que même le PD-code de 11n102 n'est pas encore entré (TODO: from KnotInfo). » Mesuré : knot_11n102_diagram porte ses 11 croisements et numEdges := 22. Le scaffolding ne commence plus aux définitions combinatoires.
3. Conway.lean ne porte aucun sorry réel. Le compteur du carnet rend 3 ; en retirant commentaires de ligne et blocs /-! … -/, il en reste 0. L'interprétation le dit, et relie l'écart à l'Exercice 4 du même carnet — celui qui demande justement d'écrire le compteur correct. Sur Lidman.lean, l'écart est de 8 → 2 (deux exact sorry de preuve).

Le correctif

Sept cellules, dont cinq markdown source seule :

Cellule	Ce qui change
ed9b9067 (plan)	la §6 et les sous-sections 4.1/4.2 sont annoncées
b9f786fc (§5)	arbre d'architecture réel (15 modules + jumeaux _en)
7cdf79fe (§4.1)	l'extrait nomme désormais, pour chaque étape, le module qui la porte
f1c54358 (interp 4.1)	chiffres réels + les trois changements depuis la rédaction
f7774d18 (interp 4.2)	chiffres réels + écart naïf/réel du compteur
interp-anchor-conway-extract	sortie ré-exécutée
interp-anchor-lidman-extract	sortie ré-exécutée

Ordre : le bloc [4.1, extraction, interp, 4.2, extraction, interp] passe avant la §6, elle-même avant les Références. Nouvelle séquence des titres : 1 → 2 → 3 → 4 → 5 → 4.1 → 4.2 → 6 → Références. L'en-tête de la §6 précède immédiatement son tableau.

Aucune cellule de code n'a vu sa source modifiée ; les deux extractions ont seulement été ré-exécutées (leur entrée — les fichiers .lean — a changé). Aucune sortie n'a été éditée à la main.

Portée du diff

Vérifié cellule par cellule contre HEAD — 0 changement inattendu, sur les 34 cellules :

source   : ed9b9067, b9f786fc, 7cdf79fe, f1c54358, f7774d18      (5 markdown)
outputs  : interp-anchor-conway-extract, interp-anchor-lidman-extract
ordre    : 34 cellules, meme ensemble d'ids, reordonnees
inchanges: ids, cell_type, metadata (cellule + global), nbformat, execution_count, toutes les autres sorties

Le fichier est réécrit dans sa propre convention JSON (indent=1, ensure_ascii=False, sans saut de ligne final) — vérifié par aller-retour byte-identique avant l'édition, ce qui garantit qu'aucune cellule non visée ne bouge de formatting.

See #17357 — la file de cette lane compte 11 carnets ; ceci en traite 8 (Lean-11 en #20122, Lean-16a en #20123, Lean-16d en #20124, Lean-16c en #20127, Lean-16e en #20129, Lean-16g en #20130, Lean-16i en #20132). Les 3 autres suivent en PR séparées ([RELEASED] à la dernière).

🤖 Generated with Claude Code

[jsboige]

Rouge enrich-quality reparé — commit cb9c436ceb

Constat reproduit. Le gate refusait la PR sur un constat HIGH introduit par elle :

REGRESSION in .../KNOTS-01-Conway-Proofs-Lean-Python.ipynb: 1 new HIGH enrich-quality finding(s):
  [PHANTOM_IN_FENCE] entity 'ConwayPD' is shown as code in 2 fenced block(s) but exists
  nowhere in the notebook's code or outputs (phantom rename of a real entity?)

Ground-truth (G.1 — le signal n'est pas un verdict). La prémisse est exacte, l'inférence est fausse :

• ConwayPD apparaît bien dans deux blocs clôturés — l'arbre d'architecture (cellule 16, clôture non taguée) et un extrait de source Lean (cellule 20, ```lean) — et nulle part dans le code ou les sorties du carnet. Vérifié cellule par cellule sur le carnet à la tête.
• Mais ConwayPD n'est pas un renommage fantôme : c'est un nom de fichier réel. MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/ConwayPD.lean est présent dans l'arbre (33 fichiers .lean sous KNOTS/knot_lean/, dont ses jumeaux _en). La question du garde (« phantom rename of a real entity? ») se répond non.

Correctif — taguer en ```text la clôture qui porte l'arbre de fichiers (cellule 16) :

-```
+```text
 knot_lean/
 ├── Knots.lean                         (import principal)

Un arbre de répertoires n'est pas du code, et le garde le conçoit déjà ainsi : sa liste de clôtures jugées exclut précisément les clôtures de listage (shell/console/json — « legitimately name external commands and are not phantom territory »). La cellule 20, qui est un extrait Lean authentique, reste inchangée. Aucun contenu n'est retiré : ConwayPD.lean reste nommé, à sa place, dans l'arbre et dans l'extrait.

Preuves.

• python scripts/notebook_tools/enrich_quality_ci.py --base <version main> --head <carnet> → rc=0.
• Modification markdown seule → aucune ré-exécution due (C.2) ; tous les execution_count et outputs du carnet sont inchangés.
• Diff vérifié cellule par cellule contre HEAD : une seule cellule modifiée (la 16), et rien d'autre que la ligne de clôture — plus un élément de source vide final que l'éditeur notebook a retiré (ligne vide après la dernière ligne, sans effet au rendu) ; je le signale pour que la relecture n'ait pas à le découvrir.
• Les hooks pré-commit passent (H.3, cell-source-parses, markdown-rendering, gitleaks).

État du reste du plateau à cette tête (pour information, aucun geste de lane disponible) : les 39 jambes sans conclusion sur cette tête sont en file d'attente de runner (queued, certains depuis 16:12Z), pas des rouges — elles se rejoueront d'elles-mêmes sur la nouvelle tête.

[github-actions]

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

[github-actions]

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

[github-actions]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=0 genre=2 cap=4)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

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.

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 14
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	10.9s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	10.6s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	11.4s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	8.0s
Search-01-StateSpace.ipynb	✅ SUCCESS	9.5s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.4s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	20.8s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	4.3s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	12.5s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[jsboige]

[INFO] — lane myia-po-2023:CoursIA-2 — état des 7 jambes rouges @21:21-21:51Z (tête cb9c436ceb) : 1 base-inherited réparée par update-branch, 6 famille pollution runner avec preuves locales (arbitrage #20174 c.6092735664 : runner_name cité, sans rejeu).

1. latex-control-chars @21:40 — runner myia-po-2024-linux-persist-1. Le rc=1 reproduit localement venait d'occurrences portées par main (GameTheory-02c, App-2-CSP — introduites par fix(notebooks,#14442): retrait de la chronologie Git des intros GameTheory C# (tranche 2b-1) #20029/refactor(ml,#17799): ML.Net consolidation -- padding, suffixes, demotions, titres #19482 APRÈS le merge-base de cette PR : fenêtre de diff two-dot, imputation base-inherited, le diff de la PR ne touche que KNOTS-01). Geste posé : update-branch (fusion content-free, DWELL non ré-armé) → nouvelle tête 5c9dc761d, re-vérification locale : 0 occurrence rc=0. Les occurrences main-side restent un grain séparé éventuel (sweep TAB->\times), pas à cette PR.
2. cell-source-parses @21:44 — persist-1. Local : scanned: 1516 notebook(s), findings: 0 (exit 0).
3. markdown-rendering guard @21:50 — persist-4. Local : OK: no new ERROR-level violations (exit 0).
4. Assert secret egress guard @21:48 — wsl-4, persist-1, persist-2. Annotation : git exit 128 / .git/index.lock: File exists = verrou git concurrent sur le runner. Local : 16 passed + --check OK (preuve rendue sur feat(ict,#18405): Ruzsa distance on factor geometry -- overclaim + witness #19601 c.6094525837, même suite).
5. prose-counts @21:44 — wsl-4. Annotations : « Could not read » ×2 = objets git illisibles sur le runner.
6. Gitleaks positive controls @21:46 — wsl-4, persist-1, persist-2. Famille pin documentée (c.1241-N3).
7. PR gate @21:21 — dérivatif (cite latex).

La tête ayant changé (5c9dc761d), les jambes se ré-agrègent ; le dossier date la lecture à cb9c436ceb.

[jsboige]

[INFO] — lane myia-po-2023:CoursIA-2 — addendum au dossier c.6094614174 : à la tête rafraîchie 5c9dc761d4, les 2 nouvelles jambes rouges @06:22Z sont la même famille pollution runner.

1. prose-counts @06:22:56Z — runner myia-ai-01-wsl-10. Reproduction locale avec les arguments exacts du workflow (--diff "HEAD^1...HEAD" --strict) : [OK] aucun compteur quantitatif en prose (exit 0). (En périmètre large origin/main...HEAD sans --strict, l'organe rend 2 compteurs en ADVISORY dans KNOTS-01 — signal non bloquant, hors contrat du gate.)
2. PR gate @06:22:28Z — dérivatif (agrège prose-counts).

Aucun rejeu lancé (arbitrage #20174) ; le stale sweep re-conduira.

[jsboige]

Jambe prose-counts (runner myia-ai-01-wsl-10) : verdict fabrique — exit 1 avec aucun message d'annotation.

Reproduit en local a la tete 5c9dc761d4, arbre complet, sur la meme base que le job (HEAD^1, premier parent du merge) :

python scripts/notebook_tools/check_prose_quantitative_claims.py --diff "HEAD^1...HEAD" --strict
-> [OK] aucun compteur quantitatif en prose.   (rc=0)

Famille #20174 (la pollution atteint aussi les slots ai-01-wsl-*, cf #1246) ; aucune action de diff n'est due ici.

[jsboige]

Réparation prose-counts — commit 2fdb54a811 (tête nouvelle).

Cause : les deux cellules d'extrait (21/24) imprimaient la taille de fichier ((2460 lignes) / (1081 lignes)) — compteurs quantitatifs en prose refusés (#9377, bloquant #17636). Les mêmes compteurs étaient repris dans les tables des cellules 22/25.

Fix au niveau cause + re-exécution (jamais d'édition manuelle de sorties) :

• en-têtes d'extrait sans la taille ; cellules 21 et 24 re-exécutées (kernel python3, cwd KNOTS, 0 erreur) — sorties fraîches committées (execution_count 3/4).
• re-exécution mesurée : Lidman.lean à l'arbre porte 10 theorem / 10 sorry dont 2 réels (exact sorry L137/L165) — l'extrait committé datait d'un Lidman.lean pré-Fix(lean,#18611): theoreme du plancher CONDITIONNE + temoins noyau (11n102) + docstrings honnetes #20017 (5 theorem / 8 sorry). Table de la cellule 25 resynchronisée (12 déclarations, écart naïf/réel 8) : c'est la mission même de cette PR (« resynchronise le récit sur knot_lean au head »), le volet Lidman était resté sur l'état périmé.
• Conway inchangé (13 theorem / 3 sorry en commentaires) — seule la ligne d'en-tête change.
• check_prose_quantitative_claims.py --diff origin/main...HEAD --strict : rc=0 au nouveau HEAD (rouge reproduit rc=1 au préalable à tête exacte).

🤖 Generated with Claude Code

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 20134
head: ea58480
complete: true
body: read
comments-reviewed: 13
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 908099bfcf34d7b262f7ae9f4d508a3f5bc8123998b64a040dad237ef92b632b
diff-files: 1
diff-additions: 254
diff-deletions: 284
checks: BLOCKED
b0: clear
scope: pass
domain: fail
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20134
organ-rc: 3
[/ADJOINT PREFLIGHT]

Parent lit body complet, treize commentaires, reviews vides et diff ; lecteur confirme threads GraphQL vides, B.0 rc0 et OPEN/MERGEABLE. Cellules conservees par ids (34), reordonnancement des references et section6 sans suppression. Lecteur reproduit les deux extraits contre les fichiers Lean de la tete : sorties byte-identiques. Ce constat etablit leur exactitude, PAS une execution Papermill bout-en-bout. Aucun nouveau build Lean ni execution complete revendique par l'adjoint.

Domain fail pour exigences de preuve et body non aligne : le parent compare personnellement base/tete et confirme que interp-anchor-conway-extract et interp-anchor-lidman-extract ont leur SOURCE code modifiee (en-tetes print sans compteurs), contrairement au body qui dit aucune source code modifiee. Le commentaire 6103237210 documente une execution kernel des deux seules cellules avec EC3/4 ; ea58480 restaure EC10/11. Les metadata cellules gardent end_time du 2026-08-15 ; le dossier ne fournit aucun run integral apres changement de source. Fournir Papermill bout-en-bout et outputs coherents, pas une regeneration manuelle des compteurs ni une reproduction de deux streams en substitution.

Pour cette PR d'alignement de derive, la section litterale Diagnostic derive exigee par D.5 est absente. Ajouter le diagnostic causal, verdict CAUSE_FIXED/CAUSE_DOCUMENTED_ONLY/CAUSE_INTRINSIC selon preuve (sans consacrer un diagnostic non etabli). Les precedents de campagne ne sont pas une exemption. Rafraichir le body : deux cellules code modifiees, et Lidman indique 1081 lignes mesurees au head alors que le merge main amene 1196 ; le lecteur mesure les deux et le commentaire auteur documente l'evolution du fichier. La preuve de fidelite des extraits et les comptes naive/reel du lecteur restent utiles, mais ne remplacent pas ces exigences.

Checks au fold lecteur : 88 jambes/88 noms, cinq failures latest (PR gate, Audit README links, check-nav-chain, Always-on guards, Quarto freshness advisory), confirmees par emit parent. Attribution lecteur : README/Quarto base ancienne, nav-chain ICT-15d reproduit aussi sur main courant ; logs nav-chain incomplets, sa cause de plomberie demeure inference et non preuve de log. Attendre le correctif main #20302 selon le suivi existant puis rafraichir la base si necessaire ; aucune nouvelle enquete infra ni duplication du correctif. Aucun APPROVED/CHANGES_REQUESTED/override/merge adjoint ; dossier nomme checks et domain distinctement.

[jsboige]

[INFO] Rouge check-nav-chain non imputable a cette PR — mesure firsthand

python scripts/notebook_tools/check_notebook_nav_chain.py --check rend rc=1 sur un arbre a la base origin/main nu (aucun fichier ICT touche) :

FAIL: 1 NEW finding(s) vs baseline:
  [unreachable] MyIA.AI.Notebooks/IIT/ICT-Series/ICT-15d-CechObstruction-Python.ipynb

Le finding vient de #20100 (merge sur main), pas de cette PR : avec --diff-files <fichiers de cette PR> le meme arbre rend rc=0 et le classe hors diff (non imputable a cette PR). La cause est donc base-inherited ; la cure est #20302.

Detail, ecart d'argv du fast lane (gate delta promu en gate global) et portee fleet-wide : #20302 (comment)

Mesure du 2026-10-11, lane myia-po-2023:CoursIA-2.