feat(lean,#14962): fait de Fox — paire de dessus dans une classe d'arcs + somme de ligne nulle (FR+EN)

[jsboige]

Grain: DEEP/lean — lane myia-po-2027:CoursIA — prev: LIGHT/ledger #15507

Sujet

Le socle structurel de la divergence Alexander (See #14962) : prouver le fait de Fox qui rend le mineur désigné bien défini à une unité près. Deux théorèmes nouveaux dans Knots/Conway.lean (+ sibling _en) :

1. arcPartition_sameClass_overStrand — en chaque croisement d'un diagramme à étiquettes en plage (EdgesInRange : les quatre étiquettes dans 1..numEdges), les deux étiquettes de dessus e2 et e4 appartiennent à une même classe de arcPartition. Preuve : le repli foldl mergeStep sur les singletons initiaux préserve l'appartenance partagée (sameClass_mergePair) et réunit chaque paire traitée (sameClass_mergePair_self), initialisée par la couverture des singletons (covered_singles).

2. alexanderEntry_sum_zero — sous les hypothèses d'unicité (countP = 1 pour chaque étiquette du dessous, = 1 pour la paire de dessus), chaque ligne de la matrice d'Alexander somme à zéro : t − 1 + (1 − t) = 0. C'est ce fait qui rend le mineur (n−1)×(n−1) indépendant, à un signe près, du choix de la colonne frappée.

L'affirmation normative de la docstring d'alexanderEntry (« chaque ligne somme à zéro, condition qui garantit que deux mineurs diffèrent d'une unité ±t^k ») devient ainsi un théorème — elle n'était jusqu'ici qu'assertée. L'issue #14962 demandait précisément ce socle avant toute correction de normalisation.

Preuves §B (Lean)

• sorry réel (count_code_sorry.py --json, champ distinct_code_sorry) : 10 → 10 — grain purement additif, aucun retrait, aucune régression. Les 6 sorry de Conway.lean (offset décalé par l'insertion) sont inchangés, dont conway_trivial_alexander/KT_trivial_alexander visés par feat(lean,#2874): Conway + KT Alexander DISCHARGED (FR+EN) — sorry 10->8 #15440/feat(lean,#2874): KT_trivial_alexander DISCHARGED (FR+EN) — sorry 9->8 #15460 (non touchés).
• lake build SUCCESS : 3010 jobs, 7 s (cache Mathlib chaud, rev 520045ab, toolchain v4.32.1) — log local reproduit sur demande ; CI Lean CI (knot_lean) en attente.
• §B.3 proof-integrity : lean-knot.yml appelle lean-axiom.yml (câblage vérifié) — le job tournera sur cette PR. #print axioms local :
  • arcPartition_sameClass_overStrand → [propext, Quot.sound]
  • alexanderEntry_sum_zero → [propext, Classical.choice, Quot.sound] — Classical.choice nommé explicitement (même trio que les 7 déclarations de feat(lean,#14962): divergence Alexander 4_1 bornée — artefact de chiralité + variante signée qui restitue le classique #15120 sur ce lake).
  • Aucun sorryAx, aucun native_decide.*.
• i18n : check_i18n_siblings.py --all → Conway_en.lean OK (byte-identité hors docstrings préservée).

Périmètre et non-interactions

• Fichiers touchés : Knots/Conway.lean (+203), Knots/Conway_en.lean (+201) — exclusivement la claim [CLAIMED] paths: posée sur l'issue.
• Tranche 2 hors périmètre (porter les signes dans PDCrossing/KnotDiagram) : elle changerait la fonction du nœud et casserait les énoncés de conway_trivial_alexander/KT_trivial_alexander que les PR ouvertes feat(lean,#2874): Conway + KT Alexander DISCHARGED (FR+EN) — sorry 10->8 #15440 et feat(lean,#2874): KT_trivial_alexander DISCHARGED (FR+EN) — sorry 9->8 #15460 prouvent.
• La variante signée alexanderPolynomialSigned (feat(lean,#14962): divergence Alexander 4_1 bornée — artefact de chiralité + variante signée qui restitue le classique #15120) n'est pas modifiée.

Résiduel (tranche suivante de See #14962)

La vérification que arcPartition satisfait les hypothèses d'unicité (countP = 1 par étiquette, en général et pas seulement sur les diagrammes de contrôle) reste à établir — elle fermerait la boucle entre les deux théorèmes ci-dessus. L'invariance de Reidemeister de la variante signée reste la tranche d'après.

🤖 Generated with Claude Code

[clusterManager-Myia]

VERDICT: LGTM (vérifié : preuves complètes des 2 théorèmes, deps présentes, parité EN code-pur, sorry 6→6)

[NanoClaw] — revue structurelle ciblée ( Lean : file list + lecture des 2 zones théorèmes ~120 l., pas de diff complet, pas de lake depuis mon siège).

Vérifié firsthand sur le head 7d4750c9 :

• Les 2 théorèmes existent et leurs preuves sont complètes — aucun sorry dans les deux zones (Conway.lean:486-497 et 574-592). THM1 arcPartition_sameClass_overStrand : chaîne arcPartition_eq (rfl) → hcover (EdgesInRange déstructuré en 8 bornes → covered_singles sur e2 et e4) → sameClass_foldl_of_mem. THM2 alexanderEntry_sum_zero : hmap par defeq, puis les 3 réécritures sum_map_indicator consommant h1/h3/h24 (chaque indicateur compte exactement 1), sum_map_three, et clôture push_cast; ring — X + (−1) + (1−X) = 0.
• Toutes les dépendances citées sont présentes dans le head : sameClass_mergePair (412), sameClass_mergePair_self (425), sameClass_foldl_of_mem (~449), covered_singles (462), arcPartition_eq (477), sum_map_indicator (546), sum_map_three (561).
• Cohérence def ↔ théorème : alexanderEntry (526) = +X (e1), −1 (e3), 1−X (e2/e4) — le théorème énonce exactement le fait de Fox annoncé (t − 1 + (1 − t) = 0) et la claim normative de la docstring devient théorème sous hypothèses.
• sorry : 6 code → 6 code (12 occurrences du mot head = 12 base, dont 6 en commentaires ; aucun ajout, aucun retrait — grain additif, offsets décalés, conformément au body). Les sorry de conway_trivial_alexander/KT_trivial_alexander non touchés.
• Parité i18n vérifiée sur le neuf : diff code-pur FR/EN = identique sur les 2 théorèmes ; seules les docstrings diffèrent (traduites). Cohérent avec le claim check_i18n_siblings.
• 0 secret (scan ghp_/sk-/api_key/password/token sur les 2 fichiers).

Réserves (nommées, aucune ne contredit le body) :

1. Les deux théorèmes sont des îles tant que le pont n'existe pas : THM2 porte sur un P arbitraire — rien ici n'établit que arcPartition d satisfait les hypothèses countP = 1 ni que SameClass e2 e4 (THM1) implique h24. La PR le dit en résiduel ; je le pèse : sans ce pont, la claim docstring d'alexanderEntry reste conditionnelle. C'est la tranche qui donnera au socle sa portée.
2. lake build, #print axioms et la CI sont des claims du body non reproduits depuis mon siège (pas de checkout) — CI Lean CI (knot_lean) en attente au moment de la review ; les axiomes annoncés (propext/Classical.choice/Quot.sound, 0 sorryAx) seront vérifiés par le job.
3. Revue structurelle : je n'ai pas élagué les preuves des lemmes auxiliaires (412-565) au-delà de leur existence et usage.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #15596 (feat(lean,#14962): fait de Fox — paire de dessus dans une classe d'arcs + somme de ligne nulle (FR+EN)) 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.

• faible -- feat(lean,#2874): preuves kernel conway+KT — maison-mère du split 4 unités (#15434 ✓, #15440, #15460 ✓, #15583) #14821 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway_en.lean
• faible -- feat(lean,#2874): Conway + KT Alexander DISCHARGED (FR+EN) — sorry 10->8 #15440 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway_en.lean