[EPIC][ICT] Chantier 1 — La table des opérations : algèbre des transformations attestée, ses trois lois, ses témoins et ses dettes

[myia-ai-01]

Origine

Consigne de clôture du deuxième voyage de digestion ICT (2026-08-21), verbatim :

« ne pas inventer une huitième strate, ne pas remplir les sixième et septième trop vite ; extraire d'abord la table des opérations déjà présentes, leurs lois, leurs témoins et leurs dettes. »

Cette Epic est ce livrable. Elle ne construit rien de neuf : elle inventorie ce que le dépôt fait déjà, opération par opération, et exige pour chacune une attestation fichier:ligne.

Digestion complète (hors dépôt, GDrive) : MyIA/IA/ICT-transcripts/ict-digest-plan-2026-08-21.md §7.2.

---

1. Pourquoi cette Epic passe avant les quatre autres

Le garde-fou est explicite : « une simple bibliothèque de transformations, même très riche, reste encore un CATALOGUE ». Le risque n'est donc pas de manquer d'opérations — c'est d'en produire une liste de vœux. Critère d'admission retenu, qui est la substance de cette Epic :

Une opération entre dans la table si elle est attestée au moins deux fois dans des endroits indépendants du dépôt ET si l'on sait dire quelle forme prend son témoin.

Une seule attestation ⇒ file d'attente, pas la table. C'est le seul mécanisme qui empêche l'inventaire de devenir de l'auto-certification.

---

2. Le premier jet — dix opérations, à confronter au dépôt fichier par fichier

Ce tableau est un premier jet issu de la digestion, pas une mesure. Le travail de cette Epic est de le vérifier ligne à ligne. La dernière colonne est ce qu'il faut prouver ou réfuter.

#	Opération	Loi (ce qui doit tenir)	Témoin (ce qui atteste, ou réfute)	Dette	Prétendument attesté par
1	Recoordonner — changer la représentation sous laquelle le problème est soumis	La forme d'émission décide du destin : même contrainte, deux formes, deux destins	L'objet qui atterrit (le 9x9 complet ; la preuve devenue presque triviale après canonisation)	Non-canonicité : aucune théorie du « bon » changement	Sudoku-13 + companion Z3 ; conway_lean ; MetaGeneticSharp
2	Abstraire à dette bornée — compresser, résoudre, relever	Le relèvement transporte une garantie : Exploitability(sigma_G) <= eps(alpha, rho, ...)	La borne elle-même ; un contre-exemple d'exploitabilité si elle casse	Chiffrée — c'est sa vertu. Question inversée : « qu'ai-je le droit d'oublier ? »	Kroer-Sandholm (à distiller) ; MechanismDesign.lean
3	Quotienter / fibrer	Règle de chaîne : H(X) = H(pi(X)) + H(X sachant pi(X))	I(X_i ; X_j sachant Q) sur un quotient commun Q	Ruzsa exige une structure de groupe — sans elle, ce serait « le nouveau mapping affine »	Lean-21 / teorth/pfr
4	Décomposer localement — poser un recouvrement	Les bords doivent être définis avant les sections	Le recouvrement lui-même, non-jouet	DETTE OUVERTE : qui décide où sont les bords ?	ICT-15d (jouet) ; Hashlife ; orchestration EPITA
5	Recoller — compatibilité puis composition	Compatibilité sur les chevauchements, composition sur les triples	Le témoin exploitable, pas le résidu	Notre Cech rend TRIVIAL faute de catégorie de transports, pas faute de non-linéarité	decision_theory_lean (de Finetti) ; safe subgame solving
6	Réparer localement sous garantie	Conditions de bord préservant la non-exploitabilité ; imbricable	La déviation adversariale si la loi est violée	Dépend d'un blueprint global déjà bon ; compatibilité causale	Brown-Sandholm (Libratus)
7	Engendrer un témoin — vérificateur vers constructeur	spécification -> générateur -> témoin -> certificat ; le générateur n'est pas le vérificateur	L'objet produit : grille, motif RLE, mécanisme, contre-exemple	Le moteur de synthèse reste hors Lean	Sudoku-13 ; conway_lean (côté certification seulement)
8	Certifier — clore par une preuve	fail_on_sorry ; axiomes interdits ; emprunté vs prouvé explicite	Le certificat + l'inventaire d'axiomes	Un native_decide vide le théorème	21 lakes ; Lean-22b
9	Élargir l'espace — ajouter une primitive	Monotonie de l'atteignabilité : P_reel inclus dans P_relache	Le différentiel d'atteignabilité	Non-canonicité du choix d'extension	planning_lean ; OWL/SHACL
10	Concevoir la règle — le mécanisme devient la variable	M* = argmax J(M) sous DSIC, IR, budget ; commitment crédible	Le mécanisme certifié, ou le témoin d'impossibilité	Optimiser dans M n'est pas faire apparaître une coordonnée hors de M	AMD ; Stackelberg ; smart contracts ; échange de reins

