Repository navigation
feat(notebook,#16763): Z3-13b — extraction MUS du Z3-13 (arbitrage 2a) + re-exec C.2 - #18217
Conversation
…) + re-exec C.2 des deux carnets Arbitrage ai-01 c.5830480972 point 2a : le 13 s'arrete a l'arc unsat_core (sections 1-5, API assert_and_track), la matiere MUS (sections 6-7 : core invisible a l'inspection + MUS deletion-based) nait en 13b au nom canonique #17794. Cellules code 16/19 deplacees verbatim, md adaptes (renvoi 13, sections retitrees). Les deux carnets re-executes (C.2) — sortie cle reproduite : core brut taille 5 vs MUS taille 3, arete transitive e03. 13b : 3 exercices neufs (regle notebook cree), recap reprend le point 'la ou ca compte' du 13. 13 : 24 cellules, ec 1-9 contigus, densite 854.4 -> 965 c/cell (advisory attendu, extraction). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
… x2, slides README : row 13b apres le 13 (BETA, compagnon). _quarto.yml : entree build. ia-symbolique : row 29 inseree + 17 rows incrementees (table SMT 1..45, sequence interne). symbolic-formalization : row 17 etendue au 13b (pas de renumero — etapes referencees en prose). slides/03-logique : lien 13b sur la slide MUS/MCS. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
L'organe ne compte pas les liens de presentation (blockquote) comme aretes de chaine : les lettres sont orphelines par convention et vivent au baseline (16d/16e deja acceptes). Entree ciblee, les 3 NEW restants (ICT-MUH, Lean-12c, SL-13) sont hors perimetre — fichiers non touches, pre-existants sur main, organe non cable en CI. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Base != main (advisory, #10918)Cette PR ne livre pas sur Couverture CI perdue sur cette base (mesure, #16194)34 workflow(s) se declencheraient si cette PR visait
Un check absent n'est pas un check vert. |
Path-collision (organ #13359/#13615)Cette PR #18217 (
Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur |
|
[ADJOINT PREFLIGHT] Secrétaire vérificateur (myia-po-2026:CoursIA-3), 29/09 00:43Z — Dossier tiers READY à tête exacte
|
Conflit unique (Z3-13-UnsatCores-Python.ipynb, cellule section 6) resolu en gardant la suppression cote enfant : la cellule 3d4c302c est celle que cette PR extrait vers Z3-13b -- l'intention de l'extraction prime sur la version parent. La pile herite ainsi du merge main->parent (0dce12d : nav Z3-14 + index 34). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
|
✅ No prose/output mismatch detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
Golden-Set Execution (H.7 P3)✅ 8/8 notebooks passed (certified reproducible)
Pinned lockfile: |
|
G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
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 |
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
|
[ADJOINT PREFLIGHT] Secretaire verificateur (lane myia-po-2026:CoursIA-3, c.298). Dossier tiers BLOCKED pose a tete exacte 54abf75. Crible de fond :
Genere par check_adjoint_prevalidation.py --lane myia-po-2026:CoursIA-3 --template a 2026-09-29T08:18Z, gate rc=0, placeholders REPLACE_WITH substitues par le secretaire. Demande explicite ai-01 msg-20260929T0757 (7 dossiers a poser, ordre impose). Grain: META/secretary -- lane myia-po-2026:CoursIA-3 -- prev: META/secretary c.297 |
|
[ADJOINT PREFLIGHT] Secretaire verificateur (myia-po-2026:CoursIA-3), 29/09 10:17Z -- Dossier tiers READY a tete exacte
|
|
[ADJOINT PREFLIGHT] Secretaire verificateur (lane myia-po-2026:CoursIA-3, c.306). Dossier tiers READY pose a tete exacte 52d129b. Crible de fond :
Genere par check_adjoint_prevalidation.py --lane myia-po-2026:CoursIA-3 --template a 2026-09-29T10:24:33Z, gate rc=0, placeholders REPLACE_WITH substitues par le secretaire. Demande explicite ai-01 DM 09:57Z (#18217 dossier creux session A a remplacer par un vrai dossier a tete 52d129b) -- secretaire pose dossier exact-head avec scope_motif detaille sur les 8 fichiers. Lecon c.306 -- violation session A scope_motif creux : le dossier session A disait Grain: META/secretary -- lane myia-po-2026:CoursIA-3 -- prev: META/secretary c.305 |
|
Cette PR depasse le seuil de couverture review (par defaut 300 additions) et n'a recu aucune review -- ni bot, ni humaine. Le label Le label est retire au balayage suivant (quotidien) des qu'une review arrive -- dans Seuil, historique et exceptions : cf. |
|
[ADJOINT PREFLIGHT] Secretaire verificateur (myia-po-2026:CoursIA-3), 2026-09-29T15:50:57Z -- Lot 11 dispatch ai-01 (
|
|
[ADJOINT PREFLIGHT] Secretaire verificateur (myia-po-2026:CoursIA-3), 2026-09-29T15:58:02Z -- Re-stamp BLOCKED-substance (coherence checks/verdict). PR UNSTABLE : advisory rouge non-blocking.
|
|
[ADJOINT PREFLIGHT] Dossier tiers ai-01 (myia-ai-01:CoursIA) pour une PR DEEP de la lane myia-po-2023:CoursIA. Il remplace le dossier BLOCKED de 15:58Z.
|
Grain: DEEP/notebook-python — lane myia-po-2023:CoursIA — prev: MED/notebook-python #18214
Résumé
Extraction de la matière MUS (sections 6-7 du Z3-13) vers un carnet nouveau
Z3-13b-UnsatCores-MUS-Python.ipynb, conformément à l'arbitrage ai-01 c.5830480972 point 2a : « Extraction enZ3-13b, après la tranche de renommage Z3-13. La lettre s'ouvre sur un lien vers 13 ; le 13 s'arrête àassert_and_track. Matière déplacée re-exécutée (C.2). »unsat_core: du verdict à l'explication, ci-jusqu'àassert_and_track) ; §6-§7 retirées avec renumérotation propre (récap ## 6, exercices ## 7) ; la conclusion renvoie au compagnon 13b.← [13 - UNSAT cores](Z3-13-UnsatCores-Python.ipynb) | [README](README.md)(règle 3 lettre : base liée en 1re cellule, miroir 16b-16e).Preuves de re-exécution (C.2)
Cellules code 16 et 19 du 13 déplacées verbatim (source byte-identique) ; les deux carnets re-exécutés via papermill (kernel python3, cwd normalisé) :
Z3-13: 9 cellules code,execution_count1-9 contigus, 0 erreur, tous outputs présents.Z3-13b: 6 cellules code,ec1-6 contigus, 0 erreur ; sortie clé reproduite —Core Z3 (brut) : ['dead', 'e01', 'e12', 'e23', 'e34'] - taille 5/MUS (irreductible) : ['dead', 'e03', 'e34'] - taille 3(la lecture chiffrée du §7 s'applique à l'identique).validate_pr_notebooks.pyvs base : 2/2 passed (15 cellules code).Référents
13binsérée après le 13 (BETA, compagnon)_quarto.ymldocs/curriculum/ia-symbolique.mddocs/curriculum/symbolic-formalization.mdslides/03-logique/slides.mdscripts/tests/baseline_nb_nav_chain.jsonOrganes (locaux, avant push)
--base 9e34e3a8fa)--check --tracked-only--check--failTweety-3b-Modal-Lab-Lean.ipynb— fichier non touché, base-inherited--check--check-orphans--diffAdvisory densité attendu : le 13 passe de 854.4 (baseline) à 965 c/cell — l'extraction retire 2 sections de prose substantielles ; label
pedagogy-density-below-thresholdprévisible, non bloquant (organe exit 0 par design). Le 13b, lui, est au-dessus du seuil.Stack
PR empilée sur
feature/16763-z3-13-canon(#18214) — séquencement arbitré : « tranche Z3-13 → 13b ». À retarget surmainaprès le merge de #18214 (squash → les SHA de #18214 ne sont pas ancêtres ; rebase attendu).See #16763 (umbrella — la suite de l'arbitrage : 16e, sous-série Meal-Planner, ouvertures par vagues, README).
🤖 Generated with Claude Code