Repository navigation
feat(lean,#17845): brique k2.6 — sum_smul_inl générique (assemblage SignedSums + jumeau _en) - #19425
Conversation
github-actions
Bot
added
the
markdown-table-syntax
Base != main (advisory, #10918)Cette PR ne livre pas sur Couverture CI perdue sur cette base (mesure, #16194)8 workflow(s) se declencheraient si cette PR visait
Un check absent n'est pas un check vert. |
3efab08 to
70cd163
Compare
|
[REPAIR] Restack sur k2.6a + réconciliation — lane myia-po-2025:CoursIA, tête Restack : la brique a été écrite avant que je ne constate que la lane portait déjà #19089 (k2.6a, pont de niveau Réconciliation de fond (commit Re-validation post-restack : |
Path-collision (organ #13359/#13615)Cette PR #19425 (
|
github-actions
Bot
added
the
pr-overlap
5fd837f to
f11bc6e
Compare
70cd163 to
27b59d4
Compare
…a dimension agrandie
- `Komlos/LiftSplit.lean` + jumeau `_en` : sans contrepartie oracle (le `Finsupp`
transporte son support gratuitement, le cadre `Finset` du lake paie ce transport)
- 5 énoncés : transfert de contenance (`supportContained_pushUp_split`),
conservation des moments liftée (`coordMoment_pushUp_split_of_support`/`_last`),
lecture du support (`pushUp_split_ne_zero`), forme `{0, snoc u 0, −snoc u 0}`
(`supportContained_pushUp_split_three`)
- Consommateur mesuré : k2.6c — l'induction elle-même (`SignedSums.lean` l.44-55)
- FORMAL_STATUS.md : rangée k2.6b + agrégateur (reste k2.6c seul, déps k2.0–k2.6b)
+ dédoublonnage de la rangée k2.6 (artefact du restack #19425)
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
Rejeu de pile après absorption de Cause mesurée. La base Geste. Rejeu de la pile entière sur
Preuve de préservation. Les fichiers Lean de chaque brique sont byte-identiques avant/après rejeu (vérifié par See #17845 |
github-actions
Bot
added
the
lean-visibility-drift
|
[ADJOINT PREFLIGHT] |
|
[ADJOINT PREFLIGHT] |
… + caracterisations de support + pullback) Etend les modules Pullback FR/_en (pas de nouveau fichier) : embedding produit toRealProd (hauteur Bool -> coordonnee reelle), caracterisations de support de la scission sous P >= 0 (max -> disjonction, min -> conjonction), et le theoreme pullback lui-meme (Lemme 1.4, transposé de Komlos/Pullback.lean l.55-92) sur Finset.mem_convexHull' + Finset.abs_sum_le_sum_abs + les ingredients k2.1/k2.2/k2.3. sum_smul_inl reporte : aucun consommateur dans le port (decomposition (z, beta) via Prod.fst_sum/Prod.snd_sum). See #17845 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> (cherry picked from commit d45cba5)
…stribution + jumeau _en) Port de Komlos/Distribution.lean l.105 (module repris nom pour nom) : le barycentre coordonne-par-coordonnee d'une distribution positive de masse 1 sur S appartient a l'enveloppe du support transporte S.map toReal. Le one-liner oracle tient sur l'organe push de k2.3 (push_apply / push_mass / coordMoment_toReal) ; infrastructure sup/inf Finsupp reportee sans consommateur ; sum_smul_inl acquiert un consommateur mesure (l.53, k2.6). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> (cherry picked from commit 0c59dab)
|
Cette PR depasse le seuil de couverture review (par defaut 300 additions) et n'a recu aucune review -- ni bot, ni humaine. Le label Le label est retire au balayage suivant (quotidien) des qu'une review arrive -- dans Seuil, historique et exceptions : cf. |
github-actions
Bot
removed
the
pr-gate-missing
|
[ADJOINT PREFLIGHT] |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM — brique k2.6 vérifiée, preuve-vive réelle au head
[Hermes] — PR jamais couverte, tier âgé (créée 06/10, ~73 h). Review complète des 4 briques empilées (retarget main : k2.4 Pullback delta + k2.5 Distribution + k2.6a Lift + k2.6 SignedSums) :
sum_smul_inllu intégralement (headd851e33) : énoncé générique correct ({E : Type*} [AddCommGroup E] [Module ℝ E],∑ ε i • (v i, 0) = (∑ ε i • v i, 0)), preuveProd.ext ?_ ?_ <;> simp [Prod.smul_mk, Prod.fst_sum, Prod.snd_sum]= la décomposition canonique, toolkit identique àConvex/Combination.leanl.460 cité au body. Position vssum_smul_snoc(k2.6a) cohérente et documentée.- Preuve-vive vérifiée au check-runs
per_page=100:lean-matrix / Lean CI (discrepancy_lean)= success au headd851e33(08/10 09:44Z, 2m57s) — le build Lean a réellement tourné sur CE head (triggerpaths:couvrediscrepancy_lean, checkout = lake complet). Pas un vert hors périmètre. - Sorry-scan code : 0
sorry/admit/native_decidedans les lignes de code ajoutées (les 4 matches = prose docstring « 0 sorry »). - Jumeaux i18n :
SignedSums.leanvs_en— code byte-identique, seuls prose/namespace (KomlosvsKomlos_en,import BasicvsBasic_en) diffèrent = convention #4980 respectée. - Délétions Pullback légitimes : les −7 lignes retirent le bandeau « pullback reste reporté » devenu obsolète (k2.4 l'a livré) — pas de contenu légitime supprimé.
- Disclosure B.3 honnête : jambe d'axiomes non activée sur ce lake (
ci_lakes.jsonsans cléaxiom-target-modulespourdiscrepancy), assumée noir sur blanc au body.
Mineur (non bloquant) : le body dit « empilée sur #19089 » alors que la base est désormais main (retarget a replié k2.5+k2.6a dans ce PR) — le framing pile du body est légèrement périmé, les rangées FORMAL_STATUS documentent chaque brique correctement.
Sous clusterManager-Myia (WRITE CoursIA #15511), author=jsboige, non-auteur → verdict réel.
[Hermes hermes-pr-review, cycle :04 09/10, host 1ed7af3074fb, sig=98519677]
|
[ADJOINT PREFLIGHT] |
github-actions
Bot
removed
the
large-pr-no-review
… FORMAL_STATUS.md Conflit unique sur le tableau de statut. Resolution mesuree, pas arbitree : - aucune ligne de main n'est absente de la branche ; - la branche porte trois lignes de plus : `k2.5`, `k2.6a`, `k2.6` ; - une seule ligne commune differe, `k2`. La version de la branche recouvre celle de main (elle enregistre comme livre ce que main liste comme restant) et conserve les references `SignedSums.lean l.37-58`, `induction n`. Un fragment de main n'etait recouvert par aucune phrase de la branche et a ete reinsere a son ancrage : la justification « Fin d -> Z n'est pas un R-module ; l'oracle enonce pullback sur E ->_0 R — le transport plonge la grille dans Fin d -> R ou convexHull R parle ». Le reste du texte de main est supersede par l'etat plus recent de la branche. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
Build local
Ecart entre la tete compilee et la tete courante de la PR (rafraichissement de base depuis) :
baseline Log complet cote lane (WSL |
github-actions
Bot
removed
the
variation-adjacency-deep-med
… FORMAL_STATUS.md Conflit unique sur le registre de statut Komlos. Resolution lue, pas aveugle : le cote branche ne supprime aucune ligne de main -- le diff branche-rel.-main est N insertions / 1 suppression, et la seule ligne supprimee est la ligne k2 que la branche reecrit (elle y ajoute les livrables k2.6x et etend la colonne finale). Rien de main n est perdu. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
[RESOLUTION CONFLIT] Tete 6fbc3a7 (precedente : Merge de
Cet enchainement se reproduit a chaque deplacement de
|
github-actions
Bot
added
lean-visibility-unmeasured
|
[ADJOINT PREFLIGHT] Dossier tiers (dispatch Verdict BLOCKED, cause unique et etrangere a la PR : l'etat du parc de runners. Deux symptomes mesures, un meme fait.
Ce que les rouges ne sont pas. Le rouge est ici le scanner de secrets, meme fichier absent que sur #19089 : deux PRs, un seul fait. Les jambes rouges sont donc la meme cause repartie sur des lecteurs differents -- trois fichiers du depot manquants dans les workspaces -- et non des defauts de cette PR, qui ne touche que des fichiers B.0 -- les trois surfaces. Domaine (section B). Le temoin vivant a la tete courante est la jambe Ce que ce dossier ne fait pas. Il ne leve aucune reserve, n'approuve pas et n'autorise aucun merge ; il ne remplace pas B.0. Le deblocage de ces quatre PRs passe par la remise en etat du parc (runners epaules et non affames), pas par un geste de lane : aucune modification de la branche ne changera un fichier absent du workspace du runner. |
Le rouge de la porte n'est pas impute a ce diff — et il ne dit pas que cette PR fuit un secretLa porte ( Le rejeu du cycle precedent l'a fait passer de Pourquoi ce n'est pas un finding de secret
Ce que je ne fais pasAucun rejeu : ce rejeu-la a deja eu lieu et n'a servi qu'a remplacer un — lane |
|
Qualification de l'unique jambe rouge (lane myia-po-2025:CoursIA, 10/10) — même famille que #19089/#19445/#19464/#20227 (c.6095805634). Verdict : famille infra #20174 (workdir amputé du runner persistant), pas le diff.
Geste prévu : aucun rejeu avant la purge des slots po-2024 (arbitrage 02:28Z, échéance 10:45Z). Après purge : rejeu de la jambe à tête constante, sans ré-armer DWELL. |
|
[ADJOINT PREFLIGHT] |
myia-ai-01
left a comment
myia-ai-01
left a comment
There was a problem hiding this comment.
Approbation a la tete exacte 6fbc3a7afc (lane myia-ai-01:CoursIA).
La review Hermes de clusterManager-Myia (APPROVED, 2026-10-09T04:38:06Z, commit d851e33f17) couvre le contenu. Ce que j'ai verifie entre ce commit et la tete :
git diff d851e33f17 6fbc3a7afc -- MyIA.AI.Notebooks/Search/discrepancy_lean: seulFORMAL_STATUS.mdchange, sur une ligne (la lignek2, issue de la fusion demain). Tous les.leansont identiques a ceux qu'Hermes a lus.- les commits apres la review sont deux fusions de
origin/main; lean-matrix / Lean CI (discrepancy_lean)estsuccessa cette tete (check_run_state.py --pr 19425) ;- aucun
sorryde code dans les fichiers du diff (les occurrences sont de la prose).
Mineur, non bloquant, laisse a la lane : le body dit encore « empilee sur #19089 » alors que la base est main.
Ordre de merge : la pile Komlos est divergente (chaque branche a fusionne main de son cote). Elle se merge dans son ordre, #19089 (k2.6a) puis #19425, puis #19445, puis #19464, jamais par le sommet. Cette approbation ne vaut pas merge : il reste le rouge d'infrastructure de la famille #20174 et un dossier a cette tete.
…ept, assembly on top Conflits add/add SignedSums(.lean,_en.lean) resolus en gardant la tete de la PR (k2.6 + k2.6c, identiques a la ligne de main post-#19425 pour sum_smul_inl). FORMAL_STATUS : lignes k2.6/k2.6b/k2.6c conservees, la ligne k2 garde le parenthese explicatif de main (Fin d -> Z n'est pas un R-module), k3 re-auditee deja en zone commune, k5 au nom recent Search-09e. distinct_code_sorry 0 avant et apres (44 -> 48 fichiers : Tent/Grid k3.1-k3.2 arrives par main, 0 sorry). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…nedSums + jumeau _en) (#19464) * feat(lean,#17845): brique k2.4 -- pas complet de pullback (toRealProd + caracterisations de support + pullback) Etend les modules Pullback FR/_en (pas de nouveau fichier) : embedding produit toRealProd (hauteur Bool -> coordonnee reelle), caracterisations de support de la scission sous P >= 0 (max -> disjonction, min -> conjonction), et le theoreme pullback lui-meme (Lemme 1.4, transposé de Komlos/Pullback.lean l.55-92) sur Finset.mem_convexHull' + Finset.abs_sum_le_sum_abs + les ingredients k2.1/k2.2/k2.3. sum_smul_inl reporte : aucun consommateur dans le port (decomposition (z, beta) via Prod.fst_sum/Prod.snd_sum). See #17845 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> (cherry picked from commit d45cba5) * feat(lean,#17845): brique k2.5 -- cas de base mean_mem_convexHull (Distribution + jumeau _en) Port de Komlos/Distribution.lean l.105 (module repris nom pour nom) : le barycentre coordonne-par-coordonnee d'une distribution positive de masse 1 sur S appartient a l'enveloppe du support transporte S.map toReal. Le one-liner oracle tient sur l'organe push de k2.3 (push_apply / push_mass / coordMoment_toReal) ; infrastructure sup/inf Finsupp reportee sans consommateur ; sum_smul_inl acquiert un consommateur mesure (l.53, k2.6). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> (cherry picked from commit 0c59dab) * feat(lean,#17845): brique k2.6a -- pont de niveau liftUp/pushUp (Lift + jumeau _en) Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> (cherry picked from commit f11bc6e) * feat(lean,#17845): brique k2.6 -- sum_smul_inl generique (SignedSums + jumeau _en) Premiere brique de l'assemblage du Lemme 1.4 : nouveau module Komlos/SignedSums.lean repris nom pour nom de l'oracle gdahia/Komlos. sum_smul_inl generique en E (l'assistant du pas inductif, l.53) ; carte de genericite des organes mesuree en tete de module, voie beta close par la mesure, decision de cadre (voie alpha) consignee ouverte. lake build local deux jumeaux EXIT=0 (WSL v4.33.0, Mathlib db584cd6) ; distinct_code_sorry = 0 ; i18n 1/1 byte-identical ; FORMAL_STATUS.md rangee k2.6 + agregateur k2 (deps k2.0-k2.6). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> (cherry picked from commit bf7378c) * docs(lean,#17845): k2.6 -- decision de cadre arbitree k2.6a, position inl vs snoc La decision de cadre que la carte de genericite laissait ouverte est arbitree par la brique k2.6a (#19089, option (c) : Fin (d + k) par liftUp). sum_smul_inl se positionne comme l'organe generique R-modulaire complementaire de sum_smul_snoc (forme lake cote grille) : consommable cote transport/hull. Docstrings FR/EN + rangee FORMAL_STATUS. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> (cherry picked from commit 27b59d4) * feat(lean,#17845): brique k2.6b -- la scission sous contention dans la dimension agrandie - `Komlos/LiftSplit.lean` + jumeau `_en` : sans contrepartie oracle (le `Finsupp` transporte son support gratuitement, le cadre `Finset` du lake paie ce transport) - 5 énoncés : transfert de contenance (`supportContained_pushUp_split`), conservation des moments liftée (`coordMoment_pushUp_split_of_support`/`_last`), lecture du support (`pushUp_split_ne_zero`), forme `{0, snoc u 0, −snoc u 0}` (`supportContained_pushUp_split_three`) - Consommateur mesuré : k2.6c — l'induction elle-même (`SignedSums.lean` l.44-55) - FORMAL_STATUS.md : rangée k2.6b + agrégateur (reste k2.6c seul, déps k2.0–k2.6b) + dédoublonnage de la rangée k2.6 (artefact du restack #19425) Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> (cherry picked from commit 6044493) * feat(lean,#17845): brique k2.6c -- assemblage final Lemme 1.4 (SignedSums + jumeau _en) Dernier cran de la pile Komlos : port de l'assemblage final (induction n du Lemme 1.4) de l'oracle gdahia/Komlos (SignedSums.lean l.37-58) dans Discrepancy/Komlos/SignedSums.lean du lake discrepancy_lean. - existe_colouring_aux : porte a deux ensembles (A pour les Ecarts, A' pour l'image snoc) -- l'induction remonte l'hypothese de stabilite par liftUp. - snocReal / mem_convexHull_map_snocReal : transport de la distribution agrandie d'une dimension. - Enonce public existe_colouring (Lemme 1.4) : consommation de la porte. - Jumeau _en regenere (byte-identical, organe i18n : 1/1 pairs). - FORMAL_STATUS.md : rangee k2.6c + agregateur k2 (le k2 est clos). Validation : - lake build Discrepancy.Komlos.SignedSums Discrepancy.Komlos.SignedSums_en -> EXIT=0 - count_code_sorry.py --json : distinct_code_sorry = 0 (44 fichiers) - check_i18n_siblings.py : 1/1 pairs byte-identical, 0 drift/orphan/unbuilt - grep sorry|admit : 0 ligne dans les deux jumeaux See #17845 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> (cherry picked from commit 10ed0fa) * refactor(lean,#17845): k2.6c -- nettoyage des 5 warnings unusedSimpArgs de SignedSums Le build de la brique k2.6c (commit 716651c) etait vert mais portait 5 warnings `unusedSimpArgs` flagges par le linter sur les deux jumeaux. Le linter est empirique : il nomme l'argument a retirer, et retirer un argument flagge est sur (l'argument n'a pas ete consomme par le simp). Sites traites (chaque retrait suit la forme cible donnee par le hint) : - l.356 `exists_colouring_aux`, branche `cast` du `Fin.lastCases` : `simp [liftUp, Pi.smul_apply, smul_eq_mul]` -> `simp [liftUp, Pi.smul_apply]` - l.384 `hid1` : `simp only [..., smul_eq_mul, Pi.neg_apply]` -> sans `smul_eq_mul` - l.394 `hid3` : idem, avec `hw` conserve - l.434 `hpt`, branche `last` : `simp [hv'snoc]` -> `simp` - l.441 `hpt`, branche `cast` : `simp [hv'snoc]` -> `simp` Jumeau `SignedSums_en.lean` regenere par `mk_signedsums_en.py` : les cinq meme lignes, hors docstrings, restent byte-identiques. Validation (post-patch, sur l'arbre de travail) : - lake build Discrepancy.Komlos.SignedSums Discrepancy.Komlos.SignedSums_en -> EXIT=0, **0 warning sur les deux fichiers** (log `k26c_build11.log`, `grep -c unusedSimpArgs` = 0 ; les 4 warnings restants du log sont les `push_neg` deja declasses de `Containment_en.lean`, hors perimetre) - count_code_sorry.py --json : lake discrepancy_lean, 44 fichiers, distinct_code_sorry = **0** - check_i18n_siblings.py --all : `SignedSums_en.lean` **OK** ; verdict global 335/341 byte-identical, **0 drift / 0 orphan / 0 unbuilt** - grep sorry|admit : 0 ligne dans les deux jumeaux Aucune preuve ni enonce modifie : seuls des arguments de `simp` inutilises sont retires, les buts restent resolus par le meme `simp` sans ces arguments. See #17845 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> (cherry picked from commit 0d2ede5) --------- Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
3 participants
Grain: MED/lean — lane myia-po-2025:CoursIA — prev: DEEP/qc #19408
k2.6 brique 1 —
sum_smul_inlgénérique (assemblage Lemme 1.4)Brique de l'assemblage final de la voie élémentaire (Karingula–Lovett, #17845), empilée sur #19089 (k2.6a, pont de niveau
liftUp/pushUp). Nouveau moduleKomlos/SignedSums.lean+ jumeau_en, repris nom pour nom de l'oraclegdahia/Komlos.Livré :
sum_smul_inlgénérique —(∑ i, ε i • (v i, (0:ℝ))) = (∑ i, ε i • v i, (0:ℝ))sur{E : Type*} [AddCommGroup E] [Module ℝ E]. C'est l'assistant que l'oracle invoque au pas de l'induction (SignedSums.leanl.53 :rw [mean_split, sum_smul_inl, Prod.mk_add_mk, add_zero] at hmem) pour distribuer une somme de couples sur la première composante.Preuve :
Prod.ext ?_ ?_ <;> simp [Prod.smul_mk, Prod.fst_sum, Prod.snd_sum]— les trois noms vérifiés au pin avant le build :Prod.smul_mkenMathlib/Algebra/GroupWithZero/Action/Prod.lean,Prod.fst_sum/Prod.snd_sumversions additives (to_additive) defst_prod/snd_prodenMathlib/Algebra/BigOperators/Pi.leanl.155 — le même toolkit queMathlib/Analysis/Convex/Combination.leanl.460 utilise pour la même distribution.Position vs k2.6a (réconciliation) : la décision de cadre que la carte de généricité documentait comme ouverte est arbitrée par k2.6a (#19089, option (c) : l'espace qui grandit est réalisé
Fin (d + k) → ℤpar l'embeddingliftUp, sans re-généralisation des organes). Les deux organes sont complémentaires :sum_smul_snoc(k2.6a) est la forme lake côté grille,sum_smul_inl(ce PR) la forme générique ℝ-modulaire, consommable côté transport/hull où les moments vivent dansℝ.Carte de généricité (mesurée, en tête du module) : l'induction oracle ré-instancie ses organes à chaque niveau sur ambiant croissant
E → E × ℝ → …; les organes k2.0–k2.5 du lake sont monomorphes (Fin d → ℤ, hauteurBool). Déjà génériques :segment_repr,add_smul_mem_convexHull,sum_smul_mem_convexHull(Pullback.lean l.150/189/213).sum_smul_inlétait le seul organe du pas qui manquait. Voie β (ping-pong deux espaces) close par la mesure : le pas oracle écrit simultanément dansEetℝau même niveau d'itération.Validation
lake buildlocal ciblé (WSL, toolchain v4.33.0, Mathlibdb584cd6) : deux jumeauxDiscrepancy.Komlos.SignedSums+_enEXIT=0, 0 erreur 0 warning — initial (brique) et re-construits après la réconciliation docstring (restack sur k2.6a)python scripts/lean/count_code_sorry.py --json:distinct_code_sorry = 0(lake discrepancy_lean)python scripts/lean/check_i18n_siblings.py <SignedSums_en.lean>:1/1 pairs byte-identicalFORMAL_STATUS.md : rangée k2.6 (positionnée contre k2.6a) + agrégateur k2 (déps k2.0–k2.6, reste k2.6b/k2.6c)
B.3 (proof-integrity) : non applicable — cas (a), écrit tel quel. Le lake est bien dans la matrice CI (le job
lean-matrix / Lean CI (discrepancy_lean)tourne et est vert dessus), mais sa jambe d'axiomes n'est pas activée : le step « Proof integrity » du template matriciel est gardé parif: matrix.axiom-target-modules != '', et l'entréediscrepancydescripts/lean/ci_lakes.json(23 entrées (mesurées surorigin/mainau 07/10 : 6 déclarent la clé —sudoku,kelly,gametheory,serre100,percolation,geometry— etdiscrepancyn'en fait pas partie)) ne porte pas cette clé — la matrice interpole donc''et saute le step. Aucun autre workflow du dépôt ne couvre ce lake en axiomes (grep -l discrepancy .github/workflows/*.ymlne rend quelean-ci-matrix.yml, seul appelant de ce template). Conséquence assumée : aucun vert CI d'axiomes n'existe sur ce lake, et le build local n'en tient pas lieu.Pile
k2.5 (#19087) → k2.6a (#19089) → ce PR. La suite : k2.6b (conservation des moments sous contenance), k2.6c (lecture du pas
SignedSums.leanl.37-58 nom pour nom).See #17845
🤖 Generated with Claude Code