Repository navigation
[lean] La fonction Alexander designee diverge du classique sur la classe a 4 croisements (knot_lean) #14962
Description
Titre
[lean] La fonction Alexander désignée diverge du classique sur la classe à 4 croisements (knot_lean)
Contexte
Le développement knot_lean (§4 de Knots/Conway.lean) désigne une
normalisation du polynôme d'Alexander : mineur sans la première ligne ni la
dernière colonne de la matrice alexanderEntry, d'entrée +t (arc entrant du
dessous), −1 (arc sortant du dessous), 1−t (arc du dessus).
Les contrôles prouvés existants (alexander_unknot, alexander_trefoil) sont
exacts. Mais la fonction ne reproduit pas le polynôme classique sur la classe à
4 croisements — c'est l'anomalie "Finding B" documentée par la PR de correction
du câblage 4_1.
Mesure (réplique validée)
Une réplique Python fidèle à la construction Lean (mergePair/arcPartition/
alexanderEntry/mineur), validée sur le théorème PROUVÉ alexander_trefoil
(rend t² − t + 1 exact ; arcs [[4,5],[1,6],[2,3]] identiques au hp du
théorème), a été utilisée pour mesurer :
-
Câblage corrigé du noeud en huit (le câblage précédent était un entrelacs
à deux composantes). Le code PD dérivé de DT[4,6,8,2]:
[[8,3,1,4],[2,5,3,6],[4,7,5,8],[6,1,7,2]], boucle unique vérifiée.
→ la fonction rend−2t² + 2t − 1(contrôlealexander_figureEight
prouvé dans la PR de correction).- arcs réels :
[[3,4],[5,6],[7,8],[1,2]] - mineur :
−1 + 2t − 2t², et|P(−1)| = 5 = det(4_1)✓
- arcs réels :
-
Énumération exhaustive des câblages orientés à 4 croisements formant une
boucle unique (passages cycliques canonisés par rotation + réflexion, ×
masques dessus/dessous, filtrés par orientation — chaque arête une fois en
dessous + une fois en dessus) :- n = 3 : 88 câblages valides, 8 rendent
t² − t + 1(dont les deux codes
trèfle connus — sanity OK, la fonction est invariante par miroir sur le
trèfle, cohérent avec son amphichiralité). - n = 4 : 2736 câblages valides, 0 rendent
unit × (t² − 3t + 1)
(le 4_1 classique). Le câblage DT-dérivé rend−2t² + 2t − 1.
- n = 3 : 88 câblages valides, 8 rendent
Diagnostic
Le trèfle est amphichiral, donc la fonction (qui code la chiralité du
croisement) rend le bon t² − t + 1 par coïncidence de symétrie. Le |P(−1)|
(= déterminant du noeud) est reproduit sur 4_1, mais la forme du polynôme
diverge dès n = 4 — la différence −2t²+2t−1 vs t²−3t+1 n'est pas une unité.
Indice : la normalisation désignée (mineur sans 1re ligne ni dernière colonne)
dépend de l'uplet (e1,e2,e3,e4) du code PD et de l'ordre d'arcPartition ; ce
mineur désigné n'est pas invariant sous les mouvements de Reidemeister pour
n ≥ 4, alors que le polynôme classique l'est à une unité près (±t^k).
Premier pas suggéré
Démontrer (ou borner) l'invariance de Reidemeister pour alexanderPolynomial,
puis corriger la normalisation si l'invariance échoue : symétrisation
Δ(t) = Δ(1/t) à une unité près, ou normalisation de Conway Δ(1) = 1,
au lieu du mineur désigné brut. Vérifier aussi que la garde
arcs'.length = rest.length + 1 ne suffit pas à garantir l'invariance (elle ne
contrôle que la non-dégénérescence du mineur, pas sa forme).
Hors périmètre
La portée de la correction du câblage 4_1 (un entrelacs à deux composantes qui
passait les gardes de formation) est traitée dans la PR de correction ; cette
issue ne tracke que l'anomalie de la fonction Alexander sur la classe 4
croisements.
Activity
jsboige commentedon Sep 7, 2026
[CLAIMED] lane myia-po-2026:CoursIA — 2026-09-07T21:05Z — reprise de l'anomalie Alexander : tranche 1 (borner l'invariance : formaliser la divergence 4_1 vs classique en Lean, non-unité), puis correction de normalisation si la fenêtre le permet. Interaction suivie : PR #14821 ouverte sur conway_trivial (valeur désignée −t⁶ calée sur la convention actuelle) — sera arbitrée/flagée avant livraison si je touche la convention.
jsboige commentedon Sep 7, 2026
Tranche 1 livrée — PR #15120.
Réponse au « premier pas suggéré » : l'invariance est bornée négativement de façon formelle —
alexander_figureEight_not_classicalprouve que la valeur désignée −2t²+2t−1 n'est égale à ε·t^k·(t²−3t+1) pour AUCUNE unité. Conséquence : les deux options de normalisation de l'issue (symétrisation, Conway Δ(1)=1) ne peuvent PAS réparer la divergence — elle est un artefact de chiralité :alexanderEntryest la ligne de Fox d'un croisement positif, appliquée à tous les croisements (le PD ne code pas les signes ; trèfle documenté tout positif → correct ; huit 2+/2− → faux sur les négatifs). Le déterminant |P(−1)|=5 survit (alexander_figureEight_eval_neg_one).La réparation est livrée en variante :
alexanderPolynomialSigned(chiralité en donnée, ligne négative dérivée de Wirtinger miroir) + preuve que l'étiquetage alterné du câblage DT-dérivé rend le classique exact t²−3t+1 (alexander_figureEight_signed) et le miroir t·(t²−3t+1) (_signed_mirror). Réplique Python validée sur les théorèmes prouvés de main + énumération des 16 affectations (les 4 rendant le classique sont exactement les alternées/mirror-paires, cohérent avec l'amphichiralité de 4_1).lake build SUCCESS 3010 jobs ; axioms [propext, Classical.choice, Quot.sound] sur les 7 nouvelles déclarations, zéro sorryAx ; sorry 12→12 / 13→13 ; rien de retiré (fonction non signée et les 4 théorèmes existants inchangés — aucune interaction avec #14821).
Résiduel (tranche 2, décision de schema) : porter les signes dans la donnée du nœud (champ PDCrossing/KnotDiagram ou structure dérivée du DT) pour faire de la variante signée LA fonction du nœud — si elle est retenue, les énoncés
conway_trivial_alexander(−t⁶) etKT_trivial_alexander(t⁵) devront être recalés (leurs valeurs désignées changeraient). L'invariance de Reidemeister de la variante signée (machinerie Reidemeister.lean disponible) est la tranche suivante naturelle.feat(lean,#14962): bound Alexander divergence on 4_1 — chirality arti…
jsboige commentedon Sep 11, 2026
[CLAIMED] lane myia-po-2027:CoursIA — le socle structurel de la divergence : prouver le fait de Fox qui rend le mineur désigné bien défini à une unité près (paire de dessus dans une même classe d'arcs ⇒ lignes de
alexanderEntryde somme nulle ⇒ tout choix de colonne frappée ne change le mineur que d'un signe) — paths: MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/Conway_en.leanReprise de la claim périmée de
myia-po-2026:CoursIA(88.6 h ≥ 48 h, cfcheck_lane_claim.py).Périmètre déclaré : Conway.lean + son sibling
_en, sur les déclarationsmergePair/arcPartition/alexanderEntry. La tranche 2 de l'issue (porter les signes dansPDCrossing/KnotDiagram) est hors périmètre de cette claim et volontairement non traitée : elle changerait la fonction du nœud et casserait les énoncés deconway_trivial_alexanderetKT_trivial_alexander, que les PR ouvertes #15440 et #15460 prouvent. Aucun fichier de ceux-ci n'est touché.jsboige commentedon Sep 11, 2026
Tranche structurelle livrée : PR #15596 —
feat(lean,#14962): fait de Fox — paire de dessus dans une classe d'arcs + somme de ligne nulle (FR+EN).Deux théorèmes nouveaux dans
Knots/Conway.lean(+ siblingConway_en.lean) :arcPartition_sameClass_overStrand— en chaque croisement d'un diagramme à étiquettes en plage (EdgesInRange), les deux étiquettes de dessuse2/e4appartiennent à une même classe dearcPartition. Preuve par le replifoldl mergeStep:mergePairne scinde jamais une classe (sameClass_mergePair) et réunit chaque paire traitée (sameClass_mergePair_self), initialisé par la couverture des singletons (covered_singles). C'est la traduction combinatoire de la relation de Wirtinger.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.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 prouvé — elle n'était jusqu'ici qu'assertée.Preuves §B :
lake buildSUCCESS (3010 jobs, cache Mathlib chaud rev520045ab), axiomes nommés au#print axioms(propext, Classical.choice, Quot.sound— même trio que #15120 sur ce lake), aucunsorryAx, aucunnative_decide,distinct_code_sorry10 → 10 (grain purement additif),check_i18n_siblings.py --allOK,lean-knot.yml→lean-axiom.ymlcâblé (jobknot target-coveragePASS sur la PR).Résiduel nommé (tranches suivantes de See #14962) : (a) la vérification que
arcPartitionsatisfait les hypothèses d'unicité (countP= 1 par étiquette, en général et pas seulement sur les diagrammes de contrôle) — c'est la boucle qui reste à fermer entre les deux théorèmes ci-dessus ; (b) l'invariance de Reidemeister de la variante signée.Tranche 2 (porter les signes dans
PDCrossing/KnotDiagram) volontairement hors périmètre : elle changerait la fonction du nœud et casserait les énoncés deconway_trivial_alexander/KT_trivial_alexandervisés par #15440 et #15460.jsboige commentedon Sep 11, 2026
Tranche 2 livrée : PR #15600 —
feat(lean,#14962): arcPartition est une partition — unicité countP=1 + somme de ligne inconditionnelle (FR+EN)(empilée sur #15596, base = sa branche).Ce que la tranche 1 laissait en résiduel est prouvé :
arcPartition_classes— la vraiearcPartitionest une partition : classes deux à deux disjointes (invariant quemergePairpréserve) et sans doublon (le bloc fusionné portex, une classe intacte ne le porte pas).arcPartition_countP_label— chaque étiquette de1..numEdgesappartient à exactement une classe : les hypothèsescountP= 1 d'alexanderEntry_sum_zerodeviennent des théorèmes.alexanderRow_sum_zero— chaque ligne de la vraie matrice d'Alexander somme à zéro, sans aucune hypothèse laissée à la main du lecteur :((arcPartition d).map (alexanderEntry c)).sum = 0.Preuves §B :
lake buildSUCCESS (3010 jobs),distinct_code_sorry10 → 10 (additif), axiomes[propext, Classical.choice, Quot.sound]sur les trois théorèmes,Conway_en.leani18n OK, Proof integrity CI PASS sur #15596 (le même câblage s'applique à #15600).Résiduel restant (tranche suivante) : l'invariance de Reidemeister de la variante signée. Le socle structurel est complet.
Merge pull request #15596 from jsboige/feature/14962-alexander-arc-ro…
feat(lean,#14962): fait de Fox — paire de dessus dans une classe d'ar…
feat(lean,#14962): arcPartition est une partition — unicité countP=1 …
jsboige commentedon Sep 18, 2026
[ADJOINT CLOSE] Adjugée CLOSE_WITH_FOLLOWUP — campagne de consolidation du 2026-09-18 (mandat ai-01 2026-09-18T03:12Z, fermeture déléguée, fille ouverte AVANT fermeture).
Socle livré, vérifié firsthand :
Résidu tracé en fille : #16650 #16650 — invariance de Reidemeister de la variante signée (
alexanderPolynomialSigned), nommée explicitement comme tranche suivante.Réouvrir en citant le critère manquant si contestation.
docs(lean,#16650): cadrage strategique invariance de Reidemeister de …
feat(lean,#16650): ReidemeisterInvariance — controle kernel-verifie d…
feat(lean,#16650): repli insensible a la permutation de paires adjace…