Add: Lean-17c section 6 — visibilité des trois modules sombres de knot_lean (#11703)

[jsboige]

Grain: MED/notebook-lean -- lane myia-po-2027:CoursIA -- prev: LIGHT/docs #18912

Ce que fait cette PR

Sous-grain de l'EPIC #11703 (visibilité du corpus Lean dans les notebooks) : le lake knot_lean portait 3 modules sombres — zéro déclaration citée dans aucun notebook : ReidemeisterMoves.lean, ReidemeisterCombinatorial.lean, FigureEight.lean. Cette PR étend le compagnon existant Lean-17c-Knots-Companion-Formel.ipynb (kernel python3, lecture pathlib du lake, aucun build Lean requis) d'une section 6 (10 cellules : intro + 3 x [contexte, code, lecture du résultat]) qui les couvre :

• 6.1 ReidemeisterMoves.lean — la relation de moves comme type inductif : listing des 31 déclarations + signatures de SameRelOn, RefinesOn et l'inductif ReidemeisterMove (constructeurs r1/r2/r3 avec leurs docstrings).
• 6.2 ReidemeisterCombinatorial.lean — le vérificateur décidable : 10 déclarations + MoveSequence (suite inductive typée par les diagrammes source/cible), verifyMoves et verifyMoves_sound.
• 6.3 FigureEight.lean — le nœud en huit : 12 déclarations + alexander_figureEightPlanar_classical (existence k, ε avec ε² = 1), _signed_mirror, figureEightPlanarDiagram_not_tricolorable.

Les sections 6→8 existantes sont renumérotées 7→9.

Détail technique : le DECL_RE local du compagnon (§2) omettait inductive — les deux types structurants de la nouvelle section en sont. La section 6 définit donc un jeu large DECL_WIDE (inductive/class/opaque inclus), aligné sur l'extracteur de l'organe de visibilité ; le DECL_RE de la §2 (utilisé par le tableau de bord du lake) est inchangé.

Preuves

• Exécution réelle : python -m papermill Lean-17c-Knots-Companion-Formel.ipynb … --kernel python3 --cwd . → 43/43 cellules, 0 erreur, execution_count partout, outputs committés (C.2). Le notebook modifié est le seul fichier du diff (C.3).
• Métrique avant/après (scripts/lean/scan_lake_notebook_visibility.py, runs locaux des deux côtés) :

Mesure	avant	après
knot_lean modules sombres	3/12	0/12
citations large (déclarations)	96	147
citations strict	83	127
total repo modules sombres	39/294	36/294

• Pas de build Lean requis : le compagnon lit les fichiers du lake par pathlib (cwd = dossier série) ; aucune preuve n'est modifiée (diff = 1 notebook, insertions seulement hors renumérotation).

Scope résiduel de l'EPIC (non couvert ici)

36 modules sombres restent sur les autres lakes (grothendieck_lean 16, conway_lean 4, …) — la PR est un sous-grain, See #11703, pas une clôture.

See #11703

🤖 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 unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

[github-actions]

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

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

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

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.6s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.6s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.9s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.5s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.4s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.5s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	17.5s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.6s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	10.8s

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: 14
• 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: 18925
head: b9dffd2
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: dc7a588d6f72939b8c4389fb4a5fac074ebb5c0591df97a4ec2257bce12e6657
diff-files: 1
diff-additions: 745
diff-deletions: 241
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

note: Dossier c377 sur PR #18925 (Add: Lean-17c section 6 — visibilité des trois modules sombres de knot_lean). Lane porteuse myia-po-2027:CoursIA. MED/notebook-lean, 1 fichier MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17c-Knots-Companion-Formel.ipynb +745/-241. Sous-grain de l'EPIC #11703 (visibilité du corpus Lean dans les notebooks) : couvre 3 modules sombres de knot_lean -- ReidemeisterMoves.lean, ReidemeisterCombinatorial.lean, FigureEight.lean -- via une section 6 (10 cellules : intro + 3 x [contexte, code, lecture du résultat]). Compagnon kernel python3 (lecture pathlib du lake, aucun build Lean requis). Item 16 du skill : la PR ne touche pas de .lean (que du .ipynb), donc les lignes B.1-B.3 (sorry counter, lake build) sont N/A. Crible de fond : base 33 cellules (11 code/22 md, 9 outputs, exec_count 11/11) -> head 43 cellules (14 code/29 md, 12 outputs, exec_count 14/14). +10 cellules = 3 sous-sections (intro + 3x3), +3 outputs, 0 marqueur de dégradation. PR gate vert : re-run de c376 SUCCESS @ 02:40:45Z (la cause redevenue verte a été re-agrégée). B.0 OK (aucun nit non levé, 7 commentaires tous github-actions informatifs). Scope pass (1 fichier .ipynb sous SymbolicAI/Lean/, pas sous .claude/ ni .github/). domain: pass (substance notebook vérifiable : 3 sections context+code+lecture, introductive+explicative). 0 review formelle (pas d'APPROVED Hermes, pas d'APPROVED ai-01). Lane porteuse po-2027:CoursIA (DIFF de ma lane po-2026:CoursIA-3, tiers autorisé). merge_ready exigera une APPROVED d'ai-01 pour exécuter. ai-01 may merge direct. Eligible READY.