fix(lean,#19891-suivi): fusion R2+R3 -- cellules §3.5 et §B.3 dans lectures existantes #19935

Activity

1. jsboige

   added

   leanLean 4 formalization (proofs, ports, theorem mining)Lean 4 formalization (proofs, ports, theorem mining)

   on Oct 8, 2026
2. jsboige

   added 2 commits that reference this issue on Oct 8, 2026

   fix(lean,#19935): fusion R2 -- cellules §3.5 et §B.3 dans lectures ex…

   ...

   c1637c6

   fix(lean,#19935): fusion R2 -- cellules §3.5 et §B.3 dans lectures ex…

   ...

   f87b75c
3. jsboige commented on Oct 8, 2026

   

   jsboige

   on Oct 8, 2026

   OwnerAuthor

   More actions

   Acceptance remplie (commit f87b75c9e3 sur PR #19891) :

   • Cellule §3.5 (lecture du certificat Euler) fondue dans §3.4 (lecture de la figure), avec sous-heading « Au-delà de la figure — ce que la chaîne établit, ce qu'elle ne dit pas, sous quelles hypothèses » et conservation du tri « établit / ne dit pas / hypothèses et bornes ».
   • Cellule §B.3 (lecture du certificat NS) fondue dans §B.2 (lecture des profils), avec sous-heading « Au-delà des profils de classes — ce que les trois chaînes établissent, ce qu'elles ne disent pas, sous quelles hypothèses » et conservation du tri.
   • Plus aucune cellule « ### Lecture du résultat » ou « ### Lecture du/des certificat(s) » ajoutée en queue de run markdown existant (règle canonique Redressement campagne densité #13410 : remplissages dégénérés — 233 notebooks, 20 paquets d'audit #17040 : max 1 lecture markdown par output de code).
   • Re-exécution C.2 non requise (markdown-only, 0 cellule code touchée, 0 cellule de reproduction touchée).
   • python scripts/notebook_tools/check_split_reading_cells.py --base /tmp/lean-31-main.ipynb --head <file> --fail-on-findings → exit 0 (0 finding).

   Périmètre respecté : 1 notebook édité, 2 cellules markdown supprimées, 2 cellules markdown existantes augmentées (Euler §3.4 : 1274 → 5305 chars, NS §B.2 : 2671 → 7274 chars), IDs cellules préservés, pin 8937a8f4cbc7 et toolchain leanprover/lean4:v4.34.0-rc2 préservées.

   Issue close — la PR #19891 porte maintenant R1+R2 levées. R3 (doublons de prose) à examiner post-re-aggregation, par re-review [NanoClaw].

   -- lane myia-po-2026:CoursIA-2, c.1464 (08/10 ~17:15Z)
4. jsboige

   closed this as completedon Oct 8, 2026
5. myia-ai-01

   added a commit that references this issue on Oct 10, 2026

   feat(lean,#19884): digestion pedagogique Euler/BKM + NS C/D -- ce que…

   ...

   e46df46