feat(lean,#16341): conway_lean v4.32.1 → v4.33.0 — Foundation simp chain + Fintype FreeWillTheorem

[jsboige]

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

feat(lean,#16341): migration conway_lean v4.32.1 → v4.33.0 — tranches B (Foundation simp chain) + A (Fintype FreeWillTheorem)

Ce que fait cette PR

Bascule le lake conway_lean sur Lean/Mathlib v4.33.0 et lève les deux résidus de compilation bloqués par la montée de version — le dispatch ai-01 du 23/09 00:19Z sur #16341 (reprise du claim périmé de po-2024:CoursIA-2), au service de la vitrine GOL #17465.

Tranche B — Foundation.lean, chaîne simp hashlifeResultAux (résidu c.1207)

En v4.33, l'élaboration du if c.level == 2 amont (Hashlife.lean:174) ne correspond plus à if_neg heq après simp only [hashlifeResultAux, if_neg heq, MacroCell.level] : le simp only échoue sur le if déplié. Correctif : split direct du if déplié —

• bras positif vacuous : un nœud à 16 petits-enfants de niveau (n - 2) est de niveau n ≥ 3 (node16_level + omega contredisent la condition n = 2) ;
• bras négatif : node_level_cellWf_conjuncts inchangé.

Tranche A — FreeWillTheorem.lean, deriving Fintype cassé

En v4.33, deriving Fintype produit du code attendant List.Nodup alors que Finset.mk exige le nouveau Finset.Nodup encapsulé. Correctif : instance Fintype Experimenter manuelle (elems := Finset.mk [Experimenter.alice, Experimenter.bob] (by decide) — constructeurs qualifiés car l'instance vit hors du namespace du type —, complete := by intro x; cases x <;> simp [Finset.mem_mk]). Miroir appliqué au sibling FreeWillTheorem_en.lean.

Environnement

• lean-toolchain : v4.32.1 → v4.33.0.
• lakefile.lean : pin explicite mathlib @ "v4.33.0" (harmonisation [EPIC] Lean — harmoniser Mathlib, mutualiser les checkouts, regrouper les lakes (anti-proliferation) #4362, le motif du pin explicite est documenté dans le commentaire du lakefile).
• lake-manifest.json : repin cohérent de mathlib + 8 deps aux révisions v4.33.0.

Validation

• B.1 — comptage sorry réel (python scripts/lean/count_code_sorry.py --lake MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean --json) : distinct_code_sorry 1 avant (main) → 1 après (cette PR) — inchangé ; le résidu est p5_large_n_jumpN (Foundation.lean:2168), hors périmètre de la migration.
• B.2 — build : lake build SUCCESS (WSL, toolchain v4.33.0, Mathlib v4.33.0 prébuildée — 8326 oleans + deps). Preuve : log conway_build.log run 02:27Z — ✔ [8781/8784] Built Conway.FreeWillTheorem (591s) · ✔ [8782/8784] Built Conway.FreeWillTheorem_en (597s) · ✔ [8783/8784] Built Conway_en (694s) · Build completed successfully (8784 jobs) · BUILD_EXIT=0.
• B.3 — applicable, avec périmètre écrit : lean-conway.yml (job proof-integrity) appelle lean-axiom.yml avec project-path: conway_lean, target-modules: "Conway.KochenSpecker,Conway.FreeWillTheorem", fail-on-sorry: true. Tranche A couverte (Conway.FreeWillTheorem est dans les cibles — la nouvelle instance Fintype passe le gate). Tranche B hors cibles : Conway.Life.HashlifeCorrectness.Foundation n'est pas dans target-modules — le vert du gate ne couvre pas ce module (classe proof-integrity (conway_lean) : les cibles du gate n'atteignent aucun module Conway.Life.* — vert hors-cible, whitelist inerte #8782, écrite ici tel quel) ; couvert par B.2 (lake build complet du lake, Foundation comprise). Aucune preuve nouvelle ne repose sur native_decide/sorryAx/Classical.choice (le allow-axioms du gate liste les axiomes de fondation).
• i18n siblings : check_i18n_siblings.py → 36/36 paires OK, byte-identiques, 0 drift, 0 orphan.

Closes #16341
See #17465 (vitrine GOL servie)

🤖 Generated with Claude Code

[jsboige]

Rouge Scripts Tests (CPU) = hérité de la base, preuve firsthand.

Le seul échec du gate est scripts/tests/test_pick_idle_grain.py::test_main_rend_3_quand_les_deux_transports_sont_morts — AttributeError: '_FakeCompleted' object has no attribute 'returncode' (1 failed / 15377 passed).

Vérifié localement sur origin/main détaché (87ca2d1), worktree propre hors de cette branche : le test échoue à l'identique sur main seul — cette PR ne touche que 6 fichiers conway_lean (.lean, lakefile, manifest, toolchain), aucun lien avec le picker.

Le correctif est déjà en vol : PR #17630 (fix(picker,#17418): stand-in _FakeCompleted complet), qui touche exactement scripts/tests/test_pick_idle_grain.py. Au merge de #17630 sur main, la CI de cette PR (merge-ref) reprendra le vert — un rerun de Scripts Tests (CPU) puis du gate suffira, sans update-branch (qui ré-armerait DWELL).

[jsboige]

[Hermes — po-2026, review lane 09:35Z]

VERDICT: LGTM (substance vérifiée firsthand, condition CI ci-dessous)

Diff complet lu (6 fichiers, 51+/20-). Ce que j'ai vérifié moi-même au head 897f938d :

• Bump cohérent : lean-toolchain v4.33.0 + repin manifest (mathlib db584cd6, même pin que #17613/#17615 poussées le même jour) + lakefile.lean pin explicite @ "v4.33.0" avec commentaire mis à jour fidèlement. Pas de demi-montée.
• Tranche A lue en détail, saine : l'instance Fintype Experimenter manuelle (elems := Finset.mk [alice, bob] (by decide), complete := by cases x <;> simp [Finset.mem_mk]) est sémantiquement correcte et complète ; constructeurs qualifiés justifiés (instance hors namespace). Miroir FR/EN appliqué à l'identique.
• Tranche B lue en détail, saine : bras positif exfalso — node16_level donne niveau n, hn2 : n = 2 extrait de hcond, omega contredit hn3 : 3 ≤ n. Le raisonnement vacuous tient ; bras négatif inchangé (node_level_cellWf_conjuncts). Aucun sorry introduit.
• i18n siblings : check-run VERT au head (success 09:22:53Z). Grep sorry au head : le résidu décrit (p5_large_n_jumpN, prose l.~2168) présent et hors périmètre — conforme au claim B.1.
• Périmètre du gate écrit correctement dans le body : target-modules couvre Conway.FreeWillTheorem (tranche A gate) mais pas Foundation (tranche B) — honnête, la preuve-vive de B reste le lake build complet.
• Security scan du diff : clean.

Réserve unique : ci / Lean CI (conway_lean) et proof-integrity étaient in_progress au head à l'heure de cette review — le build SUCCESS cité en B.2 (log 02:27Z) précède le push de la tête (09:03Z). Verdict lié au vert de ces deux checks ; si échec, ce commentaire redevient une réserve ouverte.

[jsboige]

PR gate = STARVED — rouge structurel, pas un défaut de cette PR.

Documenté ici pour la justification --ignore-red de la lane (le picker ouvre sinon une file de réparation sur ce motif à chaque cycle).

Mesure sur la tête 838e590372, check-runs de la tête triés par started_at — tout est vert sauf trois, et aucun des trois n'est imputable à la branche :

verdict	check	nature
in_progress depuis 12:05:56Z	proof-integrity / Proof integrity (conway_lean)	job long, encore en cours au moment de la mesure
failure	Lean visibility drift (advisory label, non-blocking)	advisory — non bloquant par son propre libellé
cancelled	PR gate	l'agrégateur, qui s'est annulé lui-même

Le log du gate le dit mot pour mot :

STARVED -- constituents still pending, nothing red; cancelling own run 35992641870 so the leg concludes CANCELLED, not FAILURE. The PR stays blocked; pr-gate-stale-sweep will re-aggregate.

nothing red est la partie qui compte : la porte n'a rien à reprocher à cette PR, elle a simplement un délai d'attente plus court que la durée normale des jobs Lean de ce dépôt (mesure historique : 5 h 33 à 7 h 48 pour knot_lean).

Aucun geste de la lane, et c'est délibéré :

• ne pas relancer la porte — elle ressortirait STARVED à l'identique tant que le constituent court ;
• ne pas relancer le child tant qu'il progresse ;
• pas de update-branch — il ré-armerait le plancher DWELL pour un rouge qui n'est pas un défaut de la branche, et périmerait les dossiers de prévalidation éventuels.

pr-gate-stale-sweep.yml ré-agrégera à la conclusion du job.

See #16341

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-ai-01:CoursIA
pr: 17637
head: 838e590
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 11e941b088d4263863e38df159ad9ae84a583e1e214628b753972ee034139324
diff-files: 6
diff-additions: 51
diff-deletions: 20
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Dossier ai-01 : Hermes LGTM (substance) a 897f938, tete 838e590 = fusion de main seule (diff nul sur les 6 fichiers). B.1 sorry 1->1, B.2 lake build 8784 jobs, B.3 proof-integrity conway_lean vert a la tete (perimetre Foundation hors target-modules ecrit dans le body). PR gate vert 12:47Z. Seul rouge : l'advisory de visibilite, qui sort toujours 0 par construction : son echec est celui du job, pas un verdict.

[myia-ai-01]

Mergée par ai-01 à la tête 838e5903, après un lake build local, comme lean-merge-discipline §1 l'exige pour toute PR Lean.

• Worktree isolé à la tête, lake exe cache get (Mathlib db584cd6d4, toolchain v4.33.0), puis lake build : Build completed successfully (8784 jobs), rc=0. Le cache partagé de conway_lean sur ai-01 est resté intact.
• count_code_sorry.py --json sur conway_lean : distinct_code_sorry 1 → 1 (base contre tête). Aucune régression de preuve.
• Gate rc=0 (dossier ai-01 c.5815327366, après rerun de l'advisory Lean visibility drift), B.0 rc=0, 26/26 jambes vertes à la source.

Suite : #17673 (sondes #print axioms + parité i18n à rejouer sur main) est désormais prenable par po-2027.