Repository navigation
Gorard #19741 — greffe lot Serre100 (06 + 10) #19747
Description
Activity
Grain: MED/notebook-lean — lane myia-po-2023:CoursIA — prev: DEEP/qc #19670
[CLAIMED] lot Serre100 (06 + 10) — greffe markdown des trois cellules du plan de distillation #19741 (issuecomment-6042350850) :
Carnet Cellule Timestamp Serre100/10-empilements-borne-lp-cohn-elkiesc271e800(index 17)0:02:04 Serre100/10-empilements-borne-lp-cohn-elkiesec0c5c65(index 10)0:01:54 Serre100/06-bulles-minkowskicell-16(index 17)0:00:00 et 0:00:24 Aucune cellule de code modifiee : greffe markdown-only, exception C.2 (pas de re-execution due).
Deconfliction vérifiée :
Serre100/06a deja recu une greffe de la chaine Borcherds (#18366) encell-14(index 15). La cible ici estcell-16, la cellule voisine — les deux greffes sont compatibles et ne se recouvrent pas.Verification de claim passee :
check_lane_claim.py 19747 --lane myia-po-2023:CoursIA --paths <les deux carnets>-> CLEAR.See #19741
[INFO] lane myia-po-2023:CoursIA — greffe livrée, PR #19753 (porte
Closes #19747).Correction des index de ce body, pour la lane qui relira le grain. Les index cités dans le tableau ci-dessus ont dérivé de +1 :
mainporte maintenant 25 cellules dans10-empilements-borne-lp-cohn-elkies, oùc271e800est en index 18 (et non 17) etec0c5c65en index 11 (et non 10). Les ids sont stables : c'est la bonne clé d'ancrage, et c'est ce que la greffe a utilisé.cell-16du carnet 06 n'a pas bougé (index 17).Même remarque pour les quatre grains frères (#19748, #19749, #19750, #19751) : ancrer sur l'id, vérifier l'index au moment d'écrire.
Deux grains frères sont bloqués à l'instant de ce commentaire, par des PRs ouvertes d'une autre lane sur leurs carnets : #19749 (
Lean-34, PRs #19564 et #19446 demyia-po-2024:CoursIA-2) et #19750 (Lean-16a). La vérification de claim les a rendus BLOCKED, aucun n'a été édité.Les trois cellules de ce grain sont livrées, markdown-only (exception C.2). Preuves et organes : PR #19753.
- added a commit that references this issue
on Oct 8, 2026
Grain de livraison de la chaîne Gorard (#19741) — plan de distillation : issuecomment-6042350850.
Lot Serre100 (06 + 10)
Serre100/10-empilements-borne-lp-cohn-elkiesc271e800(index 17, « Lecture du résultat — et la frontière en dimensions 8 et 24 »)Serre100/10-empilements-borne-lp-cohn-elkiesec0c5c65(index 10, « Certification : fermer chaque intervalle, borner chaque queue »)Serre100/06-bulles-minkowskicell-16(index 17, « Lecture : E8 est 32x au-dessus de la borne »)Deconfliction.
Serre100/06a deja recu une greffe de la chaine Borcherds (#18366) encell-14(index 15, « §5 Dimensions hautes : le trou contre-intuitif »), posant le lien formes modulaires <-> empilements. La cible ici estcell-16, la cellule voisine : les deux greffes sont compatibles, mais celle-ci apporte l'achevement formel de la preuve de 2016, pas le lien aux formes modulaires. Ne pas les fusionner.Matiere mesuree a l'etape 3 : les solveurs de
lanyonaietablissent des proprietes de schema numerique, et la preuve d'empilement de dimension 8 est le cas d'ecole de l'entretien (0:01:54-0:02:04). Le rapport avec la borne de Cohn-Elkies du carnet 10 est direct.Forme : paraphrase + renvoi
[mm:ss], citations courtes sourcees. Markdown-only (exception C.2 — aucune cellule de code modifiee, donc pas de re-execution due).See #19741 · See #16334