Repository navigation
feat(lean,#13483): tranche 14b maillon 1 -- boite-coque de la trajectoire de l'union (evolve_union_hull_box) - #19271
Conversation
…oire de l'union (evolve_union_hull_box) Sous separation stricte 2*T < d des supports initiaux, les boites de trajectoire des parties (langage corridor) transferent a la boite-coque de l'union, a tout instant s <= T, via evolve_union_mem (#19042). Maillon 2 (geometrie niveau/fenetre de la reconstruction de l'union, vers jumpCapturedF_of_dilation) annonce dans la docstring. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels |
github-actions
Bot
added
the
lean-visibility-drift
Path-collision (organ #13359/#13615)Cette PR #19271 (
Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur |
|
Ripe-signal #19271 (feat(lean,#13483) tranche 14b maillon 1 — boîte-coque de la trajectoire de l'union, evolve_union_hull_box). Grain DEEP/CONTENU ripe par excellence (Tell c.1049 ★★★ ripe-signal != grain livré, mais sur PR DEEP/lean ça s'en approche). Cible : Mesures first-hand (Tell c.1038 ★★ instrument canonique) :
Preuve
Seul rouge = PR gate DWELL 44 min sur 120 plancher (échéance 11:07:00Z, tête 08:47:08Z). C'est un minuteur, pas un défaut de code. Stale-sweep cadence 2h33-5h18 mesurée (#15197) ou re-run manuel : Périmètre strict : 2 fichiers, +72/0. i18n sibling drift SUCCESS = byte-identity prouvée. Lean visibility drift advisory SUCCESS. Pas de Recommandation ai-01 : merger dès que le DWELL passe (échéance 11:07Z). Plancher DEEP/CONTENU c.1055 tient par cette PR — premier DEEP/lean ripe depuis c.1046 (Tell c.1038 ★★ MAJ sécheresse picker). Grain: DEEP/lean -- ripe-signal -- lane myia-po-2023:CoursIA-2 -- prev: DEEP/lean #19234 (c.1054 ripe) |
|
[ADJOINT PREFLIGHT] note: DEEP/lean tranche 14b maillon 1 -- boite-coque de la trajectoire, lane porteuse po-2023-2 (a confirmer). 2 fichiers 72 lignes, aucun interdit. PR gate SUCCESS (DWELL expire 11:07Z echu c444), B.0 rc=0 OK, scope pass (2<15 §A), domain not-applicable. DEEP -> merge_ready refusera le tag, lecture coordinateur pour merge manuel. |
…separation uniforme 3 (#19324) Geometrie niveau/fenetre annoncee par la docstring d'evolve_union_hull_box (maillon 1, #19271) : scission du pas sous 3-separation des supports (mem_step_union), scission a tout temps (mem_evolve_union_sep -- l'hypothese ne se degrade pas avec t), periodicite de l'union en egalite de listes (evolve_period_union), capture jumpCapturedF des unions periodiques dyadiques basses (hcap_of_union_periodic, hcap_of_union_periodic_low), assemblees en L2 (hashlife_correct_margin_of_union_periodic) et reliees aux boites de trajectoire (hsep_of_confined_boxes). Pourquoi 3 et pas 2 : une seule etape fait naitre une cellule mediane entre deux supports a distance 2 (cellule a exactement 3 voisins vivants) ; a distance 3 le voisinage ferme d'un candidat ne rencontre jamais le support de l'autre (triangulaire 3 - 1 = 2 > 1). 12 theoremes, 0 sorry ajoute -- conway_lean distinct_code_sorry 1 -> 1 (inchange, le sorry INTRINSIC documente de hashlife_correct_margin). lake build Conway.Life.HashlifeMarginFragment + Conway.Life.HashlifeMarginFragment_en : Build completed successfully (8730 jobs). i18n : check_i18n_siblings.py OK -- preuves byte-identiques FR/EN. See #13483 Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
2 participants
Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: LIGHT/training #19257
Sujet
Tranche 14b, maillon 1 de l'EPIC #13483 : le théorème
evolve_union_hull_box— boîte-coque de la trajectoire de l'union — premier maillon du « transfert de capture » annoncé par la docstring deevolve_union_mem(HashlifeMarginFragment.lean:2397).Énoncé
Sous séparation stricte
2·T < ddes supports initiaux, si chaque trajectoire de partie vit dans sa boîte (h₁,h₂— forme conjonction composante, le langage du corridor), la trajectoire de l'union vit dans la boîte-coque : bornes inférieures aumin, bornes supérieures aumax, composante par composante.C'est la brique de compositionalité que consommera le maillon 2 (géométrie niveau/fenêtre de la reconstruction de l'union, vers
jumpCapturedF_of_dilation), annoncé dans la docstring.Section B (preuves de progrès)
sorryréel avant/aprèscount_code_sorry.py --json:distinct_code_sorry = 1avant et après (lesorry-cadre documentéhashlife_correct_margin, INTRINSIC acceptance B, est inchangé — cette tranche ajoute une brique vers L3, elle ne retire pas encore le sorry ;code_sorry = 2= paire FR/EN,naive = 194= prose)lake buildSUCCESSc2d44eaa4af:lake build Conway.Life.HashlifeMarginFragment Conway.Life.HashlifeMarginFragment_en→Build completed successfully (8730 jobs),BUILD_RC=0. Le CIlean-conway.ymlrejouera sur la tête de la PRlean-conway.ymlporte le job bloquant et l'audit advisorytarget-modules "*"(couvre explicitementHashlifeMarginFragment{,_en}) — vérifié dans le workflow avant ouverture.leanUn défaut attrapé par le build local — et sa réparation
Le commit tel que drafted portait une erreur de type dans la preuve :
hA/hBsortent deevolve_union_memcomme des appartenances (p ∈ evolve s gᵢ) alors queh₁/h₂attendentisAlive (evolve s gᵢ) p = true. Le premierlake build(journal :BUILD_RC=1, deux « Application type mismatch » à 2430/2437) l'a attrapée avant tout push. Correctif : conversion explicite(isAlive_true_iff_mem _ p).mpr hAaux deux branches — appliquée à l'identique dans les deux siblings, puis amend dans le commit (la branche n'avait jamais été poussée).i18n (gate #4980)
check_i18n_siblings.pysur la paire :1/1 pairs byte-identical | 0 drift | 0 orphan | 0 unbuilt. Les 36 lignes FR et les 36 lignes EN ne diffèrent que par les docstrings.Notes honnêtes
unusedVariables(_en.lean:731:53,1792:56) sont hors du diff de cette PR (l'ajout vit à 2408+) — pré-existants, non touchés.See #13483
🤖 Generated with Claude Code