fix(lean,#13483): tranche 11 — admission des témoins glider et LWSS (chaîne dyadique)

[jsboige]

Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: MED/notebook-python #18859

Résumé

Tranche 11 du programme de levée du dernier sorry distinct de conway_lean (hashlife_correct_margin, Conway/Life/HashlifeMarginFragment.lean) : admission des deux témoins phares que la docstring de hashlife_correct_margin_of_spaceship annonçait nommément — le glider (p = 4, v = (1, -1), « la vérifie strictement ») et le LWSS (p = 4, v = (0, 2), « atteint la borne exactement »).

Deux capstones, sans sorry, sans native_decide, sans axiome ajouté, tous deux par la chaîne dyadique hcap_of_spaceship :

• glider_hcap_of_spaceship : ∀ t, jumpCapturedF (gridToMacroCellWithOffset (evolve t glider)).2 = true ;
• lwss_hcap_of_spaceship : ∀ t, jumpCapturedF (gridToMacroCellWithOffset (evolve t lwss)).2 = true.

Support par témoin : canonicalité et relation de vaisseau (glider_canonical, glider_ship4, lwss_canonical, lwss_ship4), faits de cadre (*_frame_off/lvl : niveau 3, côté 7, pour le glider ; niveau 4, côté 9, pour le LWSS) et hdiv (divisibilité de la période sur les quatre phases, clos par le noyau).

Admissibilité : pourquoi la chaîne dyadique couvre les deux

hcap_of_spaceship exige 4 ∣ 2^level où level est le niveau du cadre de reconstruction. Pour p = 4 = 2², cette prémisse est acquise dès que level ≥ log₂ p = 2 : 2^2 = 4, 2^3 = 8, 2^4 = 16 sont tous divisibles par 4. Les deux témoins satisfont donc directement la chaîne : niveaux mesurés 3 (glider) et 4 (LWSS), tous deux ≥ 2. Le relâchement par containment de la tranche 9 (hcap_of_spaceship_mod, requis pour les périodes non dyadiques comme le pulsar p = 3 et 25P3H1V0.1 p = 3) n'est pas requis ici — ce sont des témoins de période 4.

Preuve

• Pont Bool→Prop sans axiome : les témoins isSpaceship du bestiaire (Life.glider_spaceship, PatternTour.lwss_is_spaceship) sont certifiés par le noyau (decide) ; le transport en égalité de listes est beq_iff_eq (loi LawfulBEq) — aucun native_decide, aucune Classical.choice ajoutée.
• hdiv par noyau : interval_cases sur les quatre phases puis decide (calcul fini, grilles de 5 cellules) — même forme que lwss_hdiv, avec set_option maxRecDepth pour les phases du glider.
• lake build Conway.Life.HashlifeMarginFragment Conway.Life.HashlifeMarginFragment_en : SUCCESS (log ci-dessous).
• i18n : paire FR/EN Pattern A — check_i18n_siblings.py sur Conway/Life : 19/19 byte-identical, 0 drift.
• count_code_sorry.py --json : distinct_code_sorry 1 avant / 1 après — la tranche ajoute du contenu sorry-free ; le dernier sorry (hashlife_correct_margin) reste, c'est l'objet du programme ([Lean fix] hashlife_correct_margin depends on sorryAx — lever la dette du lake conway_lean #13483).

$ lake build Conway.Life.HashlifeMarginFragment Conway.Life.HashlifeMarginFragment_en
[... replay du graphe de dépendances (8730 jobs) ...]
Build completed successfully (8730 jobs).
RC=0 — 0 erreur

Périmètre

• MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment.lean
• MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment_en.lean

See #13483 — livraison partielle : le sorry de hashlife_correct_margin reste (L4 global, cœur recherche documenté ; les tranches 1-11 couvrent strictement les classes d'objets du théorème).

🤖 Generated with Claude Code

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #18868 (fix(lean,#13483): tranche 11 — admission des témoins glider et LWSS (chaîne dyadique)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• terminal -- feat(lean,#13483): tranche 12 -- admission des temoins dyadiques T=2 (clignotant, crapaud) #18884 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment_en.lean, recouvrement de chemins 100% -- feat(lean,#13483): tranche 12 -- admission des temoins dyadiques T=2 (clignotant, crapaud) #18884 est deja sur main. (issues communes : [Lean fix] hashlife_correct_margin depends on sorryAx — lever la dette du lake conway_lean #13483) (issues communes : [Lean fix] hashlife_correct_margin depends on sorryAx — lever la dette du lake conway_lean #13483)

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18868
head: 254155b
complete: true
body: read
comments-reviewed: 1
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: ed1df226231c5c519870dbdb2c89c18b5c65dd2a81929155e98bbaf332e0f508
diff-files: 2
diff-additions: 187
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

note: Dossier c397 sur PR #18868 (fix(lean,#13483) tranche 11 -- admission des temoins glider). Lane porteuse myia-po-2024:CoursIA (tierce attestation). DEEP/lean, 2 fichiers MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment{.lean,_en.lean} +94/-0 +93/-0 = +187/-0. Sibling pair FR/EN conforme #4980 (FR + EN byte-identique hors docstrings). PR gate SUCCESS 2026-10-02T20:48:56Z. B.0 clear (rc=0, 0 nit non leve). Scope pass (2 .lean sous conway_lean/Conway/Life/, PAS sous .claude/, .github/, ni CLAUDE.md). domain: pass (substance Lean tranche 11 EPIC #13483, substance distincte de #18884 tranche 12, signal advisory adjacence lean->lean du guard §2 -- tranches distinctes substance distincte, jugement non mecanisable OK). Cible READY : substance prete, B.0 clear, gate SUCCESS. DEEP merge_ready v2 refuse auto mais merge manuel ai-01 OK. Note : #18884 (c387 READY) et #18868 touchent les memes fichiers, signal c387 -- item 28. Substance distincte : tranche 11 (temoins glider) vs tranche 12 (temoins dyadiques T=2). Ai-01 tranche l'ordre. Eligible merge manuel direct par ai-01 sur gate rc=0.