feat(lean,#2874): preuves kernel conway+KT — maison-mère du split 4 unités (#15434 ✓, #15440, #15460 ✓, #15583)

.github/workflows/lean-knot.yml

@@ -46,15 +46,18 @@ name: Lean Knot CI
 #   - Reidemeister.lean:        2 (reidemeister_theorem x2 — PL topology, OOS)
 #   - Basic.lean:               0 (the "1" under prose-header was a TODO prose comment)
 #   - MathlibPrerequisites.lean:0 (the "2" were the prose roadmap index)
-# Total real tactic sorry = 11 (aligné avec `LEAN_INVENTORY.md` post-#13312,
+# Total real tactic sorry = 9 (aligné avec `LEAN_INVENTORY.md` post-#13312,
 # mesure 2026-08-28 `count_code_sorry.py` champ `distinct_code_sorry` ; lowered
 # from 14 par la mesure instrument post-#11227 — le décompte « 14 » dans les
 # commentaires/README comptait 2 sorry dans `Invariant.lean` qui n'en portent
 # qu'1 une fois stripé des commentaires, et sur-comptait Conway ; historique :
 # 16 (après #8766) → 17 (#9966 wall fronted) → 16 (wall DISCHARGED) → 14
-# (#11211/#11227 fox/col) → **11** (mesure 2026-08-28, `count_code_sorry.py`).
+# (#11211/#11227 fox/col) → **11** (mesure 2026-08-28, `count_code_sorry.py`)
+# → **10** (2026-09-05, `conway_trivial_alexander` DISCHARGED — preuve kernel
+# déterminant 10×10 en ℤ[t], See #2874) → **9** (2026-09-06,
+# `KT_trivial_alexander` DISCHARGED — mineur t⁵ par transvections, See #2874).
 # Cette valeur DOIT rester synchronisée avec `LEAN_INVENTORY.md` ligne « knot_lean
-# | 11² » et avec `knot_lean/README.md` table des sorries — cf. #13312).
+# | 9² » et avec `knot_lean/README.md` table des sorries — cf. #13312).
 # Raising this baseline requires a documented
 # justification in the PR body (a NEW real tactic sorry, not prose).
 
@@ -148,7 +151,14 @@ jobs:
         with:
           project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean
           display-name: knot_lean
-          sorry-baseline: "10"
+          # 11 -> 10 : conway_trivial_alexander decharge (See #2874, preuve
+          # kernel determinant 10x10, Conway.lean 6 -> 5 sorries reels).
+          # 10 -> 9 : KT_trivial_alexander decharge (See #2874, mineur t^5
+          # par transvections, Conway.lean 5 -> 4 sorries reels).
+          # 9 -> 8 : fusion main -- unknottingNumber decharge sur main par
+          # #15082 (Invariant.lean) ; les stubs CTA/KT de main sont
+          # remplaces par les preuves completes ci-dessus.
+          sorry-baseline: "8"
           sorry-filter-mode: real
           # #14821 : le pool coursia-lean OOM-kill (exit 137) sur le pic
           # d'elaboration des siblings Conway/Conway_en DANS le meme job —
@@ -192,7 +202,7 @@ jobs:
           display-name: knot_lean
           target-modules: "*"
           allow-axioms: ""
-          # 10 acknowledged tactic `sorry`s = the `sorry-baseline` declared by the
+          # 8 acknowledged tactic `sorry`s = the `sorry-baseline` declared by the
           # build job above; the gate tolerates them (`fail-on-sorry: false`) but
           # still reports `has_sorry` per module and hard-fails forbidden axioms.
           # The per-module enumeration now lives in the gate's runtime derivation

MyIA.AI.Notebooks/SymbolicAI/Lean/LEAN_INVENTORY.md

@@ -24,7 +24,7 @@ FLT/pin Mathlib `db584cd`, même forme CI dispatcher que hecke).
 |------|-----------|--------------------:|--------------:|---------------:|--------|-------|
 | `grothendieck_lean` | v4.32.1 | 0 | 118 | 4 | REF | #1646, #2159 |
 | `conway_lean` | v4.32.1 | 1¹ | 72 | 23 | PEDA | #1453, #1651, #2162 |
-| `knot_lean` | v4.32.1 | 10² | 15 | 4 | PEDA/REF | #2874, #3003, #14821 |
+| `knot_lean` | v4.32.1 | 8² | 15 | 4 | PEDA/REF | #2874, #3003, #14821 |
 | `finiteness_lean` | v4.32.1 | 0 | 4 | 4 | PEDA | #2978, #3111 |
 | `sensitivity_lean` | v4.32.1 | 0 | 11 | 5 | PEDA/REF | famille calibration |
 | `mimo_lean` | v4.32.1 | 0 | 13 | 3 | PEDA/REF | #10984, #10986 |
