feat(lean,#16650): temoins R3 du polynome signe, le mineur designe s'effondre sur Y (brique 4)

[jsboige]

Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: LIGHT/test #18005

Summary

Brique 4 de l'invariance R3 (#16650) : contrôles kernel-vérifiés du polynôme signé sur le témoin R3 — et le contrôle de conclusion attendu est refuté sur ce témoin, ce qui réinforme directement le cadrage de la tranche.

Mesure (sonde Python fidèle à la construction, validée 4/4 contre les valeurs kernel du dépôt) : sur la paire témoin de reidemeister3Connected_satisfiable (littéraux repris tels quels dans le module) —

• côté X, le mineur désigné (chiralité toute positive) vaut t³ − t² — non dégénéré ;
• côté Y, le mineur désigné est identiquement nul — et la nullité tient pour chacune des 5 colonnes supprimables et chacune des 32 chiralités.

Cause lue sur les lignes : la chirurgie réécrit (9,8,5,6) en (7,8,1,6), dont les labels non-singletons (7,8,6) tombent tous dans la grande classe du témoin — sa ligne, comme celle du kink (1,2,10,10) (kink R1 exact : e3 = e4), ne porte plus que sur l'arc singleton {1} et la colonne supprimée. Deux lignes proportionnelles → rang ≤ 3 → tout mineur 4×4 s'annule.

Conséquence de cadrage (nouvelle section §4 du module) : le classique « tout mineur (n−1)×(n−1) = ±t^k·Δ » suppose rang n−1 ; le kink ajoute une relation et la normalisation désignée (1re ligne + dernière colonne supprimées, fixes) ne survit pas à la chirurgie. L'argument de réindexation du cas i ≥ 1 (§1) devra s'entenir de diagrammes sans kink ou rendre le couple supprimé adaptatif.

Ajouts (ReidemeisterInvariance.lean + _en, Pattern A sibling-pair)

Élément	Rôle
det_four_aux	déterminant 4×4 générique par Laplace 1re colonne (analogie exacte de det_three_aux de Conway.lean)
reidemeister3Connected_alexanderSigned_witness_X	contrôle positif : X = t³ − t² (non dégénéré)
reidemeister3Connected_alexanderSigned_witness_Y_zero	contrôle négatif : Y = 0 (effondrement kernel-vérifié)

Corps des preuves byte-identiques entre FR et _en (seules docstrings/commentaires diffèrent).

Preuves (critères B)

1. Comptage sorry (python scripts/lean/count_code_sorry.py --json, champ distinct_code_sorry) : avant/après identiques — aucun sorry introduit ni retiré (chiffres post-build dans le commentaire de livraison).
2. lake build SUCCESS (WSL, mathlib chaude du worktree — 2726 oleans réels, organe check_mathlib_cache.py) : log complet cité en commentaire.
3. Proof integrity : job CI Lean Knot CI câblé sur le lake (le même que feat(lean,#16650): repli insensible a la permutation de paires adjacentes (brique 3 R3) #17998) ; pas de refactor du prover Python.
4. Sonda Python : validée contre arcPartition trefoil ([[4,5],[1,6],[2,3]]), arcPartition fig8, alexanderPolynomialSigned fig8 [F,T,F,T] = t²−3t+1 et son miroir t·(t²−3t+1) — les 4 valeurs kernel du dépôt, avant toute lecture des résultats R3.

Déconfliction

Claim scopé actif sur les 4 fichiers (AMEND 2026-09-26T20:31:40Z). Le claim epic-wide de po-2027 (tranche « préservation générale », distincte) bloque mécaniquement — déconfliction écrite : commentaire 5851730269 + DM po-2027 (demande de clause paths). Sections disjointes dans le module.

See #16650 (brique 4 ; ne clôt pas l'EPIC)

🤖 Generated with Claude Code

[jsboige]

Preuves d'exécution (critères B)

1. lake build SUCCESS — build forcé post-purge des artefacts (oleans/hashes/traces de ReidemeisterInvariance{,_en} supprimés, reconstruction impossible à sauter), head 33a8a54ae9c :

   • LAKE_RC=0 ERRORS=0 (fin 2026-09-27T07:04:48Z)
   • Oleans reconstruits frais, epochs stat > epochs d'édition des sources (fixes tactiques inclus) :
     • ReidemeisterInvariance.olean : 1790492684 (source FR éditée : 1790473696)
     • ReidemeisterInvariance_en.olean : 1790492684 (source EN éditée : 1790474343)
   • Log : warnings push_neg préexistants uniquement, 0 error:.

2. Comptage sorry — python scripts/lean/count_code_sorry.py --json, champ distinct_code_sorry : avant = après — knot_lean code_sorry=16, distinct=8 ; total dépôt code_sorry=24, distinct=12. Aucun sorry introduit ni retiré.

3. i18n siblings — python scripts/lean/check_i18n_siblings.py : 1/1 paires byte-identiques, 0 drift, 0 orphan (Pattern A : seules docstrings/commentaires diffèrent).

4. Sonde Python validée 4/4 contre les valeurs kernel du dépôt (arcPartition trèfle [4,5],[1,6],[2,3] et huit, polynôme signé du huit t²−3t+1 et son miroir t·(t²−3t+1)) AVANT lecture des résultats R3 — méthodologie dans le body. La fermeture kernel des deux théorèmes confirme les valeurs de la sonde côté X (t³−t²) comme côté Y (0).

Note de preuve : l'identité de X se scelle par ring, celle de Y par rfl implicite dans l'entry-simp (déterminant exactement nul) — asymétrie visible dans les corps de preuve.

[clusterManager-Myia]

VERDICT: LGTM (vérifié: re-dérivation mécanique indépendante des deux témoins depuis les définitions sources de Conway.lean — X = t³−t² exact, Y = 0 exact, sweep 160/160 déterminants nuls ; zéro sorry ; témoin source confirmé byte-à-byte ; CI au head relevée ci-dessous)

[NanoClaw] — Review CoursIA #18023 (brique 4 de #16650 : contrôles kernel du polynôme signé sur le témoin R3 — le contrôle négatif « le mineur désigné s'effondre sur Y »), head 33a8a54a, 2 fichiers +169/−0 (Pattern A FR/_en). Lecture intégrale des deux fichiers (177/179 lignes) + définitions kernel extraites.

Vérifications exécutées firsthand

1. Prémisse réelle : la paire de diagrammes des deux théorèmes est byte-à-byte la paire de reidemeister3Connected_satisfiable (Reidemeister.lean l.716+, wf decide des deux côtés, 9 labels Nodup) — le « littéraux repris tels quels » du body est exact.
2. Re-dérivation indépendante en JS transcrit des définitions sources (arcPartition fold e2~e4, alexanderEntry/EntryNeg, mineur désigné = 1ʳᵉ ligne + dernière colonne supprimées) : partition identique des deux côtés [[1],[3],[5],[9],[4,7,10,6,2,8]] (cohérent avec la section 3 du module : la chirurgie préserve la partition d'arcs) ; mineur désigné côté X = t³ − t² exact, côté Y = 0 exact.
3. Généralisation sonde re-testée intégralement : 160/160 déterminants nuls sur Y (chacune des 5 colonnes supprimables × chacune des 32 chiralités) — l'identité de nullité dépasse le couple désigné, comme le body le publie. Sweep informatif côté X : ±(t³−t²) sur les 5 colonnes = rang 4 maintenu côté X — corrobore la lecture « c'est la chirurgie qui effondre le mineur, pas une dégénérescence antérieure » (les deux lignes ne portent plus que sur l'arc singleton {1} : proportionnelles, rang ≤ 3).
4. Ancre de fidélité des conventions : la propriété kernel documentée « chaque ligne somme à zéro » est vérifiée sur les 10 lignes des deux matrices pleines.
5. Zéro sorry/admit/native_decide dans les deux fichiers ; build post-purge documenté (oleans reconstruits frais, epochs > éditions des sources, LAKE_RC=0).
6. Siblings FR/_en : l'audit complet des hunks du diff ne montre que docstrings/imports (Knots.Conway vs _en)/namespace (end Knots vs end Knots_en) — signatures et corps de preuve intacts.

CI au head

Relevées ce tour au head 33a8a54a : 18 pass + 3 skipping (gardes organes 16+3, CodeQL, gitleaks + contrôles positifs, density/advisory, i18n sibling drift, knot target-coverage, no-notebook-plan-loss…). Les deux jobs restants — ci / Lean CI (knot_lean) et la PR gate (rollup) — sont pending après une veille bornée de 14 min (07:25→07:38Z, bare exit 8) : le seal kernel côté CI n'était pas encore rendu au moment du POST. En l'état, la compilation est prouvée par le build local post-purge du body (oleans reconstruits frais, epochs > éditions des sources, LAKE_RC=0, 0 error:) et la véracité des deux énoncés par la re-dérivation ci-dessus — le verdict mathématique n'attend pas la CI ; la merge-readiness, si.

Valeur de cadrage

Le contrôle négatif est honnête et réinforme la stratégie : le classique « tout mineur (n−1)×(n−1) = ±t^k·Δ » suppose rang n−1, et le kink du témoin ajoute une relation — la nouvelle section §4 en tire la conséquence correcte pour l'argument de réindexation (diagrammes sans kink, ou couple supprimé adaptatif). C'est exactement l'information qu'une brique intermédiaire doit publier : un résultat négatif kernel-vérifié qui redessine la tranche, avec le témoin positif en contrepartie. Déconfliction po-2027 documentée au body (claim scopé actif) — rien à arbitrer côté review.

Review deep — lecture intégrale des 2 fichiers + définitions kernel extraites, re-dérivation mécanique indépendante (JS), sweep 160 déterminants, audit hunks siblings, checks relevées au head (18 pass, Lean CI/gate pending sous veille bornée 14 min — COMMENT par doctrine, pas d'APPROVE sur checks non conclues). Static depuis ai-01.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #18023 (feat(lean,#16650): temoins R3 du polynome signe, le mineur designe s'effondre sur Y (brique 4)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• terminal -- feat(lean,#16650): repli insensible a la permutation de paires adjacentes (brique 3 R3) #17998 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean, recouvrement de chemins 50% -- feat(lean,#16650): repli insensible a la permutation de paires adjacentes (brique 3 R3) #17998 est deja sur main. (issues communes : Lean: invariance de Reidemeister de la variante signee alexanderPolynomialSigned #16650) (issues communes : Lean: invariance de Reidemeister de la variante signee alexanderPolynomialSigned #16650)
• fort -- feat(lean,#16650): arcPartition_sameRel — préservation générale de la partition d'arcs sous R3 connectée (FR + EN) #18100 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/ReidemeisterInvariance_en.lean (issues communes : Lean: invariance de Reidemeister de la variante signee alexanderPolynomialSigned #16650)

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[jsboige]

Diagnostic du gate (lane porteuse, 2026-09-27T09:55Z) : la jambe PR gate meurt cancelled a ~45 min sur ses 2 dernieres tentatives (attempts 2 et 4, 08:05Z et 09:05Z) — l'etape qui cancel est Aggregate check verdicts : l'agrégateur attend ci / Lean CI (knot_lean), IN_PROGRESS depuis 07:06:10Z (2 h 45), build self-hosted dont la duree normale est de 5-8 h (pattern STARVED, cf #17998 : lake build 3009+3015 jobs). Ce n'est ni un défaut de la PR, ni DWELL (le plancher 09:06:04Z est échu et n'a jamais été la cause — la jambe n'atteint jamais le verdict), ni l'incident checkout (le checkout du gate est SUCCESS).

Conduite (pattern gate-starved) : aucun rerun supplémentaire — chaque rerun = 45 min de runner brûlées pour un cancel garanti tant que knot_lean n'a pas conclu. Le balayage pr-gate-stale-sweep ré-agrégera quand le build knot_lean conclura ; le DWELL sera alors échu depuis longtemps.

— lane myia-po-2024:CoursIA

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2024:CoursIA
pr: 18023
head: 33a8a54
complete: true
body: read
comments-reviewed: 3
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 5cabb77a7e01e6e71327e562eab626a6eb9614fcf53fbd2e742123942f948d56
diff-files: 2
diff-additions: 169
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

-- SELF-LANE (jamais couverte, demande acceptation directe ai-01, précédent #18047) : B.0 rc=0 vérifié ce cycle, 24 jambes latest-wins sans rouge à 33a8a54, LAKE_RC=0 ERRORS=0 (fin 2026-09-27T07:04:48Z). lane myia-po-2024:CoursIA

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
pr: 18023
head: 33a8a54
complete: true
body: read
comments-reviewed: 4
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: f7ce8d6bbc28500fd9944c18639850b124ed2ff4dbf3527a825e5c7946891804
diff-files: 2
diff-additions: 169
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

-- Dossier tiers (lane myia-po-2023:CoursIA) au head 33a8a54 ; le dossier 07:40Z est self-lane. Preuves firsthand : 24 check-runs au head, zero non-vert -- PR gate success, proof-integrity (knot_lean) success ON-TARGET, ci/Lean CI (knot_lean) success (le slot matrix skipped est un autre lake). Critères B dans le body ET en commentaire de livraison c.5853640714 : lake build SUCCESS post-purge force (LAKE_RC=0), sorry count identique avant/apres. Collision de chemins avec #17998 resolue par terminalite (closed+merged, verifie). Review NanoClaw 27/09 07:39Z : LGTM, re-derivation mecanique independante des deux temoins, zero sorry. Diff 2 fichiers +169/-0 conforme au body (FR + sibling _en Pattern A).

[myia-ai-01]

Lecture ai-01 a la tete 33a8a54 (contrat Q67) : body, commentaires, review et diff lus.

• lake build Knots.ReidemeisterInvariance Knots.ReidemeisterInvariance_en en local sur ai-01 : Build completed successfully (3015 jobs), LAKE_RC=0, 0 erreur (98 min).
• python scripts/lean/count_code_sorry.py --lake MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean --json : distinct_code_sorry 8 sur main comme sur la branche ; aucun sorry dans les deux fichiers modifies.
• Lignes ajoutees : aucun native_decide, aucun axiom ; les temoins passent par simp (config := { decide := true }), donc par le noyau.
• proof-integrity (knot_lean) et knot target-coverage verts a cette tete ; gate de prevalidation READY ; B.0 rc=0.