enrich(smt,#13410): prose interpretative Z3-Python-12/14 (densite 759/759 -> 1318/1297) by jsboige · Pull Request #16021 · jsboige/CoursIA

jsboige · 2026-09-13T19:10:13Z

Grain: DEEP/notebook-python — lane myia-po-2026:CoursIA — prev: LIGHT/tooling #15948

Résumé

Volet SMT de la veine densité #13410 : les deux notebooks Z3 les plus bas de la
famille SymbolicAI/SMT/Z3-API passent au-dessus du plancher de 1200 caractères de
prose par cellule de code, par de la prose d'interprétation ancrée sur les sorties
réellement exécutées.

Notebook	Avant	Après	Cellules ajoutées
Z3-Python-12-Real-Arithmetic	759	1318	5
Z3-Python-14-BitVectors-Overflow	759	1297	7

Chaque cellule est placée après la cellule de code qu'elle lit, et ne dit rien que
la sortie imprimée ne montre :

Z3-Python-12 (arithmétique réelle) — la théorie se choisit à la déclaration des
variables et non à l'import (Real vs Int vs BitVec) ; x = 2 est un rationnel exact
et non un flottant, ce qui est un résultat plus fort qu'une résolution numérique ; le
? de 1.4142135623? marque un objet-racine et non un float — 1.4142135623 ** 2
vaut 1.999999999793256, donc à côté de 2 de plus de 2e-10, alors que l'objet-racine
vérifie xs * xs == 2 exactement ; unsat sur xn^2 + 1 = 0 est une preuve
d'absence et non un échec de recherche ; sur l'inégalité triangulaire, le triplet
(1, 2, 3) resterait sat parce que les inégalités sont larges — le cas dégénéré est
accepté par l'encodage.

Z3-Python-14 (bit-vectors) — Z3 reste une théorie de décision dans ce fragment ;
4 500 000 000 devient 205 032 704 (4 500 000 000 - 4 294 967 296) et c'est le
retournement du comparateur (205 032 704 < 3 000 000 000) qui fonde ULT comme
détecteur ; constater une valeur fixée n'est pas prouver sur des variables symboliques ;
le quantificateur implicite du seuil 2^31 = 2 147 483 648, moitié exacte de 2^32 ;
la même preuve retournée en garantie de sûreté (1000 + 1000 = 2000, aucune enveloppe
atteignable) ; le témoin 0xFBFF0000 = 4 227 792 896 et la contrainte n != 0 sans
laquelle le témoin aurait été trivial ; BV4 sat contre Int unsat sur le même
prédicat, ce qui est l'argument le plus net de la section.

Validation

Contrôle	Résultat
`pedagogy_density.py`	12 : 759 → 1318 ; 14 : 759 → 1297 (plancher 1200), `below_threshold: 0`
`detect_markdown_rendering.py --check`	0 violation sur les deux fichiers
`enrich_quality_ci.py --base --head`	rc=0 sur les deux
`check_null_exec.py` (H.3)	2 notebooks OK
`check_cell_source_parses.py`	0 finding
`check_prose_quantitative_claims.py --diff`	aucun compteur quantitatif en prose
`detect_repeated_prose.py`	2 → 1 finding sur le 12 : la paire intro/conclusion est préexistante (elle rougit déjà sur `origin/main`) et sa contenance baisse de 0.45 à 0.38

Édition markdown uniquement (exception C.2) : aucune cellule de code n'est touchée —
execution_count et outputs préservés. Le round-trip byte-identique a été vérifié
avant édition sur les deux fichiers (json.dumps(ensure_ascii=False, indent=1) +
newline final) ; le diff est en insertions pures : 240 ajouts, 0 suppression, donc
aucune cellule existante n'a été réécrite.

Pas d'obligation jumeau : les entrées twin_pairs.d de la famille Z3 s'arrêtent à
01-06, et 12/14 n'ont pas de frère -Csharp sur disque.

Préflight collision : seule PR ouverte touchant SMT/Z3-API = #15795
(Z3-Python-03-Tactics) — recouvrement de fichiers nul.

Tous les chiffres cités sont soit lus sur la sortie de la cellule interprétée, soit
recalculés avant écriture (1.4142135623 ** 2, 4 500 000 000 - 2**32, 0xFBFF0000).

See #13410 (contribution partielle : 2 des notebooks sous plancher ; le tracker reste ouvert pour la surface restante)

🤖 Generated with Claude Code

…/759 -> 1318/1297) Sous-grain densite de #13410 : les deux notebooks Z3 les plus bas de la famille SymbolicAI/SMT passent au-dessus du plancher par de la prose ancree sur leurs sorties reellement executees. Z3-Python-12-Real-Arithmetic, 5 cellules : la theorie se choisit a la declaration et non a l'import ; x=2 est un rationnel exact et non un flottant ; le '?' de 1.4142135623? marque un root-obj et non un float (1.4142135623**2 = 1.999999999793256, donc a cote de 2 de plus de 2e-10) ; unsat comme preuve d'absence et non comme echec de recherche ; inegalite triangulaire, ou (1,2,3) reste sat par inegalites larges. Z3-Python-14-BitVectors-Overflow, 7 cellules : theorie de decision et non approximation ; 4 500 000 000 -> 205 032 704 et le retournement du comparateur qui fonde ULT ; constater n'est pas prouver ; le quantificateur implicite du seuil 2^31 ; la meme preuve retournee en garantie de surete ; le temoin 0xFBFF0000 et la contrainte n != 0 sans laquelle le temoin serait trivial ; BV4 sat contre Int unsat sur le meme predicat. Edition markdown uniquement (exception C.2) : les cellules code sont intactes, execution_count et outputs preserves -- round-trip byte-identique verifie AVANT edition sur les deux fichiers (json.dumps ensure_ascii=False indent=1). Le diff est en insertions pures, 240 lignes ajoutees et 0 supprimee. Mesures - pedagogy_density : 12 = 759 -> 1318 ; 14 = 759 -> 1297 (plancher 1200), 2/2 ok - pas d'obligation jumeau : les entrees twin_pairs.d de la famille Z3 s'arretent a 01-06, et 12/14 n'ont pas de frere -Csharp sur disque - gardes : detect_markdown_rendering 0 violation ; enrich_quality_ci rc=0 ; check_null_exec OK ; check_cell_source_parses 0 finding ; compteurs en prose OK ; detect_repeated_prose passe de 2 a 1 finding sur le 12 (paire intro/conclusion preexistante, contenance 0.45 -> 0.38) See #13410 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

