feat(lean,#13483): tranche 12 -- admission des temoins dyadiques T=2 (clignotant, crapaud)

[jsboige]

Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: MED/tooling #18872

Résumé

Tranche 12 du programme de levée du dernier sorry distinct de conway_lean (hashlife_correct_margin, Conway/Life/HashlifeMarginFragment.lean) : admission des deux témoins dyadiques T = 2 de la classe périodique que la docstring de hashlife_correct_margin_of_period annonçait nommément — le clignotant (« clignotant T = 2 ») et le crapaud (« crapaud T = 2 »). Le pulsar (tranche 8b) couvrait la partie non dyadique (T = 3) ; ces deux-là fermaient la liste annoncée.

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

• blinker_hcap_of_period : ∀ t, jumpCapturedF (gridToMacroCellWithOffset (evolve t blinker_h)).2 = true ;
• toad_hcap_of_period : ∀ t, jumpCapturedF (gridToMacroCellWithOffset (evolve t toad)).2 = true.

Support par témoin : canonicalité (blinker_h_canonical, blinker_v_canonical, toad_canonical, toadP2_canonical), périodes par le noyau (blinker_period_two_kernel, toad_period_two_kernel : composition des équations de step), faits de cadre (blinker_frame_off/lvl (-2,-2) niv 3 ; blinkerV_frame_off/lvl (-1,-3) niv 3 ; toad_frame_off/lvl (-2,-2) niv 3 ; toadP2_frame_off/lvl (-2,-3) niv 3) et hdiv (divisibilité de la période sur les deux phases, clos par le noyau).

Admissibilité : pourquoi la chaîne dyadique directe suffit

hcap_of_period exige T ∣ 2^level où level est le niveau du cadre de reconstruction. Pour T = 2, cette prémisse est acquise dès que level ≥ 1 : toute puissance de deux ≥ 2 est divisible par 2. Les quatre cadres mesurés sont de niveau 3 — le relâchement par containment hcap_of_period_mod (requis pour le pulsar, T = 3 ne divisant aucune puissance de 2) n'est pas utilisé ici.

Preuve

• Périodes par le noyau, pas par le bestiaire Bool : blinker_period_two et toad_period_two rendent isOscillator g 2 = true, une forme Bool qui ne fournit pas l'égalité evolve 2 g = g exigée par hcap_of_period. Les équations de step sont re-prouvées par decide (blinker_h_step, blinker_v_step, toad_step, toadP2_step) puis composées.
• Définitions réutilisées : les phases 0 sont celles du bestiaire Conway.Life (blinker_h L206, blinker_v L209, toad L212) ; le seul littéral neuf est la seconde phase du crapaud (toadP2), validé avant le build par simulation Python indépendante (règle de B3 applicative : mesure de la discrimination avant le claim), puis clos par decide.
• 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).
• B.3 (proof-integrity) : non applicable, cas (b) — le job lean-axiom est câblé sur ce lake (lean-conway.yml L129) mais ses target-modules (Conway.KochenSpecker,Conway.FreeWillTheorem) n'atteignent pas Conway.Life.HashlifeMarginFragment : un vert serait hors-cible. Aucun axiome n'est ajouté par la tranche (preuves decide + interval_cases uniquement).

$ lake exe cache get
Already decompressed 8690 file(s)   # cache Mathlib intact via jonction, rien a telecharger
$ lake build Conway.Life.HashlifeMarginFragment
warning: HashlifeMarginFragment.lean:160:8: declaration uses `sorry`   # le sorry framework preexistant (L160), hors tranche
Build completed successfully (8721 jobs).
BUILD_FR_RC=0
$ lake build Conway.Life.HashlifeMarginFragment_en
Build completed successfully (8721 jobs).
BUILD_EN_RC=0

(Built FR 427 s / EN 404 s ; warnings residuels = lint des modules preexistants, aucun sur les lignes de la tranche.)

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-12 couvrent strictement les classes d'objets du théorème).

🤖 Generated with Claude Code

[jsboige]

Justification écrite du rouge PR gate (imputé à la base, pas réparable par cette lane) : la seule jambe en échec est Scripts Tests (CPU) — le témoin Actuariat 810 == 795 / 900 == 885 déjà confirmé sur main, corroboré par #18857, #18872, #18876 et #18882 au même instant. Le correctif est en vol : #18880 (issue #18875, lane po-2027). Rien à reparer sur ce diff (conway_lean seul) ; la jambe repassera au rafraîchissement de base ou au merge du correctif.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #18884 (feat(lean,#13483): tranche 12 -- admission des temoins dyadiques T=2 (clignotant, crapaud)) 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.

• fort -- fix(lean,#13483): tranche 11 — admission des témoins glider et LWSS (chaîne dyadique) #18868 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment_en.lean (issues communes : [Lean fix] hashlife_correct_margin depends on sorryAx — lever la dette du lake conway_lean #13483)

[jsboige]

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

note: Dossier c387 sur PR #18884 (feat(lean,#13483): tranche 12 -- admission des temoins dyadiques T=2 -- clignotant + crapaud). Lane porteuse myia-po-2024:CoursIA (tierce attestation). DEEP/lean -- hors perimetre merge_ready.py mais eligible merge a la main par ai-01 (regle skill). 2 fichiers MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment{.lean,_en.lean} +336/-0 -- sibling pair FR/EN conforme a la regle #4980. PR gate SUCCESS (PASS -- no failing checks, tete 3df650d). B.0 clear (0 nit non leve ; 1 commentaire non evalue post-fix, non bloquant). Scope pass (2 fichiers .lean sous conway_lean/, pas sous .claude/ ni .github/). domain: pass (substance preuves Lean core : 2 capstones sans sorry, sans axiome ajoute, par hcap_of_period). Cible prioritaire c387 : body tres riche avec preuve concrete (blinker_hcap_of_period, toad_hcap_of_period), DEEP/lean propre -- ai-01 peut merger a la main sur la base de ce dossier.