@@ -43,28 +43,25 @@ FLT/pin Mathlib `db584cd`, même forme CI dispatcher que hecke).
 ont été closes** (P4 décomposé en `p4_double_nine_shape` / `p4_wave1_ih` / `p4_wave2_ih`
 sorry-free, vérifié par `lake build Conway.Life` post-#4780), seule `HashlifeCorrectness`
 reste en cible prover. Régression de compte documentée et HONNÊTE — pas un défaut.
-² `knot_lean` = **research-HOLD** : théorie des nœuds (#2874). Compte **mesuré sur `origin/main`
-le 2026-09-11** : **10 distincts** (`count_code_sorry.py --json`, champ `distinct_code_sorry`),
-soit `0 (Basic) + 2 (Reidemeister) + 0 (Invariant, post-#15082) + 6 (Conway) + 2 (Lidman)
-+ 0 (Mathlib) = 10`. La baseline CI `lean-knot.yml` porte la même valeur (`sorry-baseline: "10"`).
-La majorité des 10 restants sont des **définitions non définies** (`IsSmoothlySlice`,
-`IsTopologicallySlice := sorry`, etc.) et des preuves de transfert classique ouvertes.
-Le pont GF(3) Path B (`triColorFoxCondition_iff_sum_mod_three`) est **prouvé** (#3003,
-sorry net-zéro vs `main`) et `trefoil_not_unknot` **prouvé** (#8766). Niveau recherche, pas un
-gap pédagogique.
-
-**Évolution documentée** (3 → 12 → 11 → 10) — n'est PAS une régression silencieuse :
-- **3** (inventaire 2026-07-15) → **12** (2026-08-27, montée initiale recherche HOLD)
-- **12 → 11** (2026-08-28, #8766 `trefoil_not_unknot` + #11227 `fox`/`col` §9.1)
-- **11 → 10** (2026-09-09, #15082 `unknottingNumber` par `Nat.sInf`, baseline CI recalibrée)
-
-**Trajectoire à venir** — `10 → 9` par #15440 (`conway_trivial_alexander`, unité 2 du split
-#14821) puis `9 → 8` par #15460 (`KT_trivial_alexander`, unité 3). Ces deux PRs portent
-elles-mêmes la recalibration `10 → 9 → 8` de la baseline CI dans `lean-knot.yml`.
-
-Cette unité 4 synchronise la présente table et `knot_lean/README.md` sur l'état **mesuré à
-date**, pas sur l'état projeté : les deux fichiers restent ainsi vrais quel que soit l'ordre de
-merge vis-à-vis de #15440/#15460. Cf. `knot_lean/README.md` pour la trace par fichier.
+² `knot_lean` = **research-HOLD** : théorie des nœuds (#2874). Le compte **est monté** de
+3 (inventaire 2026-07-15) à 12 distincts (inventaire 2026-08-27), puis rebaissé à
+**11 distincts actuels (mesure 2026-08-28, `count_code_sorry.py` distinct_code_sorry)**
+— la majorité des 11 sont des **définitions non définies** (`AreMutants`,
+`alexanderPolynomial`, `IsSmoothlySlice`, `IsTopologicallySlice := sorry`) et des
+preuves de transfert classique ouvertes. Le pont GF(3) Path B
+(`triColorFoxCondition_iff_sum_mod_three`) est **prouvé** (#3003, sorry net-zéro vs
+`main`). Niveau recherche, pas un gap pédagogique. **Évolution documentée**
+(3 → 12 → 11) — n'est PAS une régression silencieuse. Le delta 12 → 11 résulte des
+décharges successives #8766 + #11227 (cf. `knot_lean/README.md` pour la trace par
+fichier) — l'inventaire suit avec un cycle de retard. Puis 11 → **10** après la
+décharge de `conway_trivial_alexander` (preuve kernel déterminant 10×10 ℤ[t],
+See #2874, 2026-09-05 ; re-mesure canonique du jour confirmant **11 sur `main`**,
+`distinct_code_sorry` 11/22 → 10/20 — pas de dérive depuis le 2026-08-28). Puis
+10 → **9** après la décharge de `KT_trivial_alexander` (mineur t⁵ par
+transvections, See #2874, 2026-09-06 ; `distinct_code_sorry` 10/20 → 9/18). Puis
+9 → **8** : fusion de main dans #14821 (2026-09-09) — `Knot.unknottingNumber`
+déchargé sur main par #15082 (définition par infimum, cas trivial prouvé ;
+`distinct_code_sorry` 9/18 → 8/16, re-mesure sur l'arbre fusionné).
 ³ `calibration_lean` est un **composant de harnais** (prover calibration, déplacé depuis
 GameTheory, #1764). Les `· sorry` inline de `Calibration/Nash.lean` sont un **fixture de
 test intentionnel** (le harnais doit gérer un *sorry-increase* 1→2 sans régression) — pas
@@ -115,10 +112,12 @@ théorème de Conway.
 - **Toolchain** : `leanprover/lean4:v4.32.1` · **Dépendance** : Mathlib4
 - **`.lean` files** : 15 (vs 6 modules déclarés 2026-07-15 — cf. EN-siblings comptés
   dans la mesure brute)
-- **sorry (production)** : **11 distincts** (22 code_sorry bruts = 11 FR + 11 EN,
+- **sorry (production)** : **9 distincts** (18 code_sorry bruts = 9 FR + 9 EN,
   dédoublonnés via `count_code_sorry.py distinct_code_sorry`) — recherche-HOLD,
   évolution 3 (2026-07-15) → 12 (2026-08-27) → **11** (2026-08-28, mesure
-  canonique post-#11211/#11227). Majorité = `:= sorry` sur définitions non
+  canonique post-#11211/#11227) → **10** (2026-09-05, `conway_trivial_alexander`
+  déchargé, See #2874) → **9** (2026-09-06, `KT_trivial_alexander` déchargé —
+  mineur t⁵ par transvections, See #2874). Majorité = `:= sorry` sur définitions non
   définies.
 - **Notebook câblé** : 4 notebooks (vs 2 déclarés — 2 notebooks EN-siblings comptés).
 - **Suivi** : #2874 (mandate-C trio MERGED #3997/#3999/#4003), #3003 (Path B GF(3) SHIPPED).