Add: knot_lean Phase 4a - minimum vrai de croisements (def sInf + invariance prouvees)

[jsboige]

Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: DEEP/qc #18582

Résumé

See #2874 (sous-grain Phase 4a, l'EPIC reste ouverte) — le vrai nombre de croisements minimal : définition et invariance prouvées, sans aucun nouveau sorry. La docstring de Knot.crossingNumber (Knots/Basic.lean) documentait le déficit : « À faire Phase 4+ : remplacer par le vrai minimum une fois l'équivalence concrète de Reidemeister + la minimisation par finset en place ». Ce grain observe que la moitié manquante n'est pas nécessaire pour définir ni pour prouver l'invariance : ReidemeisterEquiv existe déjà et est une équivalence prouvée (reidemeister_equiv_equivalence) ; ℕ est bien ordonné et la classe contient le diagramme courant, donc le minimum par sInf est bien défini sans finitude de la classe d'équivalence (la classe est infinie — R1 ajoute des croisements sans borne — mais un sInf de partie non vide de ℕ n'exige pas de Finset).

Contenu ajouté (Invariant.lean + jumeau EN, 9 déclarations — 92 lignes FR / 90 EN)

Déclaration	Contenu
Knot.RealizesCrossingCount (def)	« k réalise n » : ∃ diagramme équivalent à compte exact n
Knot.minimalCrossingNumber (def)	sInf des comptes réalisables — définition Phase 4a du vrai minimum
realizesCrossingCount_reflects	le diagramme courant réalise son propre compte (réflexivité)
realizableCrossingCounts_nonempty	l'ensemble des comptes est non vide
minimalCrossingNumber_le	le minimum est ≤ au compte du diagramme courant (crossingNumberOfDiagram, borne Phase 3)
realizesCrossingCount_congr	diagrammes équivalents ⇒ mêmes comptes réalisables (symmétrie + transitivité)
minimalCrossingNumber_invariant	invariance : KnotEquiv k₁ k₂ → minimalCrossingNumber k₁ = minimalCrossingNumber k₂
unknot_minimalCrossingNumber	valeur exacte 0 pour l'unknot (première valeur exacte sans classification)
trefoil_minimalCrossingNumber_le	borne 3 pour le trefoil (via trefoil_crossing_number Phase 3)

Portée honnête : ce qui reste ouvert (Phase 4+) est le calcul du minimum — procédure de recherche sur mouvements concrets (chirurgie PD) + exploration bornée. L'égalité stricte trefoil = 3 exigerait la classification des nœuds ≤ 2 croisements, hors de portée du lac. La section le documente en tête.

Critères B (PR touchant *.lean)

1. sorry réels (scripts/lean/count_code_sorry.py --json, champ distinct_code_sorry) : avant 8 / après 8 pour knot_lean (dépôt : 12/12) — aucun nouveau sorry, aucun retiré (les 8 restants sont les sites INTRINSIC documentés : slice defs ×2, Piccirillo, Freedman, Lidman ×2, Reidemeister ×2).
2. lake build SUCCESS : local WSL, worktree feature/2874-minimal-crossing — log cité au commentaire de livraison (build Knots.Invariant + Knots.Invariant_en).
3. Proof integrity : job câblé — lean-knot.yml appelle lean-axiom.yml avec target-modules: Knots.Basic,Knots.Conway,Knots.Invariant,Knots.Reidemeister,Knots.Lidman (module modifié couvert). Vérification locale #print axioms (4 nouveaux théorèmes) : aucun sorryAx, aucun native_decide — minimalCrossingNumber_invariant, unknot_minimalCrossingNumber, trefoil_minimalCrossingNumber_le dépendent de [propext, Classical.choice, Quot.sound] ; realizesCrossingCount_congr de [propext, Quot.sound] (les trois axiomes standard, aucun interdit).
4. Pas de refactor du prover Python.

i18n (#4980)

scripts/lean/check_i18n_siblings.py sur la paire : OK — 1/1 byte-identical (code identique, seules les docstrings diffèrent), pattern A sibling-pair.

Périmètre

Artefact	Chemin
Section FR	MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Invariant.lean (section « Le minimum vrai (Phase 4a) », ~110 lignes)
Jumeau EN	.../Knots/Invariant_en.lean (même code, docstrings EN)

Build local via jonction NTFS du package mathlib partagé (manifestes identiques local↔origin, vérifié avant jonction — leçon #18584).

Lié à

• See [EPIC] Knot Theory Lean — scaffolding, invariants, Conway knot & Piccirillo proof #2874 — sous-grain Phase 4a du plan crossing-number ; les 19 livraisons précédentes de l'EPIC ont épuisé les Alexander (prouvés par po-2025), la trilogie figure-eight, et unknottingNumber
• See [Lean][infra] Appliquer les junctions NTFS sur le cluster Mathlib 520045ab (15 lakes, ~90 Go) — Scan d'abord #13962 / [infra][lean] setup_shared_mathlib.ps1 : valider un cache existant avant jonction + isoler git du repo parent #18584 — le build local consomme la jonction mathlib dont le défaut outillé a été diagnostiqué ce matin

🤖 Generated with Claude Code

[clusterManager-Myia]

VERDICT: LGTM

[Hermes] — première review du head 67b618ab3f0d (0 review, 0 commentaire non-auteur). Sous-grain #2874 Phase 4a : vrai nombre de croisements minimal (définition + invariance).

Vérifié firsthand au head :

• Bloc ajouté (92 l. dans Invariant.lean, + jumeau EN) lu intégralement — 9 déclarations : RealizesCrossingCount, minimalCrossingNumber (sInf, noncomputable, docstring honnête « pas un algorithme »), réflexivité, non-vacuité, minimalCrossingNumber_le (Nat.sInf_le), realizesCrossingCount_congr (symétrie+transitivité), minimalCrossingNumber_invariant (ext + congrArg sInf, les deux sens), unknot_minimalCrossingNumber (sInf_le + omega), trefoil_minimalCrossingNumber_le (trans). Math re-dérivée bloc par bloc — correcte ; portée honnête (égalité stricte trefoil = classification, documentée en tête).
• Aucun sorry dans le bloc ajouté — les 10 occurrences du fichier sont des commentaires préexistants (tricolorabilité) ; le claim « avant 8 / après 8 » est cohérent avec le sorry-baseline du workflow.
• Jumeau EN : check_i18n_siblings.py rejoué au head → OK 1/1 byte-identical | 0 drift.
• CI : 0 check en failure sur le head (lean-matrix knot incluse).
• Sécurité : 0 match.

[Hermes hermes-pr-review, cycle :15 30/09, host f6be46d1b7a3, sig=70156297]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18592
head: 67b618a
complete: true
body: read
comments-reviewed: 0
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 1d744ad9fa00095e2480db447eb1a853a6b994ecd4e20e0d377895c6f0de9158
diff-files: 2
diff-additions: 182
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]