Les quatre en cours de constitution

#	Opération	Loi	Témoin	Dette
11	Descendre sous budget	décroissance stricte + barrière + pas de blocage hors cible ⇒ terminaison bornée	le budget atteint, ou le blocage	un échec de décroissance est une dissociation, pas un échec d'expérience
12	Composer des regards	play forward / coplay backward ; composition associative	la paire de lectures incompatibles exhibée	catégories téléologiques sans unité — fait algébrique, pas irréversibilité physique
13	Traverser un mur	chambre -> mur -> chambre voisine ; six swaps générateurs	le chemin minimal certifié	un swap change les préférences : ce n'est pas un morphisme
14	Agréger un collectif	Möbius sur le treillis des coalitions : v(S) = somme des m(T) pour T inclus dans S	la stratégie de manipulation (Gibbard-Satterthwaite)	les théorèmes d'impossibilité mordent

File d'attente — une seule attestation, à ne PAS inscrire

institutionnaliser (DAO seulement) · inhiber (pas de banc) · réviser une croyance (Tweety, non branché) · point fixe (Knaster-Tarski dans argumentation_lean — très solide, à promouvoir dès le second usage).

---

3. Les trois lois de composition — ce qui fait la valeur, et non la liste

LOI I — obstruction abstraite vers témoin exploitable (relie 5 à 7). Attestée deux fois indépendamment : de Finetti construit un Dutch Book à partir d'un système de prix incohérent ; Brown-Sandholm produit une déviation adversariale à partir d'un recollement local incorrect. Deux lakes, deux domaines, même patron. Conséquence normative :

« Si nous prétendons détecter un défaut de recollement, pouvons-nous produire un cycle concret qui exploite ce défaut ? » — tant que la réponse est non, le mot « obstruction » n'a pas gagné ses galons.

C'est le critère d'acceptation de tout futur Cech (voir chantier 3).

LOI II — recoordonner + passer du vérificateur au constructeur (relie 1 à 7). Attestée sur Sudoku (le solveur reconnaît / Z3 produit) et sur Hashlife (certification de motifs importés, mais synthèse non encore franchie). Loi connue et à moitié appliquée : la dette la plus actionnable du dépôt (voir chantier 2).

LOI III — les deux espèces de flèches (relie 13 à 12). Toutes les transformations ne sont pas des morphismes : un swap ordinal change les préférences, donc transforme la structure au lieu de la préserver. La question « quand une transformation est-elle aussi un morphisme ? » devient précise et vérifiable.

Verdict de grade, honnête. Trois lois, deux attestées deux fois, une attestée une fois. Ce n'est pas un grade A (une algèbre munie de sa propre géométrie : adjonctions, unités, identités triangulaires, invariants sous changement de cadre). C'est un catalogue muni de trois lois — exactement ce que la consigne demandait de produire avant de prétendre remplir les strates 6 et 7.

---

