enrich(notebooks,#13410): Z3-Python-05 C# twin -- densite 622 -> 1490 c/cell

[jsboige]

Grain: MED/notebook-dotnet — lane myia-po-2026:CoursIA-2 — prev: MED/genai #14593

See #13410

Summary

Enrichissement markdown-only du twin C# de Z3-Python-05-Quantifiers-Proofs
(SymbolicAI/SMT/Z3-API/Z3-Python-05-Quantifiers-Proofs-Csharp.ipynb), qui était sous le
plancher pédagogique de densité (622 c/cell contre 1200).

Ce que la PR apporte (prose pédagogique, aucune cellule code modifiée) :

1. Objectifs d'apprentissage + table de la refutation dans l'intro (le parcours
   vaut pour toutes les sections : nier, checker, conclure sur le statut).
2. 8 cellules d'interprétation ### Lecture du résultat, une par section de preuve,
   chacune insérée immédiatement après sa cellule code et citant la sortie réelle
   de cette cellule (identité additive, trois théorèmes, x*x==4, carré négatif,
   trichotomie/monotonie, non-borne des réels, UNKNOWN Fermat, minorant x=0).
3. Intros de section étoffées : l'énoncé mathématique, le pattern cognitif
   (preuve par refutation), et pourquoi Z3 décide sans énumération.

Preuves

• Densité pédagogique : 622 -> 1490 c/cell (mesuré
  pedagogy_density.py --json, prose_chars 19369 / 13 code cells, below_threshold: 0).
• Markdown-only (C.2, pas de re-exec) : les 13 cellules code sont byte-identiques
  à main (vérifié par comparaison source+execution_count de chaque cellule code) ;
  seuls les md changent. Les sorties réelles de Z3 sont préservées telles quelles.
• Pre-commit : tous les hooks passés — gitleaks, strip probe banner,
  H.3 check_null_exec (toutes les cellules code ont execution_count int + outputs),
  check_cell_source_parses.
• Position des interprétations : chaque ### Lecture du résultat suit
  immédiatement la cellule code dont la sortie est citée (vérifié à l'œil, cellules
  [4]→[3], [7]→[6], [10]→[9], ..., [25]→[24]).

Résidual (pré-existant, non introduit)

detect_consecutive_code_cells signale un run de 3 cellules code consécutives dans le
bloc ## Exercices (les 3 stubs // EXERCICE 1/2/3). C'est un groupe cohérent
(feuille d'exercices), déjà présent sur main avant cette PR — non couvert par le
scope densité, laissé tel quel.

Fonctionnement du parcours enrichi

Le notebook passe de « on demande un verdict » (une sortie par section) à « on lit le
verdict APRÈS avoir vu la sortie » : l'étudiant voit d'abord Z3 trancher, puis une
lecture expliquant pourquoi (UNSATISFIABLE = valide, skolemisation pour exhiber un
témoin, UNKNOWN = limite de solveur). C'est le pendant C# du twin Python déjà à 2418.

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

Notebook PR Validation: PASS

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

prev: genre mots-clé fermant -- bloquant (#10093).

prev: reference(s) fail invariant(s) (prev-not-merged -> [14924]) -> point prev: at a MERGED PR of the same lane, distinct from the current PR. See #13475.

Une prev: dont le genre est fix/close/resolve (ou une inflexion) fait que GitHub interprète <genre> #N comme un ordre de fermeture automatique dès que le texte atterrit dans un message de commit -- c'est exactement ce qui a fermé #10067 (sans la merger) au squash-merge de #10063. Les 14 genres canoniques ne contiennent AUCUN mot-clé fermant : utilisez refactor, guard, ou tooling à la place.

Pour passer ce gate, réécrivez le champ prev: (dans le body ET dans chaque commit concerné) avec un genre non-fermant :

Grain: <TIER>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<refactor|guard|tooling|...> #<PR>

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	22.5s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	27.9s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	211.1s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	23.9s
Search-01-StateSpace.ipynb	✅ SUCCESS	7.8s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	7.0s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	34.4s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	6.5s

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

[jsboige]

[Hermes] Vérifié par comparaison programmatique main vs head (contrainte token : COMMENT only, opener jsboige).

J'ai téléchargé le notebook aux deux refs et comparé cellule par cellule :

• 13/13 cellules code byte-identiques (source + execution_count + outputs) ✓ — le claim « markdown-only, pas de re-exec » est exact.
• Exec counts 1→13 séquentiels, kernelspec .net-csharp, sorties Z3 réelles préservées (Z3 4.12.2).
• 8 cellules « Lecture du résultat » cross-checkées contre les sorties réelles : chaque verdict cité (UNSATISFIABLE/SATISFIABLE/UNKNOWN/VALIDE) apparaît dans la sortie de la cellule adjacente — y compris le cas Fermat où le tableau des 3 statuts n'est que glossaire, la citation factuelle (UNKNOWN, timeout) est conforme à la sortie ✓.
• Densité recalculée : 19369 chars prose / 13 code cells = 1489 c/cell — conforme au claim 1490 ✓.
• Rebaseline twin_pairs : SHAs Python/C# + raison documentée, prev #14593 MERGED ✓. Security scan : clean.

Enrichissement pédagogique propre, outputs authentiques. RAS.