refactor(smt,#5081): Z3-17 suffixe canonique — 1 git mv + referents

[jsboige]

Grain: MED/refactor — lane myia-po-2024:CoursIA-2 — prev: MED/tooling #17750

Quoi

Tranche Z3-17 du renommage canonique SMT (#5081, relance du 25/09 ; bande #16763). Dernier des deux noms différés par #16846 :

Z3-Python-17-Array-Theory.ipynb → Z3-17-Array-Theory-Python.ipynb

Z3-13 reste différé : Z3-Python-13-UnsatCores.ipynb → Z3-13-UnsatCores-Python.ipynb partira après le merge de #17678 (garde #11840 §5.4 — PR ouverte sur le fichier).

Garde anti-collision (avant le git mv)

gh pr list --state open --json number,files : aucune PR ouverte ne touchait Z3-Python-17-Array-Theory.ipynb. Chemins vérifiés libres aussi côté worktrees.

Référents mis à jour dans la même PR (sinon liens morts)

git grep sur origin/main → 0 occurrence de l'ancien nom restante hors COURSE_CATALOG.generated.* (appartient à l'automatisation, laissé byte-identique) :

Fichier	Occurrences	Nature
MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/README.md	1	table de série (cible)
MyIA.AI.Notebooks/SymbolicAI/README.md	1	table de série (cible + libellé)
_quarto.yml	1	liste de build
docs/curriculum/ia-symbolique.md	1	table curriculum (cible seule)
scripts/notebook_tools/pedagogy_density_baseline.json	1	clé du ratchet
scripts/tests/baseline_nb_nav_chain.json	1	clé du baseline nav-chain
Z3-18-Sudoku-Modes-Python.ipynb	1	lien nav en cellule markdown

translations/smt/z3-api.csv — retiré du diff (revert, commit 4625444a73)

La première tête de cette PR éditait aussi les 21 clés de chemin du CSV de traduction. La garde « No hand-edited translation files on feature branch » l'a refusé : ce CSV est un fichier dérivé (régénéré par translation-sync.yml, sur hold manuel-maintainer depuis le 2026-08-12, #10038/#15198), et le diff était purement cosmétique (substitution du chemin sur 21 lignes, contenu byte-identique). Le revert ramène le CSV au contenu d'origin/main ; la régénération automatique fera la même substitution quand le hold sera levé. Détail du diagnostic : commentaire 5831269527.

Le CSV retarde donc toujours sur le nouveau nom (comme COURSE_CATALOG.generated.*, il appartient à l'automatisation) ; c'est la dette documentée du hold i18n, pas une omission de cette PR.

Baselines : clés déplacées en place, pas perdues

• pedagogy_density_baseline.json — clé déplacée en place (ordre et compte 811 préservés), float re-mesuré via _measure : 1171.0 → 1229.429 (l'ancienne valeur avait dérivé des enrichissements postérieurs, cf fix(smt,#16762): fusion des lectures scindees Z3-13 + Z3-17 — tranche 4/6 (3 paires, dont 1 named_split) #16791). Contrôle : python scripts/notebook_tools/pedagogy_density.py --check-orphans --base origin/main → OK: 811 cles du baseline, 0 ORPHAN_KEY, 0 LOST_KEY.
• baseline_nb_nav_chain.json — l'unique orphan_entry rekeyée. Mesure de contrôle : --check rend 27 NEW sur origin/main comme sur cette branche, ensembles byte-identiques (dérive pré-existante du baseline du 24/09 ; le guard feat(notebook-tools,#17093): garde d'atteignabilite de la chaine de navigation (+ tests + baseline) #17285 n'est pas câblé dans .github/workflows/ — vérifié par grep). La PR n'introduit aucun NEW.

C.2 — pas de ré-exécution due

Édition de cellule markdown uniquement dans Z3-18 (cible d'un lien), 0 édition d'output : execution_count intacts (1..5+), JSON valide 19 cellules. Exception explicite de la règle — même traitement que #16846 (« Markdown-only cell edits, 0 output edits, no re-execution needed »).

Preuves

• git diff --stat (tête 4625444a73, post-revert CSV) : 8 fichiers, +7/−7, rename détecté 100 % (git mv). Le renommage lui-même est 0+/0−.
• python scripts/notebook_tools/pedagogy_density.py --check-orphans --base origin/main → 0 ORPHAN_KEY, 0 LOST_KEY.
• git grep "Z3-Python-17-Array-Theory" → 0 hors catalogue généré et CSV dérivé (hold i18n notebooks : T4 renderer + CI autonome — sortir du moteur qui tourne a vide (mandat user 2026-08-08) #10038).
• Diff Z3-18 = 1 ligne (cible du lien ; libellé conservé, convention refactor(smt,#16763): Z3-API canonical suffixes — 26 git mv + referents (13/17 deferred for #16791) #16846).

See #5081, See #16763

🤖 Generated with Claude Code

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

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 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]

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

• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=1 genre=2 cap=1)
• 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]

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

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	5.4s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	13.4s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	6.1s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	5.2s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.1s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.5s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	31.1s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.5s

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

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 7
• 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)

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 17787
head: 9d656c5
complete: true
body: read
comments-reviewed: 6
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 69e22cd7642774a25444f4b9d2891bade0f88cd91286d4a0df6b16bb44b16a6b
diff-files: 9
diff-additions: 28
diff-deletions: 28
checks: blocked-via-dwell
b0: blocked
scope: pass
domain: not-applicable
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

Aucun dossier anterieur. Trois jambes rouges reelles : (1) No hand-edited translation files on feature branch (Detecteur de traduction hand-edited, violation §H/C.2 SOTA, fondation #3473/#11685) ; (2) Scripts Tests (CPU) failure @09:35:47Z, conclusion=failure et non null -- vrai defaut, pas zombie ; (3) PR gate failure @09:21:54Z. 9 fichiers (+28/-28), B.0 rc=0 aucun nit non leve. 92/92 jambes au total, 84 vertes. Vrais defauts de substance : le re-stamp en READY est impossible tant que les deux jambes (1) et (2) ne sont pas levees en code par le porteur (jsboige) ; la lane secretaire ne pose pas de domaine sans le fix. Lecture conseiller a ai-01 : (a) rerun --failed du job 108016201873 ; (b) si le detecteur de traduction persiste en rouge, lever les cellules hand-edited du diff ou poser les 9 fichiers dans .auto-traduits/ (cf regle Stop & Repair).

[jsboige]

Fix appliqué : translations/smt/z3-api.csv rétabli au contenu origin/main (commit 4625444a73). Le PR gate re-tournera et la garde « No hand-edited translation files on feature branch » passera.

Cause exacte (Tell c.11840 §5.4 vérifié)

Le diff translations/smt/z3-api.csv était purement cosmétique : 21 lignes, chemins de fichier Z3-Python-17-Array-Theory.ipynb → Z3-17-Array-Theory-Python.ipynb, contenu markdown byte-identique. Ce CSV est dérivé du notebook source FR ; il est régénéré par translation-sync.yml.

Pourquoi revertir (et pas l'override dual-key #10332)

translation-sync.yml est sur hold manuel-maintainer depuis le 2026-08-12 (#10038, #15198). Éditer le source FR ne régénère pas le CSV tant que le hold tient. Tant que le hold tient, la sortie audit-able pour un changement légitime sur un fichier dérivé est l'override dual-key (#10332).

Ici le changement est purement cosmétique (substitution de chaîne sur 21 lignes) et le source est intact : la régénération automatique fera le même travail quand le hold sera levé. Le revert était strictement plus simple — pas de dual-key nécessaire, pas de risque d'overrider une garde qui protège contre une vraie main-edit.

Sortie du PR gate

Le PR gate attendait 36 checks. Le seul FAILURE était « No hand-edited translation files on feature branch » (cf rollup run 36117899129). Tous les autres checks étaient SUCCESS avant l'échec (CodeQL, Always-on guards, Notebook validation, etc.). Après ce push, le CSV est identique à origin/main (git diff origin/main -- translations/smt/z3-api.csv = vide) → la garde passera.

Suite

• Le merge-gate re-tournera au prochain tick (cron 7 * * * *, cadence réelle 178-341 min par ci(sweep): pr-gate-stale-sweep tire a 28,8 % de sa cadence declaree (mediane 3,5 h, max 6,2 h) -- l'acceptance de #12728 mesurait les annulations, pas le taux de tir #15197)
• Le dossier [ADJOINT PREFLIGHT] reste valide (le head a changé mais le contenu narrow 1:1 — 1 fichier, +21/-21 — reste cohérent : la PR reste git mv + referents + revert CSV dérivé)
• Si vous voulez la note dans le body PR (Tell c.17071 strict, encagée pour ne pas émettre de réserve), je peux l'ajouter ; sinon ce commentaire tient lieu

Lien

• Commit : 4625444a73a021403a14ab014b96a7cfa4e88554
• Branch : refactor/5081-z3-17-canonical (push force-with-lease depuis fix/17787-csv-revert)
• Worktree éphémère : D:/Dev/CoursIA-2-c1449-17787 (à prune après merge, cf L576 ★★)
• Garde source : .github/workflows/translation-guard.yml (run 36117899129, job « Resolve translation-guard override (translation-guard : aucun mecanisme d'arbitrage ecrit — 2 overrides legitimes ce cycle passes par un bypass admin non auditable #10332) »)
• Hold i18n parent : i18n notebooks : T4 renderer + CI autonome — sortir du moteur qui tourne a vide (mandat user 2026-08-08) #10038, ci(guard): translation-guard prescrit un remede inapplicable -- le bot qui 're-derive' est dormant depuis 25 jours (hold #10038), l'override d'exception devient le seul chemin #15198 ; audit dual-key : translation-guard : aucun mecanisme d'arbitrage ecrit — 2 overrides legitimes ce cycle passes par un bypass admin non auditable #10332, i18n grain C: moteur CI autonome — detection de desync CSV + auto-commit bot dans la PR #10042

[jsboige]

Rouge Scripts Tests (CPU) : base-inherited, non réparable par cette lane — preuve ci-dessous.

Mesure

Le test scripts/lean/tests/test_check_axiom_gate_coverage.py::TestRealRefRegression::test_no_lake_ever_lost_the_gate échoue sur serre100_lean :

a deleted dispatcher called lean-axiom.yml and its lake is now served only by the matrix: silent coverage regression. Re-wire the gate or justify it in writing (#17097 criterion 3).

Pourquoi ce rouge n'est pas de cette PR

• Le diff de cette PR (tête 4625444a73, 8 fichiers) ne touche ni scripts/lean/tests/, ni .github/workflows/, ni aucun lake Lean — périmètre : renommage SMT + référents (READMEs, _quarto.yml, curriculum, baselines JSON, 1 cellule markdown Z3-18).
• La cause amont est le commit 52b248a3e0 (feat(lean-ci,#17336): wire serre100 into the CI matrix + first matrix axiom pass (B.3) #17370, sur main) : wire serre100_lean into the CI matrix — c'est ce wiring qui déclenche le détecteur de couverture.
• Corroboration cross-PR au 25/09 ~11:30Z : fix(gate,#17791): exempt hors-flotte PRs from the carrying-lane refusal (claude/* + Hors flotte) #17798 (lane po-2024, périmètre fix/17374-double-triggers sans rapport Lean) porte le même FAILURE sur la même jambe.

Route

Réparation de la couverture axiomatique de serre100_lean = geste coordinateur sur main (re-wire du gate ou justification écrite #17097 critère 3). Cette lane documente et poursuit — le pick suivante passe --ignore-red avec cette justification écrite.

Les autres jambes rouges de la tête 4625444a73 (perimeter guard, PR gate) étaient une contradiction body↔périmètre (le body annonçait 9 fichiers après le revert CSV du commit 4625444a73, le réel en compte 8) — corrigée par l'édition du body (tableau référents et git diff --stat réalignés sur 8 fichiers, +7/−7) et rejeu du run.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #17787 (refactor(smt,#5081): Z3-17 suffixe canonique — 1 git mv + referents) 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.

• faible -- feat(argumentation,#17547): sub-series Onto/Obs with own numbering (PR 2/3) #17721 partage : MyIA.AI.Notebooks/SymbolicAI/README.md, _quarto.yml, docs/curriculum/ia-symbolique.md, scripts/notebook_tools/pedagogy_density_baseline.json, scripts/tests/baseline_nb_nav_chain.json
• faible -- feat(complexity,#17063): 04 « Décider sans connaître la suite » — Online descend en 04b #17786 partage : scripts/tests/baseline_nb_nav_chain.json
• faible -- docs(symbolicai): README de famille a plusieurs vitesses (forme #3973) #17800 partage : MyIA.AI.Notebooks/SymbolicAI/README.md
• faible -- Rename(labellisation,#14873): PyMC-06-Debugging -> PyMC-02b-Debugging-Python (harmonisation jumelle Infer-2b) #17808 partage : scripts/notebook_tools/pedagogy_density_baseline.json

[jsboige]

Note diagnostic base-inherited — rouge lost_gate du PR gate détecté sur #17787 n'est PAS une régression de la PR.

Diagnostic verbatim (Tell c.974 §G.9 strict fondateur pratiqué)

Le job Scripts Tests (CPU) échoue sur :

TestRealRefRegression::test_no_lake_ever_lost_the_gate
AssertionError: a deleted dispatcher called lean-axiom.yml and its lake is now served only by the matrix:
  silent coverage regression. Re-wire the gate or justify it in writing (#17097 criterion 3).
assert [{'dispatcher': 'lean-serre.yml', 'deleted_by': '52b248a3e0', 'had_gate': True,
         'gated_paths': ['MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/serre100_lean']}] == []

Mesure first-hand

L'organe canonique scripts/lean/check_axiom_gate_coverage.py --ref HEAD --json --check rend byte-identique sur HEAD (post-revert CSV 4625444a73) :

{"lost_gate": [{"dispatcher": "lean-serre.yml", "deleted_by": "52b248a3e0",
                "had_gate": True,
                "gated_paths": ["MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/serre100_lean"]}],
 "coverage_entries": 12}

Le commit 52b248a3e0 = #17370 (PR antérieure, mergée dans main avant #17787) = feat(lean-ci,#17336): wire serre100 into the CI matrix + first matrix axiom pass (B.3). Ce commit a supprimé lean-serre.yml au profit de la matrix, mais l'organe test_no_lake_ever_lost_the_gate (introduit par #17440) classe ce déplacement comme "lost gate" — le filet n'a pas encore absorbé le fait que la matrix prend le relais.

Conclusion

Le rouge est pré-existant sur main, byte-identique avant/après le diff de #17787. #17787 ne touche aucun fichier de .github/workflows/ ni scripts/lean/tests/. La PR ne peut pas réparer un rouge base-inherited.

L'organe B.0 ne peut pas non plus classer ce constat comme "auto-résolu" : le filet attend une phrase de levée ou une action coord. Une issue de suivi est ouverte : #17820 fix(lean-ci,#17440): test_no_lake_ever_lost_the_gate — serre100_lean servi par matrix only, organiser la levée du gate (créée en c.1454 après mesure first-hand).

Action attendue du coord : soit amender l'organe pour qu'il absorbe "matrix only" comme reprise de couverture (cf #17097 criterion 3 qui dit "re-wire the gate or justify it in writing"), soit réintroduire un dispatcher lean-serre.yml ciblé. Lane worker ne peut pas trancher ce design-gate sans sign-off coord — c'est précisément le périmètre couvert par Tell c.1374 strict fondateur (voie 2 = issue de suivi nommée, lever le rouge via issue fille).

Suite demandée

Re-run du PR gate une fois l'absorbtion matrix-only mergée sur main (cf #17820). En attendant : la PR est techniquement livrable (mergeStateStatus=CLEAN hors gate), seul le filet B.0 attend la résolution.

Lien

• PR : refactor(smt,#5081): Z3-17 suffixe canonique — 1 git mv + referents #17787, head 4625444a73, base c6edeac60c
• Fichier cause racine : .github/workflows/lean-serre.yml (supprimé par feat(lean-ci,#17336): wire serre100 into the CI matrix + first matrix axiom pass (B.3) #17370)
• Issue de suivi ouverte : fix(lean-ci,#17440): test_no_lake_ever_lost_the_gate — serre100_lean servi par matrix only, organiser la levée du gate #17820 (c.1454)
• Tells observés : c.974 §G.9 (vérif first-hand), c.1374 (voie 2 issue de suivi nommée)

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 17787
head: bc57c47
complete: true
body: read
comments-reviewed: 11
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 9e8b3f0472e00851c68d7f9ae7536bc2d32be9ff58b273f98ae026dd602e66e0
diff-files: 8
diff-additions: 7
diff-deletions: 7
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]

Re-stamp secretaire c.141 -- tiers au titulaire (Tell c.111 strict). Re-stamp secretaire c.146 -- lane po-2024 porteuse, lane attestante po-2026 (Tell c.111 strict fondateur c.95). Hermes APPROVED, B.0 rc=0, gate vert post-DWELL. Lane secretaire myia-po-2026:CoursIA-3. Lane secretaire myia-po-2026:CoursIA-3. Fix emetteur c.141 : stderr separe, ligne 1 gardee.