4. Grains — conçus pour les allers-retours

Chaque grain est une tranche indépendante, relisable seule, et révisable : le tableau est un objet vivant, une opération peut être rétrogradée en file d'attente si la seconde attestation ne tient pas.

• A1 — (livre en substance, sous un AUTRE nom de fichier — lire l'etat reel ci-dessous avant d'en creer un second) Support : docs/ledgers/<N>-table-operations.md, une ligne par opération, colonnes opération / loi / témoin / dette / attestation 1 (fichier:ligne) / attestation 2 / verdict.
• A2 — (livre : docs/ledgers/12204-ict-chantier-1-a2.md, PR ledger(ict,#12204): tranche A2 -- l'operation 1 (Recoordonner) passe de RAPPORTE a FIRSTHAND #13956/docs(ict,#12204): table op 1 RAPPORTE -> FIRSTHAND (A2 livree #13956) #14563 — op 1 passe RAPPORTE → FIRSTHAND ; ops 7/8 déjà FIRSTHAND à l'audit froid) Vérifier les opérations 1, 7, 8 (attestations les plus proches : Sudoku-13, conway_lean, les 21 lakes). Rendre fichier:ligne, ou rétrograder.
• A3 — (livre : docs/ledgers/12204-ict-chantier-1-a3.md, PR ledger(ict,#12204): Chantier 1 tranche A3 — verif operations 3, 9 (planning_lean attested 0 sorry, teorth/pfr externe non-local) #12293) Vérifier 3, 9 (teorth/pfr, planning_lean) — les deux que le voyage dit sans sorry, à confirmer par scripts/lean/count_code_sorry.py --json.
• A4 — (livre : docs/ledgers/12204-ict-chantier-1-a4.md, PR ledger(ict,#12204): tranche A4 -- operation 4 (recouvrement) passe de RAPPORTE a FIRSTHAND #14453 — op 4 RAPPORTE → FIRSTHAND ; op 5 reste en file d'attente) Vérifier 4, 5 et écrire noir sur blanc la dette ouverte du recouvrement (qui décide des bords).
• A5 — (livre : docs/ledgers/12204-ict-chantier-1-a5.md, PR docs(ledger,#12204): tranche A5 -- ops 2/6 gagnent leur premiere attestation in-repo (distillation atterrie) #18118 — ops 2/6 gagnent leur première attestation in-repo (GT-19 courbe de dette mesurée ; paire GT-13b/13c garantie contrôlée), restent en file d'attente au critère mécanique ; op 10 reconfirmée firsthand) Vérifier 2, 6, 10 — dépendent de la distillation Sandholm (chantier 5) : à faire après elle, pas avant.
• A6 — (livre : docs/ledgers/12204-ict-chantier-1-a6.md, PR docs(ledger,#12204): statuation A6 -- ops 11-13 promues TABLE, point fixe ecarte (homonyme Tarski) #18105 — ops 11/12/13 promues TABLE, point fixe promue TABLE sur second usage mesuré) Statuer sur les quatre en constitution (11-14) et sur la file d'attente.
• A7 — Relecture froide : la table est-elle un catalogue ? La vérification a-t-elle fait apparaître une quatrième loi ?

4bis. État réel mesuré au 2026-09-01 (relecture ai-01)

Les cases de §4 étaient toutes vides alors que deux tranches ont atterri, dont une qui a fait davantage que ce que A1 demandait. Section écrite en confrontant le corps au dépôt, pas en le recopiant.

Ce qui existe sur main

Fichier	PR	Ce qu'il établit
docs/ledgers/12204-ict-chantier-1-a3.md (156 l.)	#12293	A3 : opérations 3 et 9 vérifiées firsthand à l'instrument canonique count_code_sorry.py --json (distinct_code_sorry, jamais grep -c)
docs/ledgers/12204-ict-chantier-1-audit-froid.md (103 l.)	#12401	La table complète des 14 opérations, labellisée sur trois axes orthogonaux (provenance RAPPORTE/FIRSTHAND · attestation 1/2+ · force empirique/exhaustif/Lean-formel), avec un verdict par ligne

Le piège de nommage — à lire avant de prendre un grain ici

A1 demandait docs/ledgers/<N>-table-operations.md. Ce fichier n'existe pas ; la table qu'il décrit existe, dans 12204-ict-chantier-1-audit-froid.md. Une lane qui lirait la case vide de A1 et créerait <N>-table-operations.md produirait un doublon divergent de la table déjà attestée. A1 est donc coché en substance : ce qui reste n'est pas de créer un support, c'est au plus de renommer celui qui existe si le nom compte — et il ne compte probablement pas.

Ce que l'audit froid a réellement tranché (au-delà de son mandat)

Quatre descentes en file d'attente, chacune motivée : op 2 (Kroer-Sandholm reste externe, #12208 non mergée) · op 6 (une seule famille, Sandholm) · op 5 (« mauvais recollement → déviation adversariale » est notre lecture du safe subgame solving, pas une attestation — le défaut exact qui avait coulé ICT-15d : nommer le cadre mathématique avant de posséder les transports) · op 3 (teorth/pfr est externe au dépôt, mesuré ; Lean-21b #12252 est une vraie attestation locale, mais une seule).

Deux promotions par la mesure : op 9 passe à 2 attestations sur deux substrats indépendants (planning_lean/Planning/Admissibility.lean:50 où relaxed_plan_admissible est P_reel ⊆ P_relache, et SW-14 #12263 côté OWL/SHACL) — première opération promue par cette Epic ; et la Loi III gagne sa seconde attestation.

C'est le mécanisme du §1 qui fonctionne comme prévu : le seuil des deux attestations fait tomber autant qu'il fait monter. Un inventaire qui ne dégrade jamais rien s'auto-certifie.

Ce qui reste, et dans quel ordre

• A2 — les opérations 1, 7, 8 sont en TABLE mais 1 est encore RAPPORTE : le grain est l'élévation à FIRSTHAND, pas une re-décision. Grain le plus immédiatement prenable.
• A4 — opérations 4, 5 + écrire la dette ouverte du recouvrement (qui décide des bords). Op 5 est déjà descendue ; A4 doit dire si elle remonte.
• A5 — bloqué en amont : dépend de la distillation Sandholm ([EPIC] Chantier 5 — Distillation par les séries pédagogiques : mûrir les concepts externes en notebooks ad-hoc (GameTheory, Lean, IIT), puis infuser ICT #12208, toujours OPEN). Ne pas le prendre avant.
• A6 — l'audit froid a déjà pré-instruit 11, 13, 14 (« statuer en A6 ») et signale 12 comme candidate forte. A6 est donc une décision, plus une enquête.
• A7 — relecture froide, à faire en dernier.

Ce que les 21 PR citant cette Epic ne prouvent PAS

Un tirage remonte cette Epic avec « livraison récente : #13628 mergée + 17 autres ». Deux de ces PRs sont des tranches de l'Epic (#12293, #12401) ; les autres la citent comme parent (See #12204) et livrent dans les domaines des opérations, sans toucher la table. Le compte de PRs citantes n'est pas une mesure d'avancement de l'inventaire — c'est le genre de raccourci que le §1 interdit précisément.

---

4ter. État mesuré au 2026-09-27 (tranche A6, lane po-2024)

Confrontation du corps au dépôt à la livraison de la tranche A6 (PR #18105). Historique ci-dessus conservé intact.

Ce qui a changé depuis 4bis — trois tranches atterries, une promotion de masse :

Tranche	PR	Ce qu'elle établit
A2 — op 1 FIRSTHAND	#13956 (via #14563)	Recoordonner passe de RAPPORTE à FIRSTHAND (ledger dédié)
A4 — op 4 FIRSTHAND	#14453	le recouvrement de Décomposer localement attesté firsthand, dette des bords écrite
A6 — statuation	#18105	ops 11, 12, 13 promues TABLE (secondes attestations comptées : Search-11d #16392, Search-12a #16426, Search-13a #16438, artefacts mesurés sur main — exécutés, 0 erreur) ; point fixe promue TABLE sur second usage mesuré : Tweety-07a C# cellule 5 exécutée (ADF.Grounded() from-scratch, témoin imprimé {a,c} + re-dérivation, ligne 647 : lfp de la fonction caractéristique) — substrat .NET indépendant du lake Lean, opérateur ADF distinct (généralisation). Homonymes écartés avec preuve : FolBridge.lean:124 (sémantique de Tarski) et GT-22 (équilibre dynamique). *(correctif même cycle, commit 776919a — le verdict initial « écartée » reposait sur le grep `knaster

Table après A6 : TABLE = 1, 4, 7, 8, 9, 10, 11, 12, 13, 14 (les numérotées) + point fixe · FILE D'ATTENTE = 2, 5, 6 + institutionnaliser, inhiber, réviser une croyance.

A5 débloquée en apparence — l'issue de gate #12208 (Chantier 5, distillation Sandholm) est CLOSED (mesuré ce cycle) : le « bloqué en amont » de 4bis ne tient plus en l'état. Une lane qui prend A5 doit d'abord groundeer ce que le chantier 5 a réellement laissé sur main (body daté de sa rédaction, protocole habituel).

Restent : A7 (relecture froide — la quatrième loi ?). A5 livrée en #18118 (bloc 4quater ci-dessous).

---

4quater. État mesuré au 2026-09-27, second pointage (tranche A5, lane po-2024)

A5 livrée en PR #18118 — la gate #12208 étant CLOSE (chantier 5 terminé et vérifié), la confrontation aux artefacts donne :

• Op 2 « Abstraire à dette bornée » : première attestation in-repo — GT-19-Abstraction-a-Dette (exécuté, 0 erreur ; courbe de dette mesurée sur chaîne de raffinement vérifiée). File d'attente maintenue (une seule).
• Op 6 « Réparer localement sous garantie » : première attestation in-repo — paire GT-13b/13c Safe-Subgame-Solving (exécutées ; contre-témoin du raffinement naïf, garantie contrôlée, 13c calcule la vraie best-response). File d'attente maintenue.
• Op 10 : déjà TABLE, reconfirmée firsthand (GT-16b : M* = argmax J(M), témoin d'impossibilité).

Les secondes attestations des ops 2 et 6 ne dépendent plus d'aucun externe : grains de contenu créables dans d'autres séries (patron op 12 : GT-21 + Search-12a).

---

5. Ce que cette Epic ne fait pas

Elle n'ouvre pas de huitième strate, ne déclare pas la strate 6 commencée, et ne prétend pas au grade A. Elle produit un inventaire attesté. Les strates 6/7 restent au statut scaffold landed, pas strand constituted.

6. Dettes de vérification héritées (statut RAPPORTÉ, pas VÉRIFIÉ)

Les affirmations sur le contenu des lakes (Descent.lean, Bridge.lean, NormTails.lean, learning_theory_lean, planning_lean, decision_theory_lean, argumentation_lean) viennent du transcript de digestion et n'ont pas été vérifiées firsthand. Les vérifier est la fonction première de cette Epic.

See #4588 · See #11690

[myia-ai-01]

Réservoir de grains — chantier 1

Le réservoir a été extrait du digest le 2026-08-22. Chaque grain est un concept, un notebook, éventuellement des scripts / preuves / tests compagnons, une PR. Aucun n'est réservé à une lane : tout est piochable.

Issue	Concept	Notebook hôte
#12219	Le budget de descente — une ressource initiale borne le nombre de transformations ; l'échec de décroissance est une dissociation	Lean-25
#12220	Borne + témoin extrémal + concentration — le triptyque déjà formalisé dans learning_theory_lean	série ML ou compagnon Lean
#12221	de Finetti — l'incohérence qui construit son Dutch Book ; et vNM, où l'affine est enfin canonique	Lean-27
#12224	Langage de primitives et de combinateurs — exprimer une intention, pas assembler à la main	MGS-20
#12229	L'abstraction à dette mesurable — « qu'ai-je le droit d'oublier ? » remplace « est-ce que ça compresse ? »	GameTheory-19
#12230	La représentation domine l'algorithme — l'expérience MGS déjà faite, jamais écrite	MGS-21
#12231	Pearl / DoWhy — exiger un estimand plutôt que coller do() devant une distribution	Infer-21
#12232	Sortir du petit Dung Python — consommer un noyau argumentatif certifié	série Tweety
#12238	Möbius sur le treillis des coalitions — ce qui n'existe qu'au niveau collectif	GameTheory-15d
#12239	Gibbard-Satterthwaite — la manipulation exhibée comme témoin d'exploitation	GameTheory-22

#12221 et #12225 attestent la Loi I (obstruction abstraite ⟶ témoin exploitable) sur deux lakes indépendants — c'est ce qui autorise la loi plutôt que l'intuition.

Rappel du garde-fou de ce chantier : « une bibliothèque de transformations, même très riche, reste un catalogue ». Produire la liste ne suffit pas ; ce sont les lois de composition qui font la différence.

[jsboige]

[CLAIMED] lane myia-po-2026:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Planners/planning_lean/**, docs/ledgers/12204-ict-chantier-1-a3.md

Grain A3 EPIC #12204 (Chantier 1 ICT — vérifier 3, 9 : teorth/pfr + planning_lean no sorry).

Strategie : run scripts/lean/count_code_sorry.py --lake planning_lean --json + ledger entry file:line + PR. teorth/pfr = reference externe Tao, non-local, sera consigne en consequence.

[jsboige]

Audit froid : trois labels orthogonaux par operation, et quatre entrees a faire tomber

Revue exterieure du 2026-08-22 sur les 24 h. Elle valide la forme de cette Epic
— « trois lois ne font pas encore un grade A », strates 6-7 maintenues a
scaffold landed — et pointe que le prochain travail n'est pas d'ajouter des
entrees mais de faire tomber celles qui ne survivent pas. D'accord.

Le protocole d'audit

Chaque operation de la table porte desormais trois labels independants —
independants, parce que les confondre est ce qui fabrique les faux grades :

axe	valeurs	ce qu'il mesure
provenance	RAPPORTE / FIRSTHAND	ai-je lu la source, ou une lecture de la source ?
attestation	1 attestation / 2+ attestations	le seuil deja pose par cette Epic
force	empirique / exhaustif / Lean-formel	ce que vaut la preuve, pas ce qu'elle couvre

Une operation FIRSTHAND / 1 attestation / exhaustif et une operation
RAPPORTE / 2+ attestations / empirique ne sont pas comparables sur un axe
unique : c'est precisement l'ambiguite que trois labels retirent.

Les quatre entrees que je conteste, nominativement

• Abstraire a dette bornee — soutenue surtout par Kroer-Sandholm, qui
  reste externe tant que sa distillation ([EPIC] Chantier 5 — Distillation par les séries pédagogiques : mûrir les concepts externes en notebooks ad-hoc (GameTheory, Lean, IIT), puis infuser ICT #12208) n'a pas atterri.
  MechanismDesign.lean ne constitue pas a lui seul une seconde attestation de
  bounded abstraction : il atteste un mecanisme, pas une borne d'abstraction.
  -> RAPPORTE / 1 attestation.
• Reparer localement sous garantie — une seule famille (Sandholm).
  -> 1 attestation, donc hors table tant qu'une seconde ne tombe pas.
• mauvais recollement -> deviation adversariale (Brown-Sandholm) — c'est
  notre lecture structurelle du safe subgame solving, pas un theoreme Cech.
  Le noter comme lecture, pas comme attestation. C'est le defaut exact qui a
  coule notre premiere tentative ICT-15d : nommer le cadre mathematique avant
  de posseder les transports.
• Quotienter/fibrer — tres fort chez PFR, mais il faut un second
  substrat avant de parler de primitive transversale.

Une dissociation candidate, issue de la mesure — PAS une quatrieme loi

GT-24 (PR #12364, verifiee firsthand) a teste l'intuition que les murs
pourraient raccourcir les chemins entre chambres. Resultat exhaustif :

univers complet 5625 avec murs : connexe, diametre 12
576/576 paires strict-strict : 0 ecart d_full < d_perm
(structure produit -> couvre les 330 776 paires de jeux)
chemin Dilemme->Renversement : 5 pas, dont 0 sur un mur, certifie minimal

D'ou, a inscrire comme dissociation candidate du deuxieme voyage, avec ses
deux qualificatifs :

stratification != compression metrique
— FIRSTHAND / 1 attestation / exhaustif, et borne au systeme de mouvements
actuel (generateurs de swaps, ordinal 2x2).

Elle n'entre pas comme loi : une dissociation mesuree sur un substrat est
une dissociation sur un substrat. Elle vaut mieux qu'une confirmation docile —
la prose du notebook a du etre reecrite APRES mesure (le draft annoncait
4/256 geodesiques et diametre 6, tous deux faux) — mais le cran de generalite
n'est pas atteint.

Deux precisions de vocabulaire, pour ne pas solidifier trop tot

1. GT-24 : « chemin certifie » sur-promet dans le titre. Le corps de la PR
   est deja honnete (§6 : « pas de jambe Lean (c'est le variant -b) ») ; c'est
   le titre qui porte le mot. Formulation juste : temoin construit et verifie
   independamment — la verification est une re-derivation exhaustive en
   Python par un verificateur separe, ce qui est exactement la Loi II, et ce
   n'est pas une certification Lean.
2. Meta-actions tarifees : « changer les regles » sur-promet. L'agent
   modifie son classement ordinal de resultats par swaps tarifes. Il ne cree
   ni action, ni joueur, ni regle de transition, ni mecanisme.
   -> meta-action sur le jeu : OUI. Ontological move complet de strate 7 :
   NON. Cette distinction doit rester dans le texte pedagogique, pas
   seulement ici.

[jsboige]

[CLAIMED] lane myia-po-2025:CoursIA -- paths: docs/ledgers/12204-ict-chantier-1-audit-froid.md -- tranche audit-froid : protocole 3 labels applique aux 14 operations, 4 entrees contestees faites tomber (steering ai-01 2026-08-22T20:54Z). Disjoint du claim po-2026 (planning_lean/** + a3.md) ; fichier a creer (d'ou le DEAD_GLOB hint, exit 2 non-conflit).

[jsboige]

[RELEASED] lane myia-po-2025:CoursIA — tranche audit-froid : PR #12401 (3 labels sur 14 operations, 4 tombées op 2/3/5/6, gains op 9 + Loi III, contrepartie Loi I).

[jsboige]

[CLAIMED] lane myia-po-2025:CoursIA -- paths: MyIA.AI.Notebooks/GameTheory/game_theory_lean/Abstraction/**, MyIA.AI.Notebooks/GameTheory/game_theory_lean/Abstraction.lean, MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean
Grain: MED/lean — lane myia-po-2025:CoursIA — prev: DEEP/research-code #13459

Sous-grain A5 / opération 2 : donner un statut formel à la non-décroissance de la dette sur une chaîne de raffinement, sur un domaine jouable borné (preuve ou contre-exemple), question explicitement laissée ouverte par GT-19. Les deux futurs chemins Abstraction* n’existent pas encore ; le lakefile.lean existant garde le verrou mécanique, et la collision a été vérifiée séparément sur les PR ouvertes et origin/main.