Repository navigation
[Lean][GOL] Recadrage Gosper : prouver evolveHashlifeFastAtN inconditionnel (étape 2, #6724) — la capture devient corollaire #11161
Description
Activity
[CLAIMED] lane myia-po-2025:CoursIA -- recadrage Gosper : evolveHashlifeFastAtN inconditionnel (dispatch ai-01 c.108) -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/**
(check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative. Release with
[RELEASED]when your PR lands.)[RELEASED] lane myia-po-2025:CoursIA -- grain 1 livre : PR #11257 (gridFrameN_frame_invariant + gridFrameN_level_ge_two + frame_jumpAt_capture_centered, FR+EN #4980, lake build SUCCESS, 0 sorry, check_i18n 17/17). Le claim reste detenu pour grain 2 (induction de fuel evolveHashlifeFastAtAuxN) et grain 3 (signature inconditionnelle evolveHashlifeFastAtN n g = evolve n g).
[RELEASED] lane myia-po-2025:CoursIA — grain 2 livre : PR #11281 (squelette induction fuel
evolveHashlifeFastAtAuxN_correct+evolveHashlifeFastAtN_correctsousOneJumpAtCorrect, 0 nouveau sorry, 4 temoins #eval true dont line7 n=8 et glider n=12 deux sauts).Claim RETENU pour le grain 3 (decharge de
OneJumpAtCorrect: P4-AthashlifeResultAt+ pont localite + invariant du cadre grain 1) — paths: MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/*.lean- added a commit that references this issue
on Aug 16, 2026 - added a commit that references this issue
on Aug 16, 2026 - added 6 commits that reference this issue
on Aug 16, 2026 - added a commit that references this issue
on Aug 16, 2026 [CLAIMED] lane myia-po-2024:CoursIA -- grain 3b : decharge de OneJumpAtCorrect (P4-At hashlifeResultAt + pont localite + invariant cadre grain 1) -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/** Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: MED/notebook-python #11345 (dispatch coord DM 2026-08-16T22:33Z, check_lane_claim CLEAR firsthand 2026-08-17T01:15Z)
- added a commit that references this issue
on Aug 16, 2026 20 remaining items
Tranche 4 livree dans #11407 (commit pousse DANS feature/11161-grain3b-env16, conformement au DM file Actions) : hashlifeResultAt_step_converse_mem — direction CONVERSE (RHS->LHS) du pas inductif, miroir exact du forward de la tranche 3.
Enonce : sous l'hypothese d'induction forte hIH (les 9 briques n_i de niveau M satisfont la fenetre centrale), tout point p de l'evolue 2^j du parent restreint a la fenetre [2^(M-1), 2^M) appartient a la sortie mono-ronde At lue a l'ancre centrale (2^(M-1), 2^(M-1)) — l'inclusion inverse qui complete l'equivalence point par point du pas inductif.
Chaine : mem_restrictGridTo.mp hp -> hpalive (bridge isAlive sur l'evolue du parent) -> reduction du but (unfold + hashlifeResultAtAux_succ_node_at + if_neg + hrw1..9) -> refine (out16_toGrid_mem ...).mpr (construction constructive de la disjonction 16-voies) -> split positionnel 16 cas (rcases lt_or_ge imbriques, fenetre [2S, 6S)^2) -> par tuile : call-site au bras factorise.
Refactor Path B (lecon tranche 4) : la version tuiles inline echouait par TIMEOUT d'elaboration (>= 2M heartbeats sur les by_cases portant evolve (2^j) ((node ...).toGrid (0,0)) concret — corps de tuile re-elabore 16 fois sans type attendu). Fix : 4 bras step_converse_arm_{se,sw,ne,nw} (signature (hj) (n r) (o1 o2 x y) (cg) (p) hrw hrl href hih hagree hXY hbox hpalive : p in (subX r).toGrid (x, y)), corps commun factorise (hS, hS0, hAc, rw Nat.cast_pow 2 (M-2) at hih, hQalive, hQmem by_cases+exfalso, hQrest mem_restrictGridTo.mpr <;> omega, hQsub mem_toGrid_shift.mp + Prod.ext <;> omega, conclusion subX_toGrid_mem.mpr) ; les 16 tuiles deviennent des call-sites a 3 bullets (hagree = nX_evolve_agree (j := j) ... (by omega) ; hXY et hbox = combinator first|omega|constructor<;>first|omega|trivial|skip SANS prefixe simp — sur goals pure npow le simp ne fait pas de progres et first retombe sur skip avec "No goals to be solved"). Meme pattern que step_forward_arm_* (5d).
Lecons d'elaboration consolidees (detail body PR) : ancres coercees ((2^k : Nat)) vs npow ((2^k : Int)) — pont propositionnel Nat.cast_pow, normalise par hSc/hAc + rw ; asymetrie forward/converse : le forward consomme hih via rw [← hih] suivi d'un exact qui absorbe la difference coercee/npow par defeq (rw brut indifferent), la converse via rw [hih] directionnel contre un but npow propre est SYNTAXIQUE et exige un hSc ASCRIBE (le rw brut produit l'ancre base-cast ↑2^(M-2), desunifiable) ; shapes de bullets des 16 call-sites normalisees au format valide par le forward (continuation a exact+2, pipes a first+2 — la generation initiale les mettait a la meme colonne, erreur de parse unexpected token 'by' en cascade) ; j implicite de nX_evolve_agree passe explicitement (j := j) sinon omega voit 2^?m non assigne ; t1 (subSE, ancre (A,A)) : simp only [Int.sub_zero, Prod.mk.eta] at hQ AVANT simp [isAlive, hQ] (eta-collapse du point local).
Validation : lake env lean EXIT 0 reel (wrapper REAL_EXIT, log complet sans | tail), lake build -Kjobs=2 EXIT 0 (fallback -Kjobs=1 sur std::bad_alloc/exit 3221226505), distinct_code_sorry conway = 1 inchange (invariant ai-01 tenu). B.3 : cablage lean-axiom conway inchange (aucun sorry ajoute/retire).
Residuel grain 3b : induction forte -> hashlifeResultAt_central_correct -> chainage OneJumpAtCorrect. See #11161
Tranche 5 livree sur la branche
feature/11161-grain3b-t5(commit c06f785, stackee sur #11407, PAS de PR - DM ai-01 file Actions, la livraison attend le merge de #11407 ou un feu vert) : hashlifeResultAt_central_correct - l'induction P4-At elle-meme, pur assemblage. +83 lignes.Enonce (k-forme sans soustraction) :
forall k c, c.wf = true -> c.level = j + 2 + k -> (hashlifeResultAt j c).toGrid (2^(j+k), 2^(j+k)) = restrictGridTo (evolve (2^j) (c.toGrid (0,0))) (2^(j+k)) (2^(j+k+1))- induction ORDINAIRE sur k suffit (l'IH est universellement quantifiee sur la cellule, donc re-instantiable sur les neuf briques).Assemblage : base k=0 =
hashlifeResultAt_base_central(deja sur main, moteur plein a fuel sature) ; pas k+1 = exposition des 16 petits-enfants parhnode+ rfl en cascade, les deux directions du pas inductifhashlifeResultAt_step_forward_mem(5f) +hashlifeResultAt_step_converse_mem(5g) aM := j+k+2avechIH':= l'IH re-ecrite dans la forme exacteM-2/M-1, reliees en egalite de grille par le pontp4at_ext_bridgeaM := j+k+3(la biconditionnelle point par point est exactement forward-then-converse, appliquee partiellementhfw p/hcv pau constructeur anonyme de l'iff).Lecon d'elaboration 1 (capture de sous-terme par rw total) : les normalisations d'exposants
M-2<-> forme propre ne sont PAS defeq, donc chaque passage se fait parrwdirectionnel SYNTAXIQUE - unrw [a = b] at hreecrit TOUTES les occurrences deadansh, y compris imbriquees dans le resultat d'un rw precedent. Rewriterj+k+1 -> j+k+2-1(taille) puisj+k -> j+k+2-2(ancre) corrompt la taille. Remede : les rw sur le BUT dans le sens M-forme -> forme propre (motifs disjoints), les plus GRANDS motifs en premier quand une inclusion existe (j+(k+1)+1avantj+(k+1)).Lecon d'elaboration 2 (rcases sur cellWf OPAQUE apres subst) : decomposer
cellWf_of_wf _ hwfparobtain ⟨..., noms⟩apres le dance hnode+rfl introduit les 7 champs inaccessibles (✝) - les noms du pattern ne se lient PAS, quel que soit le pattern (nomme, wildcard, have explicite sans trou - isole par probes minimaux avec trace_state). Pivot : extraire les trois egalites de niveau DIRECTEMENT du wf Bool transparent, technique de la preuve decellWf_of_wfelle-meme (Foundation) :have hAB : A.level = B.level := by simp_all [MacroCell.wf, beq_iff_eq]. Les temoinscellWfdes enfants ne sont pas nommes au passage - inutiles ici : forward/converse consomment le wf du PARENT, les wf des briques vivent dans l'IH universellement quantifiee.Validation :
lake env leanEXIT 0 reel, 0 erreur, 0 sorry (log complet ~/t5_c8.log, sans | tail) ;lake build -Kjobs=2complet EXIT 0 (8723 jobs, 0 erreur) ;count_code_sorry.py --jsondistinct_code_sorry conway = 1 inchange (residuel MarginFragment, INTRINSIC #9568). B.3 : cablage lean-axiom conway inchange (aucun sorry ajoute/retire).Note infra (le jour meme) : le pont 9p WSL->/mnt/d a gele 3x en serie (thread p9_client_rpc fige, read_bytes delta 0) - les compiles ont ete basculees sur ext4 natif WSL : copie du lake + robocopy des 8,5 Go de packages reels via
\\wsl.localhost(direction 9p inverse, saine), LEAN_PATH 100% ext4 verifie par /proc//environ. Les logs c6-c8 sont les preuves d'execution (ext4, toolchain v4.32.0 identique).Residuel grain 3b : derivation de
OneJumpAtCorrectinconditionnel depuishashlifeResultAt_central_correct(re-signature, grain 3 de l'issue) ->evolveHashlifeFastAtN_correctinconditionnel. See #11161- added a commit that references this issue
on Aug 17, 2026 Tranche 6 livree sur la branche
feature/11161-grain3b-t5(commit 61b6924, stackee sur c06f785 / #11407) : grain 3 complet — derivation inconditionnelle deOneJumpAtCorrect+ capstoneevolveHashlifeFastAtN_correct_uncond(l'hypothesehbrdu squelette grain 2 est dechargee : pour TOUT n et TOUTE grille,evolveHashlifeFastAtN n g = evolve n g). +265 lignes, 0 sorry ajoute.Les 4 theoremes :
-
mem_toGrid_gridToMacroCellWithOffsetN'(private) : miroir N de BR1 (MacroCell L861) — cases hF : gridFrameN n g, simp [gridToMacroCellWithOffsetN, hF, MacroCell.toGrid, mem_sortDedup], mem_toCellsAux_buildFromGrid + gridFrameN_contains_g. Byte-miroir de la preuve non-N. -
hashlifeJumpAt_correct_uncond(private) : miroir de hashlifeJump_correct_of_captured (L6494) OU la capture est remplacee par un argument de cone de lumiere. InstantiationhashlifeResultAt_central_correct (lvl-2) 2 (padCenter2 c)(tranche 5) : fenetre centrale ancre (2^lvl, 2^lvl), restrict [2^lvl, 2^lvl + 2^(lvl+1)). Depot du restrict parrestrictGridTo_eq_selfSANS capture : tout point vivant du evolve 2^(lvl-2) a un ancetre vivant (evolve_reach_chebyshev, portee Chebyshev <= 2^(lvl-2)) dans le contenu — boite [32^(lvl-1), 52^(lvl-1)) via padCenter2_toGrid_shift + mem_toGrid_extent — d'ou point dans [5X, 11X) ⊂ [4X, 12X) avec X = 2^(lvl-2). La marge geometrique 2^(lvl-1) couvre DEUX FOIS la portee 2^(lvl-2). Arithmetique : coord_bound_of_chebDist_le (ConeGeometry) + normalisations npow/cast vers l'atome X, omega ferme. -
one_jumpAt_toGrid_correct(private) : miroir de one_jump_toGrid_correct (L6517) SANS hcap — l'algebre de decalages (hnew/jumpResultOff, hmc0/toGrid_shift_grid, chaine rw, hz1/hz2) est byte-identique : la geometrie de jumpResultOff ne depend pas de la taille du saut. -
one_jumpAt_correct+evolveHashlifeFastAtN_correct_uncond: derivation (intro n g, cases hF : gridFrameN n g, hun + pont BR1-N, buildFromGrid_wf, application de 3) puis capstoneevolveHashlifeFastAtN_correct one_jumpAt_correct n g.
C'est la fermeture du re-cadrage Gosper : la capture (jumpCaptured) etait un artefact du moteur mono-ronde ORIGINAL, pas une propriete du monde — le moteur decorrele n-aware la rend theoreme gratuit.
Validation : compile
lake env leanEXIT 0 reel, 0 erreur ;lake build -Kjobs=2complet EXIT 0 ;count_code_sorry.py --jsondistinct_code_sorry conway = 1 inchange (residuel MarginFragment, INTRINSIC #9568). B.3 : cablage lean-axiom conway inchange.Logs : ~/t6_c1.log (fichier), ~/lake_t6_full.log (build). See #11161
-
- added a commit that references this issue
on Aug 17, 2026 [RELEASED] lane myia-po-2024:CoursIA-2 -- released
- added a commit that references this issue
on Aug 18, 2026 - added a commit that references this issue
on Aug 19, 2026 [CLAIMED] lane myia-po-2025:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeCorrectness.lean
Grain: DEEP/lean — lane myia-po-2025:CoursIA-2 — prev: MED/notebook-python #11774Livraison des tranches 5+6 (ecrites le 2026-08-17 sur cette machine, tenues jusqu'au merge de #11407 -- condition du DM ai-01 satisfaite : merge 653d1d5 le 2026-08-19T04:55Z). Branche rebasee frais sur origin/main (cherry-picks c06f785 + 61b6924, les tranches 1-4 tombent en vide = deja sur main via squash 653d1d5). Claim herite de la lane CoursIA de cette meme machine (grain 3b 2026-08-17T06:06Z + [OVERRIDE] ai-01 2026-08-17T04:20Z).
[RELEASED] lane myia-po-2025:CoursIA-2 -- PR #11781 (tranches 5+6 : hashlifeResultAt_central_correct + one_jumpAt_correct + capstone evolveHashlifeFastAtN_correct_uncond).
Libere AUSSI le claim grain 3b de la lane soeur myia-po-2025:CoursIA (2026-08-17T06:06Z, meme machine) : le grain 3b est complet — l'acceptance de #11161 est entierement couverte (build EXIT 0 frais, sorries 0->0, 4 temoins true, arithmetique jumpAt_capture_centered sur main via #11407). La PR porte Closes #11161.
- added a commit that references this issue
on Aug 19, 2026 [INFO] candidate-delivered + release de claim (Tell c.1356 strict) — lane myia-po-2026:CoursIA-2
Le picker sert #11161 comme grain neuf. Confrontation body ↔ main (verification first-hand L1356) :
Grain "manquant" du corps d'origine : la re-signature inconditionnelle
evolveHashlifeFastN n g = evolve n g(l'acceptance explicite du body, point 3).Mesure sur
origin/main:MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/Hashlife.leanligne 513 :theorem evolveHashlifeFastN_eq_evolve (n : Nat) (g : Grid) : evolveHashlifeFastN n g = evolve n g := by cases n with | zero => rfl | succ m => exact evolveHashlifeFastAuxN_eq_evolve (m + 1) (m + 1) g (by omega)
Signature inconditionnelle (aucune hypothese de capture), preuve par induction sur n. La PR #10973 (lane myia-po-2026:CoursIA, merge 2026-08-14T17:40:36Z) a livre ce theoreme comme grain 3a (b2') de l'EPIC : elle demontre par ailleurs que le garde de saut N3 est structurellement mort (
gridToMacroCellWithOffsetN_level_gt_n), ce qui rend la preservation VACUE et livre gratuitement le pont — plus fort que le pontn <= 2initialement reporte (cf. body de la PR, lignes detaillees).Recadrage Gosper (5 PRs mergées au total) : #11257 (grain 1, capture du saut decorele inconditionnelle), #11281 (grain 2, squelette induction fuel), #11303 (grain 3a, socle hashlifeResultAt_base_central), #11781 (grain 3 complet, OneJumpAtCorrect theoreme + capstone), #18645 (doc). Body d'origine 2026-08-16 obsolet sur le point 3 — livre depuis 2026-08-14, deux jours plus tot.
Conclusion : la re-signature inconditionnelle est livree sur main, l'EPIC #11161 est complet. Aucune modification a apporter ; le corps d'origine date et consigne mal. La fermeture reste signee coordinateur/adjoint (R6/lane
delivered).
[Lean][GOL] Recadrage Gosper : prouver
evolveHashlifeFastAtNinconditionnel (étape 2, #6724) — la capture devient corollaireContexte
no_padding_depth_suffices(#6724, JumpCapture.lean) prouve que le rembourrage ne peut pas refermer la capture dans le cadrage standard (saut2^lvldepuis une cellule de niveaulvl) : le rembourrage augmente la cellule ET le saut à parts égales, le rapport marge/portée reste1 − 2^(1-p) < 1, le déficit = demi-largeur du contenu, constant en p. La seule voie restante est la décorrélation portée/niveau (paramètrejde Gosper) : sauter2^jindépendamment du niveauM ≥ j+2. Avecj = lvl-2, la marge (2^(lvl-1)+pad) excède la portée (2^(lvl-2)) — la capture cesse d'être une hypothèse.C'est l'étape 2 annoncée dans
JumpCapture.lean(note « Marges nommées » : « Cette étape 2 fera l'objet d'une PR distincte »). Cette issue est la traduction concrète de la discussion session user du 2026-08-16 (« le théorème général est faux (clip), pas dur — un moteur re-cadré le rend atteignable »).État sur main (VERIFIE, main
2c391cc0e)La machinerie est déjà committée dans
Conway/Life/Hashlife.lean:hashlifeResultAt j: avance exactement2^jgénérations, indépendant du niveau de la cellule (fenêtre centrale2^(M-1)àt = 2^j, demi-largeur2^(M-2)excédant la portée d'un facteur2^(M-2-j)).hashlifeJumpAt,jumpSizeAt lvl = 2^(lvl-2),evolveHashlifeFastAtAuxN,evolveHashlifeFastAtN.jumpAt_capture_centeredPROUVÉ (théorème, sorry-free) : sousB + 2·pad ≤ 2^lvletlvl ≥ 2, la marge gauche2^(lvl-1)+padet la marge droite3·2^(lvl-1)−pad−Bcouvrent chacune la portée2^(lvl-2)— la capture du saut est un corollaire de l'invariant du cadre.guardAt_viable_gliderPROUVÉ : le garde décorrélé TIRE (glider n=8, lvl=5,jumpSizeAt 5 = 2^3 = 8 ≤ 8), contra du garde plein (b2) mort pour toute grille.Manquant : la correction globale
evolveHashlifeFastAtN n g = evolve n g(aucun théorème ne l'énonce encore dansHashlife.lean).Grains
gridToMacroCellWithOffsetN n gsatisfaitB + 2·pad ≤ 2^lvlà chaque itération (ou documenter où c'est déjà acquis par la construction du cadre).evolveHashlifeFastAux_correct(feat(lean,#6724): DISCHARGE p5_large_n_jumpN — fuel induction + trajectory-capture re-signing (b3') #11007) — induction sur le fuel, invariantn ≤ fuel, bras saut = brique un-saut (jumpAt_capture_centeredà la place de l'hypothèse∀ t ≤ n) + IH ré-instantiée ent + js+ recompositionevolve_add.hashlife_correctNsans hypothèse de capture — le théorème initial le plus général revient.Bénéfice / coût
2^(lvl-2)au lieu de2^lvl— plus de niveaux pour la même distance temporelle. C'est la convention standard de hashlife (Gosper) : le moteur actuel sautait trop loin par rapport à sa fenêtre. L'accélération reste exponentielle ; le compromis est à documenter dans le body de la PR.Acceptance
lake build Conway SUCCESS(WSL ou natif, règle B pr-review-discipline)grep -cE '^\s*sorry\s*$': HashlifeCorrectness 0 → 0 (aucun nouveau sorry)evolveHashlifeFastAtN 8 glider = evolve 8 glider, blinker,lineCell3(le témoin qui falsifiait le moteur plein doit passer sur le moteur décorrélé)jumpAt_capture_centered:2^(lvl-2) ≤ 2^(lvl-1)+pad ∧ 2^(lvl-2) ≤ 3·2^(lvl-1)−pad−B) + verdict b3'See #6724 (Epic) · #11007 (squelette induction + re-signature trajectoire, à adapter) · #9568 (cribleur : cribler les énoncés du recadrage AVANT leur figement)