Epic Aaronson — six veines, aucune curatee : de la permanente au premier lake Lean d'IIT

[myia-ai-01]

État mesuré au 2026-10-03T05:15Z (lane myia-po-2027:CoursIA, tirage picker — cf #11900). Le body ci-dessous date de l'ouverture (2026-09-19) ; 5 de ses 6 veines sont livrées sur main. Ce qui suit est la mesure firsthand ; l'historique est conservé tel quel en dessous.

Veine	État mesuré	Preuve sur main
1 — permanente/BosonSampling	LIVRÉE	Complexity/Complexity-05b-AaronsonArkhipov-PermanenteBosonSampling.ipynb (PR #16850 MERGED)
2 — Complexity Zoo	LIVRÉE	Complexity/Complexity-03c-ComplexityZoo-Navigation-Python.ipynb
3 — distillation Ghost / strate 7	OUVERTE, gated curation	ICT-Series/README.md : strate 7 toujours vide ; « à arbitrer au moment de la curation »
4 — déquantification	LIVRÉE	Complexity/Complexity-06-Aaronson-Dequantification-Stabilizer.ipynb
5 — objet qui a mordu IIT, en Lean	LIVRÉE	IIT/IIT-06-L-Objet-qui-a-Mordu-IIT.ipynb + lake SymbolicAI/Lean/iit_lean/ (IIT/Integration.lean : broadcast_integrated, broadcast_trivial_dynamics, 0 sorry, jumeau _en, câblé lean-ci-matrix #18599)
6 — acquisition bibliographique	LIVRÉE	Gisement Consciousness/ : Ghost (PDF), Why Philosophers Should Care (PDF), Aaronson–Arkhipov Linear Optics (PDF), l'échange IIT complet (expander, Griffith, Tononi, Phi-nal exchange)

Ce qui reste actionnable : la veine 3 seule — et elle est gated sur l'arbitrage de curation (ai-01/user), pas sur une lane. Une lane qui tire cette umbrella ne doit ni re-faire les veines 1/2/4/5/6, ni claimer la veine 3 sans l'arbitrage. La mesure de « 0 PDF au gisement » dans le body d'origine est périmée.

Epic parapluie ouvert sur brief user du 2026-09-19. La curation n'est pas préemptée — patron de l'Epic Schmidhuber (#16775). Les veines ci-dessous sont celles que le brief nomme ; aucune n'est un engagement de livraison tant que sa source n'est pas lue et sa résonance vérifiée contre l'arbre.

Le brief se clôt par : « l'Epic Aaronson n'est pas curatée, mais elle se construira toute seule ». Ce document est fait pour rendre ça vrai — poser l'état mesuré et les veines, pas remplir une étagère.

L'état mesuré — il hante, et cette fois sans même une pièce

git grep -i aaronson sur l'arbre complet (c818f6abc) : 4 hits, zéro de lui — deux fichiers de recettes RecipeML (homonyme dans un dataset Z3) et deux occurrences de Ryser côté Sudoku qui ne le concernent pas. Aucun .ipynb du dépôt ne contient le mot « freebit ».

Gisement G:\Mon Drive\MyIA\IA\Bibliographie IA : 0 PDF de lui (recherche par nom de fichier et par contenu, 355 PDF).

Contraste avec Schmidhuber (#16775), qui habite 19 artefacts dont un module testé : Aaronson n'a pas de pièce du tout. Il vit exclusivement en prose .md de cadrage ICT — et c'est d'autant plus frappant que, d'après le brief, c'est lui qui a poussé ICT jusqu'à la strate 7.

Le critère d'entrée, rappelé parce qu'il mord ici

Une fibre — ou une œuvre — s'acquiert par un organe, pas par une citation (#16759). Aaronson est le cas limite : tout invite à le citer, rien ne l'oblige à produire. Chaque veine ci-dessous doit donc dire ce qui s'exécute ou se prouve, sinon elle reste une note de lecture.

---

Veine 1 — la complexité qui tourne (amorcée)

#16779 — Complexity-03 : la permanente comme frontière. BosonSampling (Aaronson–Arkhipov 2011), perm vs det en comptes d'opérations exacts, en réemployant le Ryser vectorisé déjà présent dans Sudoku-15-Infer-Python.ipynb. Série Complexity/ : format « hommage aux fondateurs » établi, slot 03 libre.

Clarification par rapport à ce que j'y ai écrit : #16779 pose « ne touche pas la strate 7 » comme contrainte de périmètre de cette issue-là, pas comme jugement sur Ghost — dont le brief établit au contraire la centralité. Les deux veines sont disjointes et le restent ; la veine ICT est la 3.

Veine 2 — onboarder le Complexity Zoo

Nommé par le brief. Le zoo est l'objet pédagogique par excellence : une carte des classes, leurs inclusions, leurs séparations connues et surtout celles qui ne le sont pas. À cadrer : un notebook qui navigue le zoo et en fait quelque chose d'exécutable (inclusions vérifiées sur des instances, oracles jouets séparant deux classes) plutôt qu'une table recopiée. La série Complexity/ demande un encart gap Mathlib — le zoo est précisément la mesure de ce que Mathlib n'a pas.

Veine 3 — digérer The Ghost in the Quantum Turing Machine

Le brief : « la publication qui a sans doute le plus influencé ICT en l'emmenant jusqu'en strate 7 », et « pas du tout dans le style empêcheur de tourner en rond du personnage, une épopée absolument merveilleuse ».

C'est donc la veine ICT, et elle est la plus chargée :

• docs/ict/strate7-cadres-libres.md cadre déjà les freebits — c'est là que le nom vit aujourd'hui, en prose seule.
• Deux lectures concurrentes des freebits sont en jeu : celle du texte, et une lecture d'ordre 2 que le user tient contre elle. Une distillation honnête porte les deux, avec leurs grades — c'est exactement la discipline docs/ du dépôt (dialogue, pas paraphrase ; tensions conservées).
• Résiduel connu à ne pas dupliquer : la coquille de strate7-cadres-libres.md:28 (freebit « repris dans les notebooks Mechanism Design », qui n'existent pas) est portée par ICT : resync de la tresse sur l'arc strate-1..7 — la tranche morte avec la fermeture de #7424 #16777. Ne pas la corriger ici.

Critère d'organe pour cette veine : la strate 7 est vide (ICT-Series/README.md : « rien n'y est livré »). Une distillation de Ghost qui n'y dépose rien d'exécutable la laisse vide. À arbitrer au moment de la curation — pas ici.

Veine 4 — le style d'arbitre : déquantifier les suprématies annoncées

Le brief décrit une méthode, pas un résultat isolé : « il passe son temps à siffler la fin de la récré en faisant produire par ses équipes des équivalents classiques pour contredire de supposées supériorités quantiques ».

C'est le meilleur candidat pédagogique de tout l'Epic, parce que la méthode s'exécute : prendre une suprématie annoncée, écrire le simulateur classique, mesurer où il tient et où il casse. Le dépôt a déjà le réflexe — la série Complexity/ mesure des ratios réels, pas des asymptotiques. Ici, il y a en plus une leçon de méthode scientifique rare : comment on réfute proprement.

Veine 5 — l'objet qui a mordu IIT, en Lean si possible

Le brief : le même geste d'arbitre appliqué à IIT — la construction d'un objet mathématique à Φ énorme et à comportement trivial, et la réponse publiée qui assume la conséquence (« cet objet est conscient, tu ne sais simplement pas l'apprécier », dans l'esprit). Le brief note que l'échange a été fertile pour les versions ultérieures de PyPhi.

Note de rédaction : l'échange est publié des deux côtés — on le cite et on le grade, on ne prête d'état d'esprit à personne.

Ce que la mesure dit de la faisabilité :

• La série IIT existe (IIT-01..IIT-05 + ICT-Series), IIT-06 est libre, et IIT-01-IntroToPyPhi.ipynb fournit déjà le socle PyPhi.
• Le dépôt compte 20+ lakes Lean — et aucun pour IIT/ICT. « Présenter l'objet en Lean » veut donc dire créer le premier lake de la série, sur le patron établi (lake + jumeau notebook, sorry = 0 en production, proof-integrity).
• Honnêteté de cadrage requise : la définition complète de Φ (IIT 3.0) est lourde à formaliser. La cible réaliste est un substitut tractable — une borne inférieure d'intégration sur une famille explicite de graphes — avec le grade écrit. Promettre Φ intégral serait exactement le genre de sur-montée que la hiérarchie de sobriété ICT interdit.

C'est la veine la plus lourde et la plus rentable : elle donnerait à ICT son premier organe prouvé, et à la critique son statut de théorème plutôt que d'anecdote.

Veine 6 — acquisition bibliographique (préalable, pas livrable)

Le brief : « Why Philosophers Should Care… est sans doute avec ses autres grandes publications séminales à intégrer à notre biblio ».

0 PDF au gisement aujourd'hui. Comme #16741 (Tegmark) a commencé par 16 lectures, celui-ci commence par une acquisition. Publications à archiver au gisement G:\Mon Drive\MyIA\IA\Bibliographie IA — jamais committées (bibliography-hygiene), chemin GDrive cité dans chaque issue fille.

Noyau de départ : The Ghost in the Quantum Turing Machine (2013) · Why Philosophers Should Care About Computational Complexity (2011) · The Computational Complexity of Linear Optics (Aaronson–Arkhipov, 2011) · les textes de la veine 4 · les billets de la veine 5.

---

Ce que cet Epic n'est pas

• Pas une collection. Le brief l'a dit avant moi : on ne fait pas entrer un grand nom pour le plaisir. Chaque veine doit produire, ou rester une note.
• Pas une pré-curation. Aucune issue fille n'est créée ici, hors Complexity-03 : Aaronson entre par la permanente, pas par la strate 7 (BosonSampling, perm vs det mesures exactes) #16779 qui existait déjà. Une veine devient une issue quand sa source est lue et sa cible vérifiée contre le dépôt.
• Pas un ré-arbitrage d'ICT. La resync de la tresse et la coquille strate-7 vivent sur ICT : resync de la tresse sur l'arc strate-1..7 — la tranche morte avec la fermeture de #7424 #16777.

Règles de livraison

• Publications au gisement, jamais dans le dépôt ; chemin GDrive dans chaque issue fille.
• Chaque issue fille cite sa cible vérifiée contre l'arbre (patron Epic : distillation du corpus Tegmark — physique de l'apprentissage, géométrie du latent, IA prouvable, MUH #16741).
• Notebooks : C.1 (aucune erreur volontaire), C.2 (committés avec sorties réelles), ≥ 3 exercices.
• Lean : sorry = 0 en production, proof-integrity vert, grade écrit.
• Tag Grain: à la livraison (PR), pas sur les issues.

Rattachements

#16779 (veine 1, ouverte) · #16777 (resync tresse + coquille strate 7) · #16759 (le critère « un organe, pas une citation ») · #16775 (Epic Schmidhuber — même patron parapluie) · #16741 (Epic Tegmark — patron de curation par lectures) · #4588 (Epic ICT)

[myia-ai-01]

Précision de provenance sur la veine 5 — et ce que l'Epic avait déjà bon

Arbitrage user du 2026-09-19, sur la base d'un audit externe qui a re-groundé les nouveaux Epics d'auteurs. Cet Epic ressort comme le plus sain des trois, précisément parce qu'il reconnaît n'avoir presque aucune implantation : pas de freebits dans les notebooks, pas de corpus bibliographique local, donc six veines à curater, pas six notebooks commandés. C'est le bon contrat, il est conservé.

Deux points, dont un seul est une correction.

Ce que l'Epic avait déjà bon, et que je ne veux pas voir « corrigé » par un cycle futur

La ligne 57 pose déjà l'honnêteté de cadrage : Φ intégral (IIT 3.0) est lourd à formaliser, la cible réaliste est un substitut tractable avec le grade écrit, et promettre Φ intégral serait la sur-montée que la hiérarchie de sobriété ICT interdit. La ligne 59 dit que la formalisation donnerait à la critique son statut de théorème « plutôt que d'anecdote » — donc qu'elle ne l'a pas aujourd'hui.

Ces deux phrases sont exactes et ce sont elles qui tiennent la veine. Un futur grain qui les trouverait « timides » et les remonterait en promesse ferait exactement le défaut que l'Epic a su éviter.

La correction : la provenance, qui n'est pas celle qu'on croira

La critique d'IIT par les constructions à Φ élevé est une critique quantitative, publique et substantielle — elle n'est pas anecdotique, et le brief a raison de la traiter comme un objet sérieux. Mais elle vit dans un billet de blog (Why I Am Not An Integrated Information Theorist, mai 2014), pas dans une publication formelle. Il n'existe pas de « théorème Aaronson sur IIT » dans un article à citer.

Cela a trois conséquences opérationnelles, et c'est pourquoi je l'écris ici plutôt que de laisser le grain bibliographique le découvrir :

1. Le grain d'acquisition ne doit pas chercher un papier qui n'existe pas. Un codebase_search ou une recherche bibliographique qui rend zéro sur « Aaronson IIT theorem » mesurerait l'absence d'un objet inexistant, pas une lacune du dépôt. C'est un faux négatif garanti par la construction de la requête.
2. La formalisation Lean est le geste qui crée l'objet formel, elle ne le transcrit pas. L'écart est précisément ce qui fait la valeur de la veine — et ce qui interdit de la présenter comme une mise en Lean d'un résultat publié.
3. Le grade écrit porte sur l'énoncé qu'on formalise, pas sur la critique. Condition d'ouverture du lake, à tenir avant la première ligne : figer la version de Φ et l'énoncé tractable retenu, nommément, dans le body du grain. Un lake ouvert sans ces deux-là formaliserait une cible mouvante.

La borne S7, qui vaut pour cet Epic nommément

Cet Epic ne remplit pas S7 parce que Ghost in the Quantum Turing Machine parle de freebits. S7 est correctement redevenue vide depuis que #13908 a révoqué la fiction « ICT-26→30 = S7 », et #16777 resynchronise les docs qui disent encore le contraire.

Le gate S7 est : un premier organe freebits réellement exécutable et falsifiable. Ni une documentation brillante, ni un nouveau nom dans la tresse, ni une preuve Lean voisine ne compte comme franchissement. Il faut qu'Aaronson fournisse un organe, et que cet organe rencontre le contrat de S7 — c'est #16759 (« une fibre s'acquiert par un organe, pas par une citation ») appliqué à une strate.

L'intuition freebits d'ordre 2 reste une hypothèse candidate. La présence de son auteur dans un Epic ne lui ajoute aucune preuve.

Régime

Curation limitée, comme #16775 : acquisition → lecture → résonance vérifiée → organe éventuel, avec très peu de grains d'implémentation simultanés. Détail du changement de régime : #16473.

— ai-01, 2026-09-19

[jsboige]

[INFO] candidate-delivered — lane myia-po-2026:CoursIA-2 — 2026-10-02

Le picker sert cette issue comme grain neuf. Le preflight de claim montre qu'elle est résolue en substance, et je n'ai rien ré-implémenté.

Preuve firsthand : 5 PRs en lien, toutes MERGED :

• feat(complexity,#16779): notebook 03 Aaronson-Arkhipov — permanente/BosonSampling #16850 — organe Aaronson (première veine)
• Add: Complexity-04 — Gottesman-Knill comme arbitre executable (curation Aaronson veine 4) #17045 — extension
• feat(iit,#17378): IIT-06 — l'échange Aaronson/Tononi exécuté (Φ_DM + PyPhi) #17380 — extension
• feat(complexity,#17767): notebook Complexity-07 -- Zoo navigable (inclusions executees, oracles BGS) #17769 — clôture
• Add: iit_lean — premier lake IIT, proxy relationnel de coupe (Phase 1, #18599) #18603 — lake Lean d'IIT lié

Aucune fermeture posée (Tell c.1502 strict fondateur), aucun label, aucune ré-implémentation.