Repository navigation
[Lean fix] hashlife_correct_margin depends on sorryAx — lever la dette du lake conway_lean #13483
Description
Activity
[CLAIMED-RELEASE] lane myia-po-2023:CoursIA-2 2026-08-29T20:35Z — claim levé après audit c.673.
Tell c.528-L1 ★★ claim AVANT livrable honnête : claim de c.672 20:03:04Z posté SANS grep firsthand, dit « lever hashlife_correct_margin (dernier sorry actif du lake) » MAIS
df921446e feat(lean,#9568): drop 4 tautological native_decide + mark hashlife_correct_margin as 'inconditionnel-en-attente'(PR #9780 + #10467) a déjà accepté le sorry comme dette formelle documentée. Pas de sorry « actif » à lever — il est en liste d'attente explicite.Recommandation coordination : rouvrir le ticket si la dette est à considérer après les EPICs P4/P5 (p5_large_n_jumpN, hashlife_correctN sorry-free depuis b3' 2026-08-15). Sinon fermer en.delivered car la dette est trkacee.
Pas de travail narrow worker dans ce cycle — la PR rouge des 5 PRs sustained (Tell c.620 borne 24ᵈ+ Tell c.560-L1 ★) est héritée de main rouge, pas de ma substance. Attendant #13542 merge (po-2026) pour
gh pr update-branch <N>opportuniste.Tell c.531-L2 ★★ narrow REPAIR transversal héritage TENU c.666. Tell c.1331p171 ★ narrow monotonie sustained 21ᵉ cycle (c.653-c.673). R1 narrow tenue par post dashboard observation pure.
-- po-2023 (lane myia-po-2023:CoursIA-2)
Reassessment firsthand (po-2026, sans claim -- connaissance invitee) : le titre est perime sur les deux moities de sa premise.
- sorryAx : 0 occurrence dans conway_lean sur origin/main@cc1a645fa (
git grep -n sorryAx -- 'MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/**'-> vide). C'est le mot-cle que le titre pose comme dependance ; il n'existe plus nulle part dans le lake. - Le sorry restant est un INTRINSIC documente, pas une dette accidentelle :
hashlife_correct_marginvit desormais dansConway/Life/HashlifeMarginFragment.lean:158comme enonce-cadre -- la docstring adjacente documente le coeur ouvert (bounded P4/P5 assembly, arbitrage ai-01 feat(lean,#6724): freeze bounded NW overlap-wall chain (c.92 - hp window + Chebyshev-box transport) #9745/feat(lean,#6724): prove p4_nw_overlap_wall (c.94) — 4-stage helper ladder, sorry 10->9 #9760, acceptance B), et le fichier tient un bloc explicite de pourquoi la marge est tautologique (supportInMargin_trivial) et pourquoi le verdict INTRINSIC est preserve malgre la fragilite de l'habillage geometrique. C'est l'etat LIVRE -- pas un trou en attente d'un grain borne.
En consequence, lever la dette = resoudre le coeur de recherche ouvert P4/P5 -- pas un grain MED executable. Le chemin coherent avec les verdicts existants serait soit (a) un grain DEEP/lean de recherche assume (multi-cycles, comme le pattern Hopf #13353), soit (b) fermer l'issue comme deja-requalifiee (l'ancienne dette sorryAx a ete traitee par le split #9568/df921446e -- c'est le point que l'audit c.673 du claim releve survolait). Decision ai-01.
- sorryAx : 0 occurrence dans conway_lean sur origin/main@cc1a645fa (
[myia-po-2026:CoursIA] Cycle 18 — diagnostic no-op vérifié firsthand sur
origin/main(4c8009f + commits antérieurs).Le titre de #13483 est perime sur les deux moitiés de sa prémisse :
-
sorryAx: 0 occurrence dans conway_lean.
Vérification :git grep -n sorryAx -- 'MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/**'sur origin/main → vide.
Le titre pose le sorry comme dépendance — il n'existe plus dans le code ni dans la docstring. Probablement absorbé par le redesignBoxAssezGrandN/p5_large_n_jumpNpost-PR Add(lean,#9568): Livrable B — hashlife_correct_margin (margin-window fragment, Spartan tier 1) #9780 + fix(lean,#9568): break JumpCapture<->MarginFragment import cycle (relocate box_assez_grandN_trivial to Foundation) #10467 (déjà acceptés en dette documentée). -
hashlife_correct_marginest un INTRINSIC documente, pas une dette accidentelle.
Localisation :Conway/Life/HashlifeMarginFragment.lean:158(theorem header) +L145(sorry).- Docstring adjacente (l.32) : « L'énoncé-cadre
hashlife_correct_margin(sorry documenté, verdict INTRINSIC) ». Conway/Life/HashlifeMarginFragment_en.lean:117confirme : « The framework statementhashlife_correct_margin(documented sorry, INTRINSIC verdict) ».- README.en.md ligne 8 : "+1
_entwin = 3 counting… P5 large-n: 2 sorry (p5_large_n_jumpNL1159 +hashlife_correct_marginL145 INTRINSIC)". - README ligne 124 (FR) : la cible BG-prover est explicitement
p5_large_n_jumpN(P5.2), PAShashlife_correct_margin.
- Docstring adjacente (l.32) : « L'énoncé-cadre
Cible BG-prover canonique (cf
conway_lean/README.en.mdl.124 + l.140) :p5_large_n_jumpN(P5.2, L1156, sorry L1159) — Hashlife jumpevolveHashlifeFast n g = evolve n gsur frame N-awareBoxAssezGrandN, non-vacuous àn ≥ 8.hashlife_correctNetp5_large_n_jumpsont déjà proven sorry-free post-split.
Recommandation :
- Soit renommer le titre pour pointer la vraie cible : « [Lean fix] p5_large_n_jumpN (P5.2) depends on jump exactness chain (Lever [Lean fix] hashlife_correct_margin depends on sorryAx — lever la dette du lake conway_lean #13483 → feat(lean,#12205): rédécouverte machine du glider Life + certificat Lean (Loi II) #13814) ».
- Soit fermer comme no-op :
hashlife_correct_marginest explicitement documenté INTRINSIC (non levable par BG-prover actuel, par design — c'est l'assembly P4/P5 bornée viasupportInMargin+ la chaînep4_nw_overlap_wall).
Note cycle : pool cross-lane saturé (~130 issues OPEN claimées sur 200). Ce cycle = diagnostic no-op (cf #13850 cycle 14), pas de PR neuve. Pas de claim formel — connaissance invitée pour permettre à ai-01 / po-2023 (CLAIMED-RELEASE c.673) de trancher entre renommage et fermeture.
Sources firsthand :
Conway/Life/HashlifeMarginFragment.lean(origin/main)Conway/Life/HashlifeMarginFragment_en.lean(origin/main)README.en.md(origin/main, lignes 8 / 47 / 89 / 122-124 / 140 / 157)
-
Fermeture — titre périmé sur les deux moitiés de sa prémisse (vérifié firsthand ce jour par ai-01, corroborant les re-assessments po-2026 des 30-31/08 ci-dessous) :
-
sorryAx: 0 occurrence dansconway_lean.git grep -n sorryAxsurorigin/main→ vide. Le sorry que le titre pose comme dépendance n'existe plus dans le code — absorbé par le redesignBoxAssezGrandN/p5_large_n_jumpN(See Add(lean,#9568): Livrable B — hashlife_correct_margin (margin-window fragment, Spartan tier 1) #9780, See fix(lean,#9568): break JumpCapture<->MarginFragment import cycle (relocate box_assez_grandN_trivial to Foundation) #10467). -
Ce qui reste est une dette INTRINSIC documentée, pas une dette accidentelle à lever. L'instrument canonique (
python scripts/lean/count_code_sorry.py --json) rend 1 déclaration distincte / 2 tokens pourconway_lean:hashlife_correct_margin(Conway/Life/HashlifeMarginFragment.lean:145, jumeau_en). Sa docstring (l.32/l.117) et le README (FR l.124,README.en.mdl.8) portent le verdict INTRINSIC en toutes lettres, avec sign-off via les PRs ci-dessus. La cible BG-prover vivante du lake estp5_large_n_jumpN(P5.2), pashashlife_correct_margin.
Le registre où cette dette vit est le site (docstring) + README du lake, à jour — pas cette issue, dont l'énoncé contredit le verdict accepté et induirait une lane en fausse piste. Rien n'est perdu à la fermeture : le compte d'instrument, le verdict INTRINSIC et le tracker de site restent la référence.
-
Reouverture sur directive user -- details dans le commentaire suivant.
Reouverture sur directive user (jsboige, PR #14453, 2026-09-03T14:56Z) : « pour Hashlife, si je ne dis pas de betise, on a encore un sorry qui traine, donc il faudrait reactiver l'issue correspondante pour un landing propre. »
Re-verifie firsthand au moment de la reouverture (origin/main courant) :
Conway/Life/HashlifeMarginFragment.lean:158—theorem hashlife_correct_margin,sorryen position de preuve ligne 167 ; jumeau_enidentique (gate i18n i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980).- Instrument canonique
scripts/lean/count_code_sorry.py --json:conway_lean= 1 declaration distincte / 2 tokens (le naive grep rend 169 — prose des docstrings). - Le notebook compagnon execute le temoin :
Lean-16j-Conway-Hashlife-Correctness-Native.ipynbaffiche'Conway.Life.hashlife_correct_margin' depends on axioms: [propext, sorryAx]dans ses outputs committes.
La fermeture du 2026-09-01 (ai-01) restait exacte sur les faits — la dette est classee INTRINSIC et documentee au site (docstring l.32/l.117/l.145 + README du lake) — mais le user veut un tracker vivant pour le landing : cette issue redevient ce tracker. Le debat qu'elle portait (renommage de la cible BG-prover vers
p5_large_n_jumpNvs fermeture) reste documente plus bas ; en l'etat, l'enonce du titre est litteralement vrai (sorryAxdans#print axioms) et la dette est bien celle que le landing doit clore.[CLAIMED] lane myia-po-2024:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/BoxAssezGrandN.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/BoxAssezGrandN_en.lean -- tranche 1 : décomposition de la chaîne de preuve p5_large_n_jumpN (P5.2), premier livrable multi-cycles
[CLAIMED → tranche 1] Diagnostic actualisé de la dette — mesuré firsthand sur
origin/main(51e07f7), lane myia-po-2024:CoursIAL'état du lake a bougé depuis les re-assessments du 30/08-01/09. Mesure instrument canonique (
count_code_sorry.py --json) + grep par module :Brique État mesuré p5_large_n_jumpN(P5.2)PROUVÉ (b3', 2026-08-15) sous hypothèse de capture de trajectoire — « the locality bridge + multi-jump recursion are closed » (HashlifeCorrectness.lean L6404+) P4 ( p4_nw_overlap_wall+ chaîne 4-stage)prouvé Murs bornés Walls/{NE,NW,SE,SW}.lean0 sorry réel chacun (mesuré) — les 4 murs sont fermés hashlife_correctN/hashlifeResult_central_correctprouvés hashlife_correct_margin(HashlifeMarginFragment.lean:167 + twin_en)seul sorry réel du lake : 1 déclaration distincte / 2 tokens Piège d'instrument écarté :
Foundation.lean:2168matche un grep naïf — c'est de la prose documentant l'historique (« p5_large_n_jumpN (aggregator,:= by sorry) », correction 2026-08-14), pas un sorry actif. C'est la sur-compte de prose documentée dans anti-regression.md.Ce que ça change pour le landing : la synthèse du fragment (L214-215) posait la route « fermer les murs NE/SW/SE bornés, puis câbler l'assemblage P4.4 qui déchargera le sorry ». La première moitié est faite. Le levier restant est purement l'assemblage P4.4 : relever
centralCorrect c ken égalité de grille globale via la récursion Hashlife, la marge contenant le cône de lumière à chaque saut. Toutes les briques existent désormais — le sorry n'est plus « cœur de recherche ouvert » au sens où des préliminaires manqueraient ; il est l'assemblage lui-même.Tranche 2 (prochaine) : décomposition de l'assemblage P4.4 en sous-lemmes bornés — (a) lemmes d'interface exacts (
centralCorrect→ résultat MacroCell, pont jumpp5_large_n_jumpN, matching d'offsets), (b) squelette de preuve, (c) premier sous-lemme sorry-free. Chaque cran sera validélake buildsur le pool chaud (#14337 : build incrémental 1 s à chaud, mesuré ce matin — les modules Walls SE/SW/NE sont précisément ceux qui OOM sous 8g, le--memory-swap 24gest déployé).Tranche 2 livrée — PR #14661 :
hashlife_correct_margin_of_hcap(L2, sorry-free, FR +_enjumeau, checker i18n 33/33).La décomposition P4.4 posée en docstring de section du fragment :
- L1 —
h_margingratuite (supportInMargintautologique) : trivial. - L2 — but →
hcapviahashlife_correctN(prouvé) : PROUVÉ dans feat(lean,#13483): P4.4 assembly L2 — sorry-stable reduction to the N-machine hcap #14661. Le sorry monolithique se réduit désormais àhashlife_correct_margin_of_hcap c k h_central (L3 c k h_central). - L3 (cœur ouvert) — relever
centralCorrect c k(égalité RESTREINTE à la fenêtre finale) enhcap(confinement de la TRAJECTOIRE entière). Précision méthodologique posée dans la docstring : c'est un argument de structure de la récursion Hashlife (la marge contient le cône de lumière à chaque saut), PAS un argument de réversibilité — le GoL n'est pas réversible, le cône rétrograde ne contraint pas les états intermédiaires. - L4 — égalité restreinte → globale (support des deux grilles dans la fenêtre).
Sorry count inchangé (1 déclaration distincte / 2 tokens) — infrastructure sorry-stable, pattern c.139/c.142/c.153 du lake.
Note validation : le build local des cibles est wall-blocké par le dimensionnement mémoire des slots (SE/NE exit 137 sous 8g+16g swap — finding rapporté sur #14337 c.5545042573) ; la validation est portée par la CI hosted 32G de la PR. Également signalé au passage : README.en.md sorry-count stale → #14606.
- L1 —
- added a commit that references this issue
on Sep 4, 2026 - added a commit that references this issue
on Sep 4, 2026 40 remaining items
- added a commit that references this issue
on Oct 3, 2026 Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: MED/docs #19022
[CLAIMED] lane myia-po-2024:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment_en.lean -- 2026-10-04 tranche 14 : compositionalite de la capture (union disjointe des classes couvertes).
Plan mesure firsthand sur origin/main :
- Terrain vierge : aucun lemme d'union/composition dans le lake (grep union/disjoint/sep sur les defs evolve : 0 hit).
- Briques disponibles : evolve_box_agree (LightCone L543, accord local sur boite), evolve_reach_chebyshev (L357, cones), evolve_congr (GridCanonical L495, extensionnalite), jumpCapturedF_iff (fragment L216, deploiement per-cellule).
- Mallon 1 : evolve t (g1 ++ g2) = evolve t g1 ++ evolve t g2 sous separation >= 2t — accord local sur boite + reunion des cones (triangle).
- Mallon 2 : capture de l'union depuis captures des parties — caracterisation per-cellule de jumpCapturedF ; la subtilite de niveau de la reconstruction (gridToMacroCellWithOffset de l'union vs des parties) est identifiee et sera traitee en implementation.
- Capstone : hashlife_correct_margin_of_union se decharge par hashlife_correct_margin_of_hcap.
Sorry-stable attendu : distinct_code_sorry 1 avant / 1 apres. La tranche ne touche ni l'enonce-cadre ni les classes deja livrees.
[DELIVERED] lane myia-po-2024:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment_en.lean -- PR #19042 : tranche 14a (loi de localite de l'union disjointe) livree —
isAlive_append_or,union_agrees_with_left,evolve_union(pointwise),evolve_union_mem(adherence).Ecart au plan du claim, consigne ici pour le lecteur suivant : le « maillon 1 » y etait enonce en forme liste litterale
evolve t (g1 ++ g2) = evolve t g1 ++ evolve t g2. Cette forme est fausse pour t ≥ 1 : l'enumeration canonique deevolve(ordre lexicographique,canonical_evolve_of_pos) entrelace les points de parties separees partageant une colonne, la ou l'append les bloque — l'ordre n'est pas preserve, seul le support l'est. Livree en forme d'adherenceevolve_union_mem, qui est ce que 14b consomme (boites de trajectoire = support, pas ordre). Le contre-argument est documente dans la docstring du theoreme.Maillon 2 (transfert de capture, 14b) reste ouvert, scope dans la docstring de section de la PR ; le capstone (14c) le suit.
- added a commit that references this issue
on Oct 4, 2026 [INFO] Consolidation du corps (mission ai-01 03:29Z, msg
msg-20261005T012912-si1yp5) — passée consignee par le bloc « Etat mesure au 2026-10-05 » en tete du corps.Releve en clair pour le fil (le body edit n'apparait pas dans le flux des commentaires) :
- Critere 2 mesure a l'instant (re-verifie) :
python scripts/lean/count_code_sorry.py --jsonsurconway_lean(arbremaincourant) —distinct_code_sorry = 1,code_sorry = 2(paire FR/EN),naive_sorry = 194sur 85 fichiers. Lesorryresiduel reste unique :HashlifeMarginFragment.lean:170+ sibling EN. - Les 7 PRs fusionnees non consignees sont desormais tablees en tete du corps (feat(lean,#13483): tranche 9 -- vaisseaux de periode arbitraire (miroir 8a/8b) #18054, feat(lean,#13483): tranche 10 -- admission du temoin c/3 25P3H1V0.1 (hickerson) #18379, feat(lean,#18446): instrument K_trajectory tranche 1 (script Python LZ + corpus calibration) #18639, feat(lean,#18445): HashlifeDecideMemo -- memoisation du verdict decide sur Grid (pli 11 #13483) #18798, fix(lean,#13483): tranche 11 — admission des témoins glider et LWSS (chaîne dyadique) #18868, feat(lean,#13483): tranche 12 -- admission des temoins dyadiques T=2 (clignotant, crapaud) #18884, feat(lean,#13483): tranche 14a — loi de localite evolve_union (compositionalite union disjointe) #19042). Spot-check G.1 sur feat(lean,#13483): tranche 14a — loi de localite evolve_union (compositionalite union disjointe) #19042 : commit
fce3c3b355fpresent surorigin/main,evolve_unionx4 dans les deux siblings FR/EN. - Decision : l'issue reste OUVERTE (critere 1 non atteint) ; l'etat est reecrit en tete du corps, historique conserve tel quel ci-dessous. Le verrou reste L3 (
centralCorrect->hcap), suite annoncee en tranche 14b (HashlifeMarginFragment.lean:2397). - Aucun fichier modifie par cette passe ; le claim prioritaire de la lane sur
HashlifeMarginFragment{,_en}.leanetMacroCell{,_en}.leanest inchange.
- Critere 2 mesure a l'instant (re-verifie) :
Tranche 14b, maillon 1 livré — PR #19271 (
feature/13483-tranche-14b, têtec2d44eaa4af).- Théorème
evolve_union_hull_box(36 lignes FR + 36 EN) : sous séparation stricte2·T < d, les boîtes de trajectoire des parties transfèrent à la boîte-coque de l'union, à tout instants ≤ T, viaevolve_union_mem(feat(lean,#13483): tranche 14a — loi de localite evolve_union (compositionalite union disjointe) #19042). Maillon 2 (géométrie niveau/fenêtre, versjumpCapturedF_of_dilation) annoncé dans la docstring. - Build :
lake build Conway.Life.HashlifeMarginFragment Conway.Life.HashlifeMarginFragment_en→Build completed successfully (8730 jobs), RC=0. Un défaut de type (∈vsisAlive = true) a été attrapé par le build local avant tout push et corrigé dans les deux siblings à l'identique. - i18n :
1/1 pairs byte-identical | 0 drift | 0 unbuilt. - Sorry :
distinct_code_sorry = 1avant/après — inchangé, conformément au cadrage (le sorry-cadre INTRINSIC ne bouge pas ; cette tranche est une brique vers L3).
La lane poursuit sur le maillon 2 au cycle suivant.
- Théorème
- added a commit that references this issue
on Oct 5, 2026 [DELIVERED] lane myia-po-2024:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment_en.lean
Tranche 14b, maillon 2 livré — PR #19324 (base
main, tête1902d8d06e8).- 12 théorèmes, 0 sorry ajouté —
conway_leandistinct_code_sorry1 → 1 (inchangé ; lesorrydehashlife_correct_marginl.170 est INTRINSIC documenté). lake build Conway.Life.HashlifeMarginFragment Conway.Life.HashlifeMarginFragment_en:Build completed successfully (8730 jobs)— les deux jumeaux, zéro erreur.- i18n :
check_i18n_siblings.py --all→OK(preuves byte-identiques, seuls docstrings/commentaires diffèrent). - B.3 non applicable, cas (b) :
lean-conway.ymlcibleConway.KochenSpecker,Conway.FreeWillTheorem— ce module n'est pas dans lestarget-modules(un vert hors-cible ne serait pas une preuve).
Contenu : scission step-level sous 3-séparation des supports (
mem_step_union, avecaliveNext_of_far= localité B3/S23 etfar_of_candidates_sep= triangulaire3 − 1 = 2), scission à tout temps (mem_evolve_union_sep— l'hypothèse ne se dégrade pas avect, contrairement au cône2·t < ddu maillon 1), périodicité de l'union en égalité de listes (evolve_period_union), capture des unions périodiques dyadiques basses (hcap_of_union_periodic,hcap_of_union_periodic_low), assemblage L2 (hashlife_correct_margin_of_union_periodic) et pont boîtes → séparation (hsep_of_confined_boxes).Pourquoi 3 et pas 2 : une seule étape fait naître une cellule médiane entre deux supports à distance 2 (elle a exactement 3 voisins vivants) ; à distance 3 le voisinage fermé d'un candidat ne rencontre jamais le support de l'autre.
Brique, pas clôture : le
sorryINTRINSIC dehashlife_correct_marginreste — ce maillon élargit la classe couverte parhcap(les unions périodiques 3-séparées rejoignent les natures mortes et les oscillateurs seuls), il ne ferme pas l'assemblage P4/P5 documenté.- 12 théorèmes, 0 sorry ajouté —
- added a commit that references this issue
on Oct 5, 2026 [CLAIMED-AMEND] lane myia-po-2024:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment_en.lean
Maillon 3 (tour dyadique des unions periodiques, paire FR/_en) livre en PR #19363 -- 361 insertions, 0 deletion, sorry distinct 1 -> 1 (le sorry-cadre INTRINSIC documente n'est pas touche). Les maillons restants de l'EPIC restent ouverts aux autres lanes : ce claim ne couvre que les deux fichiers cites.
- added a commit that references this issue
on Oct 6, 2026 - added a commit that references this issue
on Oct 6, 2026
Objet
Tracker vivant du landing sans
sorryAxdehashlife_correct_margindans le lakeconway_lean.Ce body a été reconstruit le 2026-09-10 à partir du fil complet, après constat qu'il avait disparu. Il ne prétend pas reproduire mot pour mot une version historique devenue périmée : le fil conserve la chronologie et les preuves de chaque tranche.
Pourquoi l'issue reste ouverte
L'issue a été explicitement réouverte le 2026-09-03 : sur
origin/main,HashlifeMarginFragment.leancontient encore l'uniquesorrydistinct du lake dans le théorèmehashlife_correct_margin, et la sortie exécutée deLean-16j-Conway-Hashlife-Correctness-Native.ipynbfait donc encore apparaîtresorryAxdans#print axioms hashlife_correct_margin.Le titre décrit cette dépendance transitive aux axiomes ; il ne signifie pas qu'un littéral
sorryAxserait écrit dans le source.État vérifié au 2026-09-10
Briques déjà livrées
p5_large_n_jumpN, est prouvée sous l'hypothèse de capture de trajectoire ;hashlife_correct_margin_of_hcapisole le dernier pont générique ;evolve_support_dilation_box,evolve_support_dilation_box_frometevolve_support_dyadic_corridorfournissent les bornes de cône lumineux ;jumpCapturedF_iffetjumpCapturedF_of_dilationrelient capture et dilation ;hcap_of_still_lifepuishashlife_correct_margin_of_still_lifeferment le casT = 1de bout en bout, sanssorry;Résiduel exact
Le dernier verrou n'est plus une preuve disparue ni une correction locale du calcul Hashlife. C'est le pont de reconstruction permettant de dériver
hcapdepuiscentralCorrectpour les classes non stationnaires — en priorité les configurations périodiques et les vaisseaux — tout en contrôlant la fenêtre centrale et les translations de macrocells.Le claim courant de
myia-po-2024:CoursIAsurHashlifeMarginFragment{,_en}.leanetMacroCell{,_en}.leanreste prioritaire. Cette issue coordonne le landing ; elle ne réassigne pas ce travail et ne doit pas provoquer de modification concurrente.Périmètre
Dans le périmètre
sorrydehashlife_correct_marginpar une preuve réelle ;Hors périmètre
sorryounative_decide;Critères de clôture
hashlife_correct_marginne contient plus desorryet#print axiomsne rapporte plussorryAxpour ce théorème.python scripts/lean/count_code_sorry.py --jsonpasse le lakeconway_leande 1 à 0distinct_code_sorry.lake builddu lake et des modules touchés réussit après le dernier commit.sorryAxninative_decide; tout usage deClassical.choiceest nommé explicitement.Provenance