github-actions · 2026-09-13T19:10:37Z

⚠️ 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 · 2026-09-13T19:11:00Z

Notebook PR Validation: PASS

Notebooks checked: 2
Code cells validated: 18
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 · 2026-09-13T19:11:02Z

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	2.7s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.1s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	3.3s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	3.2s
Search-01-StateSpace.ipynb	✅ SUCCESS	2.6s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	1.8s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	15.8s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.4s

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

github-actions · 2026-09-13T19:11:56Z

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

…uctural fold (#16112) The existing organ (#15901) measures source VOLUME. A cell whose source folds entirely into a comment is invisible to it by construction: on the founding case (PR #16097, Lean-18 cell 40cb37d5) the head GROWS 1132 -> 1728 chars because the same write that stripped the newlines appended a 639-char recovery note, so the magnitude gate stops before any floor. The BLOCKING notebook-cell-source-parses guard is blind too -- a fully commented cell parses clean -- which is why it stayed green on a cell whose code had disappeared. Adds two structural signals to the SAME check-run, no new fast-lane wiring: * `emptied` matched cell whose statement count went from > 0 to 0. * `orphan-output` non-empty outputs with 0 statements and no IPython magic (base-free by construction -- the issue's 3rd criterion). The existing exemptions speak about the base->head RELATION, so they arbitrate the comparative signal only; `orphan-output` is intra-cell and stays true whatever happens to the code elsewhere. Both exemption fractions measure 0.00 on the founding case, so nothing was suppressed. `_scan_line` / `_strip_ipython_magics` / `_is_python_kernel` are imported from check_cell_source_parses rather than reimplemented, so the organs cannot disagree about the same cell. Criterion 1 of the issue (unterminated-item count) is REFUTED by measurement, not implemented: per-character serialization already exists on main (GenAI/Texte/21_LoRA_FineTuning.ipynb cell 69b296cb -> 802 unterminated items, 10 statements, real output, healthy). Histogram over the 11970 code cells of main's 953 Python notebooks: {0: 11970, 1: 1, 802: 1}. The signal is withdrawn rather than shipped with a threshold; the folds it targeted are covered twice without it (code-first fold -> the blocking syntax guard; comment-first fold -> `emptied`). Calibration: 0 structural findings on main's full Python corpus; 0 structural findings on the 18 notebooks changed by 12 merged PRs (#16080, #16071, #16069, #16067, #16041, #16039, #16027, #16024, #16021, #16020, #16013, #16012). A first sweep without the no-magic guard flagged 6 cells, all `# comment` + `!python`/`%pip` -- the magic IS the producer, so the guard is measured necessity, not caution. Evidence: 30 tests green in the file, 89 across the sibling organ files; `--self-test` OK with BOTH founding-case replays firing (volume #15901 and structure #16110); live end-to-end run at #16097's head reports the exact measured finding with RC=1. Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>

… only Les tranches de densite (#16007, #16012, #16021, #16343, #16352) ne touchent jamais la baseline : elle est un snapshot Phase-1 ("burn down, do not grow"), ses valeurs ne se retro-fitent pas. Restauration de la version main. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

Les tranches de densite (#16007, #16012, #16021, #16343, #16352) ne touchent jamais la baseline : elle est un snapshot Phase-1 ("burn down, do not grow"), ses valeurs ne se retro-fitent pas. Restauration de la version main. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…ML-2/ML-3 Python (#16381) * enrich(mlnet,#13410): tranche densite fondations scikit-learn ML-1/2/3 Python ML-1 753->1209 (graine, lecture des 4 points, coefficients OLS, jeu de test extrapolation, interpolation vs extrapolation, graphique, perfection 100% comme signal d'alerte, grammaire commune). ML-2 957->1231 (describe, expansion one-hot 7->9, R2=1.0 sur-apprentissage). ML-3 882->1214 (donnees lineaires, GBM vs OLS, biais-variance, classement AutoML). Markdown uniquement (exception C.2), baseline scoped 3 cles. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * revert(mlnet,#13410): baseline edits — canon des tranches = notebooks only Les tranches de densite (#16007, #16012, #16021, #16343, #16352) ne touchent jamais la baseline : elle est un snapshot Phase-1 ("burn down, do not grow"), ses valeurs ne se retro-fitent pas. Restauration de la version main. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(16381): rebaseline twin pairs ml-1/ml-2/ml-3 after markdown-only density tranche Pairs attested: ML-1 Introduction, ML-2 Data&Features, ML-3 Entrainement&AutoML (ML.NET/Python family). Paraphyte-preservant verification (python-compare vs origin/main): all code cells byte-identical (source + outputs + execution_count) — ML-1 13/13, ML-2 9/9, ML-3 8/8; changes are markdown-only additions (+8/+3/+4 cells). Command run per pair: python scripts/notebook_tools/check_twin_parity.py --update --pair "<name>" --by "myia-po-2026:CoursIA" Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(ml,#16381): aligner moyennes 1 434 s / 4,4 km sur describe 1433.57 / 4.4125 Markdown-only fix (pas de re-exec, pas de cellule code touché) : - moyennes : 1 722 s et 4,8 km -> 1 434 s et 4,4 km (arrondi describe) - ecart-type : ~1 000 s -> ~958 s (aligne sur cellule describe plus haut) Source de verite : cellule C describe 7.000000 8.000000 7.000000 8.000000 mean 1.428571 1.875000 1433.571429 4.412500 Tells : c.1175-L1 (markdown-only PR diff, pas hand-edit d'output) + c.564 strict reponse nominative observation adjoint c.661 + c.974 strict 1 amend/cycle. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(ml,#16381): rebaseline twin pair ML-2 Data&Features post-markdown drift fix Suite au drift introduit par mon precedent commit `6f19facb2` (markdown 1 434s/4,4km aligne describe), le registre `twin_pairs.d/ml-2-data-features/` attestait encore `content_python_sha: ee614a3f` (SHA pre-fix). Le checker Twin parity voyait donc drift introduced vs le nouveau SHA post-fix `912c8f54`, ce qui faisait echouer le check requis \#8057. Nouvelle attestation YAML `0006-2026-09-18-myia-po-2026-CoursIA.yaml` : - python_sha: 9f0afcb - content_python_sha: 912c8f5490cb747d648bafa4f3a29b486974bb09dbec0b16ba5c2528ef00cad0 Fix substance : drift elimine (1 drift remaining = GameTheory-4c NashExistence = DRIFT PRE-EXISTING non lie a cette PR cf rapport CI `drift_introduced: 0 / drift_pre_existing: 1`). Tells : c.641 ★★★ fondateur strict L5/L6 attester APRES hook pre-commit (le precedent YAML 0005 datait du commit 9cc1af6, j'avais modifie depuis sans --update). c.974 strict 1 amend/PR (substance uniquement, pas body PR cette fois). Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(ml,#16381): clarifier vendor_id/payment_type dtype str (pandas 2.x) Suite revue ai-01 c.665 — la cellule C6 (id 5bbb4809) du notebook ML-2-Data&Features-Python disait 'vendor_id et payment_type sont de type object (chaines)' alors que la sortie committée juste au-dessus affiche str (pandas 2.x). Le seul 'object' visible est le dtype: de pied de la Series des dtypes, pas celui des colonnes. Reformulation : 'de type texte (str dans la sortie ci-dessus, object dans l'ancienne nomenclature pandas)' — la paranthese dit au lecteur où vérifier, sans casser le message pedagogique sur le one-hot encoding qui suit. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(ml,#16381): re-attester twin pair ML-2 post dtype str fix Suite rebase-arm-DWELL c.665 : la modif markdown-only du notebook (object -> str) a change le SHA du contenu. Tell c.641 ★★★ re-attestation twin parity AFTER hook pre-commit. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>

…ncement / 09-Einstein / 10-Cryptarithmetic (#16379) * enrich(z3,#13410): tranche densite SMT - lectures mesurees 08/09/10 08-Ordonnancement 735->1267 (NP-difficulte + bornes, anatomie du modele 7 vars / 6 disjonctives, lecture glouton 14h vs optimal 8h, lecture Gantt). 09-Einstein 1115->1228 (verification du temoin : 4 indices relus). 10-Cryptarithmetic 879->1290 (anatomie des retenues contre la solution, temoin vs preuve, lecture DANGER). Markdown uniquement (exception C.2), baseline scoped 3 cles. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * revert(z3,#13410): baseline edits — canon des tranches = notebooks only Les tranches de densite (#16007, #16012, #16021, #16343, #16352) ne touchent jamais la baseline : elle est un snapshot Phase-1 ("burn down, do not grow"), ses valeurs ne se retro-fitent pas. Restauration de la version main. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(z3,#13410): repositionne 2 cellules Interpretation apres leur code (check_interp_positioning) Einstein cell#7 et Cryptarithmetic cell#5 etaient parachutees entre deux headers, sans code au-dessus dans leur section (incident PyMC-15 #10580). Deplacees juste apres le code qu'elles interpretent (l'affichage du modele / le solveur SEND+MORE) : sources inchangees, ordre seul, outputs intacts. check_interp_positioning --check : OK repo-wide. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>

jsboige merged commit 1661db9 into main Sep 13, 2026
77 of 78 checks passed

myia-ai-01 mentioned this pull request Sep 14, 2026

merge_dwell: le message tait le declencheur 'push' du balayage et fait craindre une heure d'attente la ou la mediane est de 8 min #16092

Closed

jsboige mentioned this pull request Sep 14, 2026

fix(nb-tools,#16110): source-collapse ratchet — second mechanism, structural fold #16112

Merged

jsboige mentioned this pull request Sep 16, 2026

enrich(z3,#13410): tranche densite SMT — lectures mesurees 08-Ordonnancement / 09-Einstein / 10-Cryptarithmetic #16379

Merged

jsboige mentioned this pull request Sep 20, 2026

fix(density,#17040): redressement paquet P18 — SMT/Z3-API + SemanticWeb #17059

Merged

Navigation Menu

Repository navigation

enrich(smt,#13410): prose interpretative Z3-Python-12/14 (densite 759/759 -> 1318/1297) - #16021

enrich(smt,#13410): prose interpretative Z3-Python-12/14 (densite 759/759 -> 1318/1297)#16021
jsboige merged 1 commit into
mainfrom
feature/densite-13410-z3-arithmetique-bits

jsboige commented Sep 13, 2026

Uh oh!

github-actions Bot commented Sep 13, 2026

Uh oh!

github-actions Bot commented Sep 13, 2026

Uh oh!

github-actions Bot commented Sep 13, 2026

Uh oh!

github-actions Bot commented Sep 13, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

jsboige commented Sep 13, 2026

Résumé

Validation

Uh oh!

github-actions Bot commented Sep 13, 2026

Uh oh!

github-actions Bot commented Sep 13, 2026

Notebook PR Validation: PASS

Uh oh!

github-actions Bot commented Sep 13, 2026

Golden-Set Execution (H.7 P3)

Uh oh!

github-actions Bot commented Sep 13, 2026

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

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

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