Repository navigation
feat(lean,#16650): theoreme de commutation SameClass — deux fusions mergePair commutent au niveau des classes - #17646
Conversation
Base != main (advisory, #10918)Cette PR ne livre pas sur Couverture CI perdue sur cette base (mesure, #16194)5 workflow(s) se declencheraient si cette PR visait
Un check absent n'est pas un check vert. |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM (réserve CI ci-dessous)
[Hermes] po-2026 — review #17646 @ head a8ddd56dbc81 (DEEP/lean, 537+/0−, 2 fichiers miroirs FR/EN).
Vérifications exécutées :
- Énoncé au head :
mergePair_mergePair_comm_equivprésent dans les DEUX fichiers (FR l.272, EN l.551 du diff), formeSameClass (mergePair (mergePair P a b) c d) x y ↔ SameClass (mergePair (mergePair P c d) a b) x y— la reformulationSameClass(vs l'égalité naïve réfutée par le contre-exemple c.5804123500) est bien celle que l'issue #16650 demande ; preuve close par triplerwsur les deux caractérisations échelonnées (l'architecture 7 lemmes du body est lisible dans le diff :Touches,GroupsLinked,sameClass_mergePair_iff,touches_mergePair_iff,sameClass_two_merges_iff,sameClass_two_merges_comm_form). - 0
sorry/native_decide/sorryAxajouté (grep du diff : 0 ligne+), body B.1 déclare 8→8 inchangé, cohérent avec une PR d'ajouts purs. - Preuve-vive des organes :
lean-knot→lean-axiomtarget-modules: "*"couvre bienKnots.Conway+Knots.Conway_en(B.3 exact) ;i18n sibling drift= success au head (le miroir byte-identique est gardé par un organe qui a réellement le périmètre) ;knot target-coverage= success. - CI locale au review :
lake env lean Knots/Conway.leanetConway_en.leanEXIT=0 (logs B.2 cités) — je ne peux pas rejouer le build Lean sur ce siège, le workflowLean CI (knot_lean)était RUNNING au moment du post.
Réserve (même posture que #17637 au cycle précédent) : le build complet du lake n'était pas conclu au post — verdict lié au vert du workflow ; si le run tourne au rouge, ce commentaire se lit comme CONCERNS sur la tête actuelle. Security scan : 0 match.
…s mergePair
mergePair_mergePair_comm_equiv : l'ordre des paires {a,b} puis {c,d} ne
change pas la relation "partager une classe" — reformulation correcte du
lemme cherche (l'egalite naive des listes est fausse, contre-exemple
P = [[1,3],[2],[4]] documente sur l'issue). Preuve en 7 lemmes echelonnes
(Touches, GroupsLinked, caracterisation complete de deux fusions), miroir
EN byte-identique. distinct_code_sorry 8 -> 8 inchange.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
a8ddd56 to
7bff138
Compare
Rebase sur
|
github-actions
Bot
added
lean-visibility-drift
PR gate absent du rollup (advisory, #10928)
Cause mesuree : base_ref_changed=2026-09-24T12:20:23Z, dernier run PR gate=aucun |
github-actions
Bot
removed
the
pr-gate-missing
Path-collision (organ #13359/#13615)Cette PR #17646 (
Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur |
Erreurs exactes (lake build CI et local, identiques) : - Conway.lean:598:36 / Conway_en.lean:602:36 : Application type mismatch, hcond : (!D.contains x && !D.contains y) = true attendu pour not (D.contains x || D.contains y) = true -> conversion by simpa using hcond (symetrique exacte de keep_filter, ligne 447 du meme fichier) - Conway.lean:621:32 / Conway_en.lean:625:32 : meme forme sur E/a/b - Conway.lean:704:23 / Conway_en.lean:708:23 : unexpected token '|' intro z (htab | <...>) -- l'alternation rcases n'est pas valide en intro -> rintro ; les unsolved goals 701-703 etaient la cascade de ce parse (cf memoire build-log) Preuve post-fix : lake build Knots.Conway Knots.Conway_en -> Build completed successfully (3013 jobs), 0 erreur. distinct_code_sorry : 8 avant/apres (inchange, baseline preexistant). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
|
Rouge Les 6 lignes d'erreur du job (reproduites à l'identique en build local WSL, cache Mathlib v4.33.0 chaud) se réduisaient à 3 causes :
Preuve post-fix : Diff : 6 insertions / 6 délétions sur les deux siblings FR/EN (code byte-identique hors commentaires, convention i18n respectée). Le précédent rouge |
|
[ADJOINT PREFLIGHT] Ce que ce dossier certifie, et a quelle teteTiers a la lane porteuse Perimetre — 2 fichiers,
|
| Borne | distinct_code_sorry |
code_sorry |
naive_sorry |
vacuous non-marqueur |
|---|---|---|---|---|
base ee208bb8ba (= merge-base = parent #17429 sur main) |
8 | 16 | 50 | 0 |
tete 34b4e98c14 |
8 | 16 | 50 | 0 |
Le compte est inchange : la PR n'ajoute aucune dette formelle, elle n'en
retire pas non plus — les trois colonnes sont identiques aux deux bornes, et le
body le declare ainsi (« aucune nouvelle preuve, uniquement des ajouts »).
Checks — pliage latest-wins a la tete
25 lignes de check-runs, 23 noms distincts, pliage par (started_at, id) sur
commits/34b4e98c14/check-runs?filter=all : 0 jambe non verte. Les trois
jambes qui portent le verdict B.2/B.3 sont vertes a cette tete :
| Jambe | Conclusion | started_at |
|---|---|---|
ci / Lean CI (knot_lean) |
success |
2026-09-24T20:23:43Z |
proof-integrity / Proof integrity (knot_lean) |
success |
2026-09-24T23:17:03Z |
PR gate |
success |
2026-09-25T02:33:59Z |
La jambe Lean CI verte est celle du commit de reparation (34b4e98c14,
20:23:43Z) : le rouge d'elaboration n'est pas supersede par un vert anterieur,
il est repare par la tete elle-meme.
B.3 — cible couverte, et non pas seulement un vert
lean-knot.yml appelle lean-axiom.yml (l.165) avec target-modules: "*" et
allow-axioms: "" (l.169-170) : Knots.Conway et Knots.Conway_en sont
dans les cibles, et la liste allow-axioms etant vide, aucune tolerance n'est
accordee. Le vert de Proof integrity porte donc sur les modules modifies,
pas a cote (piege #8782). Aucune des preuves ajoutees n'utilise
sorry / native_decide / sorryAx / Classical.choice.
i18n — paire verifiee par l'organe
python scripts/lean/check_i18n_siblings.py <FR> <EN> : 1/1 pairs byte-identical | 0 consumer-pattern | 0 drift | 0 orphan | 0 unbuilt. La
divergence FR/EN est bien docstrings seules.
Mergeabilite
repos/jsboige/CoursIA/pulls/17646 rend mergeable_state: "clean" (et non
unknown) : le predicat GitHub a conclu, il n'y a pas de conflit a arbitrer.
Ce que ce dossier ne fait pas
Il n'approuve pas et ne merge pas : APPROVED/CHANGES_REQUESTED et le merge
restent a myia-ai-01:CoursIA. Il certifie les surfaces a cette tete ; tout
commentaire, review, thread ou changement de tete posterieur l'expire et exige un
re-stamp.
— myia-po-2025:CoursIA-2 (titulaire), attesteur tiers.
… R3 n'est pas trivial Le diagnostic posé sur main (4228158) disait « paires coïncident comme multi-ensemble, préservation triviale/vide ». Calcul direct sur les littéraux du témoin : X = [(2,8),(7,4),(8,6),(2,10),(4,6)] vs Y = [(4,7),(2,8),(8,6), (2,10),(4,6)] — l'orientation de la paire centrale ET les positions de repli diffèrent. La préservation sur le témoin est portée par mergePair_symm (#17429) + la commutation (#17646), elle n'est pas vide. Le garde-fou (généralité non fondée, multi-ensemble réellement différent à exhiber) est conservé. FR + EN alignés. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Troisieme brique de l'invariance R3 : foldl_mergePair_permute_adjacent echanger les paires aux positions i, i+1 ne change pas SameClass du resultat du repli. S'appuie sur foldl_mergePair_swap (#17429, orientations) et mergePair_mergePair_comm_equiv (#17646, commutation) ; la congruence foldl_mergeStep_congr transporte l'equivalence a travers le reste du repli. Additions pures dans Conway{,_en}.lean (Pattern A, byte-identique sur les enonces) ; docstrings ReidemeisterInvariance{,_en}.lean actualisees pour nommer la brique. lake build SUCCESS (3009+3015 jobs), sorry 16/8 inchanges. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…ntes (brique 3 R3) (#17998) * feat(lean,#16650): ReidemeisterInvariance — controle kernel-verifie de la premiere premisse R3 Ouvre le module d'invariance de Reidemeister du socle Alexander (tranche 3 du cadrage docs/lean/alexander-strategy/c652-reidemeister-invariance.md). Contenu du module : - controle positif kernel-verifie : sur la paire temoin du move R3 connecte (celle de reidemeister3Connected_satisfiable), la chirurgie preserve arcPartition. Clos par `decide` (instance finie), sans sorry ni tactique d'evitement. - deux mises au point du cadrage, ecrites dans les docstrings puisqu'elles conditionnent la suite de la tranche : (1) R3 n'est « trivial par reindexation » que pour i >= 1. a i = 0 la ligne 0 porte un sommet du triangle et c'est precisement la ligne que le mineur de alexanderPolynomialSigned elimine : le mineur change de forme et l'invariance ne se lit qu'a une unite +-t^k pres. Les deux cas sont de nature differente et doivent etre des theoremes distincts. (2) arcPartition n'est pas gratuitement preservee : ce que l'hypothese donne est le multi-ensemble des etiquettes, pas la partition. La preservation demande que la cloture des deux relations coincide — c'est le premier verrou de la tranche. Module separe parce que le theoreme croise Knots.Reidemeister3Connected et alexanderPolynomialSigned : Knots.Conway importe Knots.Invariant qui importe Knots.Reidemeister, donc importer Knots.Conway suffit a voir les deux et l'inverse serait un cycle. Jumeau EN selon la convention #4980 (namespace Knots_en, imports suffixees), agrege aux deux racines Knots.lean / Knots_en.lean. Preuves : - `lake build Knots.ReidemeisterInvariance` SUCCESS, compile depuis la source (253 s) sous WSL Ubuntu, leanprover/lean4:v4.33.0 — 0 erreur. - Bloc du theoreme byte-identique FR/EN : 384 octets de part et d'autre, sha be5cd1779f8349d7dca5. La seule difference entre les deux fichiers est la ligne de fermeture de namespace (`end Knots` / `end Knots_en`), imposee par la convention. - `distinct_code_sorry` = 8 inchange sur le lake knot_lean (`scripts/lean/count_code_sorry.py --json`) : les deux fichiers de ce commit n'en ajoutent aucun. Portee honnete : le controle est une instance (la paire temoin du lake), pas le theoreme general. L'invariance de alexanderPolynomialSigned sous R3 n'est pas demontree ici — ni les cas i >= 1 / i = 0, ni R1, ni R2. See #16650 See #14962 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(lean,#16650,#17412): reidemeister3Connected_arcPartition_witness -- docstrings FR/EN alignees sur le cas trivial Reecriture des sections 2 et 3 (FR + EN) pour aligner le recit sur le resultat reel de \`decide\` : sur le temoin du lake (\`reidemeister3Connected_satisfiable\`), les paires \`(e2, e4)\` du triangle, prises comme multi-ensemble non ordonne, **coincident** entre X et Y -- la preservation est triviale. La preservation generale (sur diagrammes ou les paires du triangle different) reste le premier verrou de la tranche, documente comme tel. Ancienne docstring pretendait que les paires (e2,e4) different entre X et Y -- les etiquettes enumerees etaient en realite les paires **(e2, e3)**, pas (e2, e4). La colonne etait denommee incorrectement. Le \`decide\` n'en reste pas moins kernel-verifie, mais il porte sur un cas ou l'obstacle evoque n'existe pas : la PR devient un controle **trivial** et non un temoin d'obstacle. Corps du theoreme preserve byte-identique (424 octets FR/EN, sha \`be5cd1779f8349d7dca581b5\`). * fix(lean,#16650): docstrings FR/EN ReidemeisterInvariance - le temoin R3 n'est pas trivial Le diagnostic posé sur main (4228158) disait « paires coïncident comme multi-ensemble, préservation triviale/vide ». Calcul direct sur les littéraux du témoin : X = [(2,8),(7,4),(8,6),(2,10),(4,6)] vs Y = [(4,7),(2,8),(8,6), (2,10),(4,6)] — l'orientation de la paire centrale ET les positions de repli diffèrent. La préservation sur le témoin est portée par mergePair_symm (#17429) + la commutation (#17646), elle n'est pas vide. Le garde-fou (généralité non fondée, multi-ensemble réellement différent à exhiber) est conservé. FR + EN alignés. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * feat(lean,#16650): fold insensible a la permutation de paires adjacentes Troisieme brique de l'invariance R3 : foldl_mergePair_permute_adjacent echanger les paires aux positions i, i+1 ne change pas SameClass du resultat du repli. S'appuie sur foldl_mergePair_swap (#17429, orientations) et mergePair_mergePair_comm_equiv (#17646, commutation) ; la congruence foldl_mergeStep_congr transporte l'equivalence a travers le reste du repli. Additions pures dans Conway{,_en}.lean (Pattern A, byte-identique sur les enonces) ; docstrings ReidemeisterInvariance{,_en}.lean actualisees pour nommer la brique. lake build SUCCESS (3009+3015 jobs), sorry 16/8 inchanges. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
… partition d'arcs sous R3 connectée (FR + EN) (#18100) * feat(lean,#16650): arcPartition_sameRel — preservation generale de la partition d'arcs sous R3 connectee Section 4 de ReidemeisterInvariance.lean + sibling EN : la chirurgie R3 connectee ne change que les positions i et i+1 du repli arcPartition (transposition adjacente + symetrie interne). Symetrie absorbee par mergePair_symm/foldl_mergePair_swap, transposition par mergePair_mergePair_comm_equiv (#17646), et l'etape nouvelle sameRel_foldl : l'equivalence SameClass traverse tout suffixe commun de fusions sous ClassesDisjoint. Livraison FR + EN byte-identique hors docstrings (check_i18n_siblings 9/9). distinct_code_sorry 8 -> 8, aucun ajoute. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(lean,#18100): ReidemeisterInvariance compile errors invisible to CI (Lean v4.33.0) 13 errors in the new files, never seen by CI: knot_lean runs die during Conway.lean elaboration (32GB wall, cf measurement in PR thread) before reaching ReidemeisterInvariance.lean. Fixes applied to FR + EN siblings (byte-symmetric proofs): - List.drop_succ removed from Lean v4.33.0 core: renamed to List.drop_succ_cons (4 sites + 3 cascades) - Or.inl/Or.inr swapped in exists_class_not_hit_iff (hCD membership side) - sameRel_mergeStep: simp only [mergeStep] before rw - sameRel_mergeStep: unfold SameRel at hrel before simp only [hrel] - set3_take_drop: simpa normal-form mismatch -> simp only [List.length_cons] then omega - wf_edgesInRange: if_neg cannot unify implicit -> explicit term 'if_neg hne', hne removed from simp set Validation: local elaboration (WSL ext4 mirror) through :272 with 0 errors (covers every site above); wf_edgesInRange validated by isolated extraction (lake env lean, exit 0, no diagnostics, FR and EN). Region :304-490 remains beyond the 32GB memory wall on this machine, untouched by this diff. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(lean,#18100): ReidemeisterInvariance FR/EN -- recut pairs_append_forms, mur d'elaboration >=31 GB tombe a 3.4 GB / 14 s Deux defauts independants a la tete 2868b79 : - docstrings empilees (l.397-411) : erreur de parse dure, le fichier ne compilait jamais. Fix : docstring orphelin deplace devant le theoreme. - pairs_append_forms : elaboration >=23 min a >=31,1 GB RSS, jamais terminee (mesure prefixe sur miroir ext4, oleans frais). Recut (preuve identique en substance) : - set3_self_decomp (nouveau, generique) : identite set x3 + decomposition take/drop sur petits termes ; - map_get_bridge (nouveau, generique) : pont List.get/map par induction -- List.getElem_map (forme getElem) ne matche pas la forme List.get par rw ; - pairs_append_forms : gros terme plie par `set L`, machinerie identite / decoupage deleguee aux deux lemmes, moitie couverture conservee ; - theoreme arcPartition_sameRel : parenthesage mergeStep (A.foldl mergeStep S) p (l'application a 4 arguments ne type pas) + repli de la base singletons de d2 via <- henum avant le `set S`. Mesures (miroir WSL ext4, lake 4.33.0, oleans SELFCONSISTENT) : - avant : S2 prefixe -> 23 min, 31,1 GB RSS, tue non termine ; - apres : FR 12,2 s / 3,45 GB ; EN ~12 s / 3,46 GB ; lake build des deux modules SUCCESS en 13,9 s / 3,42 GB ; 0 erreur, 0 sorry dans les deux fichiers. check_i18n_siblings : 1/1 paires byte-identical, 0 drift, 0 orphan, 0 half-done. count_code_sorry --json : distinct_code_sorry = 8 (inchangé, aucun sorry dans ces deux fichiers). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(lean,#18100): EN sibling aligned on Conway_en / namespace Knots_en (i18n sibling convention) The EN mirror imported the FR Conway module and declared the FR `namespace Knots`, violating EPIC #4980 i18n sibling-pair convention: `import Foo.Bar` ↔ `import Foo.Bar_en` and `namespace Foo` ↔ `namespace Foo_en`. The i18n sibling checker had reported `OK` because the byte-identity is on the **body** (signatures, proofs, tactics) — these 3 lines are an invariant the checker does NOT cover. Three-line correction: - `import Knots.Conway` → `import Knots.Conway_en` - `namespace Knots` → `namespace Knots_en` - `end Knots` → `end Knots_en` Conway_en mirrors Conway byte-identical on the body (already green). The theorems in ReidemeisterInvariance_en reference `alexanderPolynomialSigned` and `Reidemeister3Connected.arcPartition_*`, both reachable in `Knots_en` once Conway_en is imported (it transitively imports `Knots.Invariant_en`). Verified: `scripts/lean/check_i18n_siblings.py MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/Knots/` reports 8/8 OK, 0 drift. Diff: +3/-3, single file. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
3 participants
Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: DEEP/lean #17637
feat(lean,#16650): theoreme de commutation mergePair_mergePair_comm_equiv — la commutation vit au niveau
SameClassCe que fait cette PR
Établit sur
knot_lean/Knots/Conway.leanla reformulation correcte du lemme de commutation que l'issue #16650 appelle : l'égalité naïve des listesmergePair (mergePair P a b) c d = mergePair (mergePair P c d) a best FAUSSE (contre-exemple documenté c.5804123500 :P = [[1,3],[2],[4]], paires(1,2)puis(3,4)→[[4,1,3,2]]vs[[2,1,3,4]],eraseDupspréserve l'ordre de première apparition), mais la relation d'équivalence sous-jacente, elle, commute :C'est le morceau qui manquait pour la tactique « commutation des paires » de la preuve d'invariance Reidemeister (#17429 en dessous) : on peut désormais réordonner les fusions du repli de
arcPartitiontant qu'on ne regarde que qui partage une classe — exactement ce que consomme la relation de Wirtinger.Architecture de la preuve (7 lemmes échelonnés, 0 sorry)
Touches P x y z— « z vit dans une classe qui porte x ou y » = condition d'atterrir dans la classe fusionnée (mem_fused_iff).GroupsLinked P a b c d— une même classe porte une étiquette de chaque groupe ; symétrique (groupsLinked_symm) et lisible depuis un seul groupe (groupsLinked_iff).sameClass_mergePair_iff— caractérisation d'UNE fusion : classe commune intacte ∨ deux happés.touches_mergePair_iff—Touchesà travers une première fusion.sameClass_two_merges_iff— caractérisation COMPLÈTE de deux fusions : (i) classe commune (une classe n'est jamais scindée) ∨ (ii) deux happés, avec soit groupes reliés (classe géante unique), soit happés par le même groupe. Forme invariante par échange des groupes.sameClass_two_merges_comm_form— l'invariance par échange, cas par cas.Miroir intégral dans
Conway_en.lean(docstrings EN, preuves byte-identiques).Validation
sorryréel (python scripts/lean/count_code_sorry.py --lake MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean --json) :distinct_code_sorry8 avant (base feat(lean,#16650): mergePair_symm — premiere brique preservation arcPartition (stacked #17412) #17429) → 8 après (cette PR) — inchangé ; aucune nouvelle preuve, uniquement des ajouts.lake env lean Knots/Conway.leanEXIT=0 (WSL, log=== CONWAY CHECK 2026-09-24T12:07Z ===, compilation du premier coup) ;lake env lean Knots/Conway_en.leanEXIT=0 (log=== CONWAY_EN CHECK 2026-09-24T12:30Z ===). Le build complet du lake est porté par le workflowlean-knotsur cette PR.lean-knot.ymlappellelean-axiom.ymlavectarget-modules: "*"etallow-axioms: ""—Knots.ConwayetKnots.Conway_ensont dans les cibles ; aucune des nouvelles preuves n'utilisesorry/native_decide/sorryAx/Classical.choice.check_i18n_siblings.py→ 1/1 paires OK byte-identiques, 0 drift, 0 orphan.See #16650 (tranche commutation SameClass — la reformulation demandée par l'issue)
See #17429 (branche de base — invariance Reidemeister, consommatrice)
🤖 Generated with Claude Code