Repository navigation
feat(lean,#13483): tranche 14a — loi de localite evolve_union (compositionalite union disjointe) - #19042
Conversation
…itionalite union disjointe) Quatre briques sorry-free dans HashlifeMarginFragment (+ jumeau _en byte-identical) : isAlive_append_or (brique 0 ensembliste, isAlive de l'append = ou des isAlive), union_agrees_with_left, evolve_union (loi pointwise), evolve_union_mem (forme d'adhérence : q ∈ evolve t (g₁++g₂) ↔ q ∈ evolve t g₁ ∨ q ∈ evolve t g₂). La forme liste littérale est fausse pour t ≥ 1 (énumération canonique lexicographique entrelace des colonnes séparées). Pont d'ordre d'append via evolve_congr + or_comm (append non commutatif au niveau liste, couvert à t = 0 par la brique 0). Séparation stricte 2·t < d exigée (le cas d'égalité laisse la boîte toucher les deux supports). Briques : evolve_box_agree, evolve_reach_chebyshev, chebDist_triangle, chebDist_comm, evolve_congr, isAlive_true_iff_mem. Tranche 14b (transfert de capture) scoppée dans la docstring de section, non embarquée. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
github-actions
Bot
added
the
lean-visibility-drift
|
[myia-po-2026:CoursIA-3] c423 : PR #19042 -- NO-DOSSIER Tell c400 #1 strict : PR gate absent/failure/in_progress (rolled up at head, source: commits//check-runs). Aucune levee par push du secretaire possible. Lane porteuse doit pousser un commit qui reussit le PR gate (ou faire lever foo PR pour redepasser le gate au vert). |
Path-collision (organ #13359/#13615)Cette PR #19042 (
Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur |
|
[ADJOINT PREFLIGHT] |
github-actions
Bot
added
the
large-pr-no-review
|
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. |
…oire de l'union (evolve_union_hull_box) (#19271) 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>
2 participants
Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: MED/docs #19022
See #13483 (tranche 14a, compositionalité — suite du programme de landing de
hashlife_correct_margin).Ce que livre cette PR
La loi de localité manquante du lake : deux configurations aux supports séparés de plus de
2·tévoluent indépendamment — l'évolution de l'union est l'union des évolutions. C'est la brique d'assemblage des classes admises (nature mortehcap_of_still_life, oscillateurshcap_of_period{,_mod}, vaisseauxhcap_of_spaceship{,_mod}) : le contenu réel des motifs Life est une juxtaposition de pièces de ces classes.Quatre briques sorry-free dans
HashlifeMarginFragment(+ jumeau_en, preuves byte-identical) :isAlive_append_orisAlive (g₁ ++ g₂) q = (isAlive g₁ q || isAlive g₂ q)— aucune séparation exigéeunion_agrees_with_lefttd'un point proche de la partieevolve_uniontgénérations est le « ou » des états des partiesevolve_union_memq ∈ evolve t (g₁ ++ g₂) ↔ (q ∈ evolve t g₁ ∨ q ∈ evolve t g₂)Pourquoi pas la forme « liste littérale »
evolve t (g₁ ++ g₂) = evolve t g₁ ++ evolve t g₂: elle est fausse pourt ≥ 1— l'énumération canonique deevolve(ordre lexicographique,canonical_evolve_of_posde GridCanonical) entrelace les points de parties séparées partageant une colonne, là où l'append les bloque. L'ordre n'est pas préservé, seul le support l'est — et c'est le support (boîtes de trajectoire) que consomme 14b.Pont d'ordre d'append : la loi pointwise près de
g₂s'obtient surg₂ ++ g₁— le pont versg₁ ++ g₂passe parevolve_congr(adhérence identique viaList.mem_append+or_comm), invalide àt = 0au niveau liste ; le cast = 0est couvert par la brique 0 directement.Pourquoi la séparation est stricte (
2·t < d, pas≤) : au cas d'égalité, la boîte de rayonttouche les deux supports (témoin dehnearà distancetdeq, cellule deg₂à distancetde l'autre côté — distance mutuelle exactement2·t) et l'accord local échoue. Identifié pendant la conception du maillon (a), avant toute tentative de build.Preuves — briques existantes uniquement
evolve_box_agree+evolve_reach_chebyshev(LightCone),chebDist_triangle/chebDist_comm(ConeGeometry),evolve_congr(GridCanonical),isAlive_true_iff_mem. Trois cas par point : proche deg₁(accord local + mort deg₂par cône et triangulaire), proche deg₂(symétrique, via le pont d'ordre d'append ci-dessus), hors des deux cônes (tout mort,evolve_reach_chebyshevsur l'union +List.mem_append). Les lemmes BoolBool.or_false/Bool.false_orferment les cas de mort.Validation
lake build Conway.Life.HashlifeMarginFragment: SUCCESS (WSL local, incrémental)lake build Conway.Life.HashlifeMarginFragment_en: SUCCESS — preuves byte-identicalscripts/lean/check_i18n_siblings.pysurConway/Life/) : 19/19 byte-identical, 0 driftlean-conway.yml→lean-axiom.ymlavectarget-modules: "*"(dérivation des modules porteurs de sorry, incluantHashlifeMarginFragment+_en)scripts/lean/count_code_sorry.py --json:conway_leandistinct_code_sorry1 avant / 1 après (sorry-stable — lesorryde l'énoncé-cadre reste l'objet du programme)Non embarqué (par design)
jumpCapturedFde la reconstruction de l'union). Il exige la géométrie du rendu paddé (padCenter2 c).toGridvs contenu), la cloison déjà nommée par la docstring dejumpCapturedF_of_dilation(« les hypothèses h₀/hwin sont ce que la partie géométrique de L3 doit établir »). Scoping consigné dans la docstring de section de cette PR.hashlife_correct_margin_of_unionsuivra 14b (il consomme le transfert de capture pour décharger parhashlife_correct_margin_of_hcap).🤖 Generated with Claude Code