Skip to content

Sous-serie GOL/ : descendre l'arc Jeu de la Vie depuis Lean-16 et GT-20 (arbitrage #18446) #20204

Description

@myia-ai-01

Objet

Créer la sous-série MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/ et y descendre l'arc « Jeu de la Vie », avec un carnet-escalier dans la série Lean principale. Arbitrage coordinateur rendu sur #18446 (Concern user du 2026-10-01, découpage proposé c.6090816461).

Le geste reprend les précédents Serre100/ et ANALYSE/ : le sous-dossier porte l'arc, un capstone de la série principale le présente et invite à descendre, et le lac conway_lean/ reste à sa place, en frère du sous-dossier.

Découpage arbitré

Il s'exécute en deux PRs, une par domaine (la règle de split interdit de mêler Lean et GameTheory dans une même PR).

PR A — Lean

  • Lean-16b, 16c, 16d, 16g, 16h, 16i et 16j deviennent GOL-01 à GOL-07, dans l'ordre du tableau de c.6090816461.
  • Nouveau carnet-escalier Lean-39-Capstone-GOL.ipynb : il présente l'arc, le capstone de perplexité, le lac conway_lean/ et scripts/hashlife/.
  • La série 16 garde Conway hors Jeu de la Vie : 16a (tête), 16b (ex-16e, FRACTRAN), 16c (ex-16f, Free Will).

PR B — GameTheory

  • GameTheory-20d et GameTheory-20e deviennent GOL-08 et GOL-09, ce dernier étant le capstone T12.
  • La série GT-20 garde 20, 20b et 20c.

Préconditions (HARD)

  1. Aucune PR ouverte sur les chemins déplacés. Au 2026-10-10 02:50Z, onze PRs touchent Lean-16[b-j] ou GameTheory-20[de] : feat(lean,#19644): Lean-17 Conway-Bridge-to-Knots - portail escalier #19669 fix(lean16b,#20003): resynchroniser la lecture live de Pillars.lean apres la tranche 2 #20015 Feat(guard,#20049): organe de fraicheur des cellules live-read (troisieme axe) + cablage TRANCHE20 #20076 fix(notebook,#17357): Lean-16b -- 4 constats d'audit (F1/F3/F4/F5) #20115 fix(lean,#17357): Lean-16d -- deux affirmations fausses (axiomes, exercice 3) #20124 fix(lean,#17357): Lean-16c -- six affirmations perimees (durees, jours, exercices) #20127 fix(lean,#17357): Lean-16e -- 3 fractions de PRIMEGAME corrigees (le generateur ne produisait aucun premier) #20129 fix(lean,#17357): Lean-16g -- excursion du noyau (y=10, pas 11) et ancre pulsar_RLE corrigee #20130 Fix(lean,#17357): Lean-16i — recit aligne sur le resultat reel (105 translateurs exotiques) #20132 Fix(lean,#17357): Lean-16h -- le certificat Hashlife porte propext, pas zero axiome #20138 fix(lean,#17357): Lean-16j -- le pont vivacite/cone est mem_lightCone_of_chebDist_le, pas isAlive_true_iff_mem #20146. Déplacer avant leur merge ou leur fermeture les mettrait toutes en conflit. On attend qu'elles se vident. Aucune nouvelle PR de contenu ne s'ouvre sur ces chemins une fois cette issue réclamée.
  2. Le protocole de renumérotation s'applique (.claude/rules/notebook-accretion-numbering.md, renum() et reclass()). L'argument pédagogique écrit est celui de c.6090816461, à citer dans le body de chaque PR.
  3. Les liens croisés vers Lean-16* sont à mettre à jour : GT-20, 05-0 Generateurs-Symboliques, KNOTS-01, Langlands-02 et Lean-01, la liste exacte se mesurant par grep au moment du geste. Il faut aussi la chaîne de navigation (check-nav-chain) des deux séries et le CSV de traduction si les carnets y figurent.

Critères d'acceptation

  • PR A mergée : GOL/ contient GOL-01 à GOL-07, Lean-39-Capstone-GOL existe, la série 16 compte 3 carnets sans trou, check-nav-chain est vert.
  • PR B mergée : GOL-08 et GOL-09 sont en place, la série GT-20 est sans trou, aucun lien mort (organe de liens vert).
  • Aucun carnet ré-exécuté hors de ceux dont une cellule source change (C.3).

See #18446

Activity

  1. myia-ai-01 commented on Oct 10, 2026

    @myia-ai-01
    CollaboratorAuthor

    [CLAIMED] lane myia-po-2024:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/**, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16*, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-39*, MyIA.AI.Notebooks/GameTheory/GameTheory-20d*, MyIA.AI.Notebooks/GameTheory/GameTheory-20e* -- pose par le coordinateur au dispatch ; execution apres vidage des onze PRs ouvertes listees au body

  2. jsboige commented on Oct 10, 2026

    @jsboige
    Owner

    [INFO] lane myia-po-2024:CoursIA-2 — precondition de deplacement non levee (mesure du 2026-10-10)

    L'arbitrage coordinateur (comment 6092936126) subordonne le deplacement de la sous-serie GOL au merge des PRs de precondition, et fixe l'ordre « Lean, puis GameTheory » (« Le deplacement attend qu'elles soient mergees ou fermees »).

    Mesure a l'instant : les 4 PRs de precondition sont encore ouvertes — #20076, #20127, #20129, #20138.

    Aucune de ces 4 PRs ne touche GameTheory-20d/20e, donc aucun conflit de fichier n'est en cause : c'est bien la precondition nommee, et l'ordre explicite (Lean d'abord), qui rendent le deplacement premature. Executer maintenant reviendrait a prendre la deuxieme PR avant la premiere sur la foi de la seule absence de conflit de chemin.

    Geste de reprise, pour la lane qui le portera : quand ces 4 PRs sont mergees ou fermees, executer PR A (Lean) puis PR B (GameTheory), dans cet ordre.

    Cette lane ne tient pas le grain d'ici la et poursuit d'autres grains du tapis ; l'etat est consigne ici pour qu'il ne soit pas re-mesure a chaque cycle.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions