From c4c17a95fc555c4f5b3384bb06ffad7eedf4f3ad Mon Sep 17 00:00:00 2001 From: jsboige Date: Wed, 14 Oct 2026 05:30:50 +0200 Subject: [PATCH 1/4] Add(iit,#20649): marche 2 de l'escalier iit_lean -- IIT-08 Parite-et-Broadcast-Lean (theoremes B et C) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Carnet consommateur du lake iit_lean (declarations 11-19, non couvertes par la marche 1 #20419) : outil parite + 4 lemmes, systeme broadcast, oracle d'orbites par enumeration (n=2 unique point fixe, n=3 deux points fixes, convergence <= 2 pas, colonnes pas3=pas4 mesurant le theoreme C), theoreme B broadcast_integrated ([propext] seul), theoreme C broadcast_two_cycle + alias figé broadcast_trivial_dynamics (#18599), contraste A/B, critique d'Aaronson, 3 exercices C.1. Kernel lean4-wsl, 16/16 cellules, 0 erreur, 12.9 s. Pre-commit: normalisation papermill-paths appliquee (tolerance admise). README serie + LEAN_INVENTORY differes au merge #20419 (path README partage). Co-Authored-By: Claude Sonnet 5.5 --- .../IIT/IIT-08-Parite-et-Broadcast-Lean.ipynb | 2215 +++++++++++++++++ 1 file changed, 2215 insertions(+) create mode 100644 MyIA.AI.Notebooks/IIT/IIT-08-Parite-et-Broadcast-Lean.ipynb diff --git a/MyIA.AI.Notebooks/IIT/IIT-08-Parite-et-Broadcast-Lean.ipynb b/MyIA.AI.Notebooks/IIT/IIT-08-Parite-et-Broadcast-Lean.ipynb new file mode 100644 index 0000000000..9e3605aa35 --- /dev/null +++ b/MyIA.AI.Notebooks/IIT/IIT-08-Parite-et-Broadcast-Lean.ipynb @@ -0,0 +1,2215 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "d0a464a9", + "metadata": { + "papermill": { + "duration": 0.005408, + "end_time": "2026-10-14T03:30:05.119690+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:05.114282+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "# IIT-08 — Parité et broadcast : le couple qui a mordu IIT\n", + "\n", + "**Marche 2 de l'escalier `iit_lean`** (issue #20649, escalier #20414, veine 5 de l'EPIC #16781).\n", + "La marche 1 ([IIT-07](https://github.com/jsboige/CoursIA), PR #20419) a établi le vocabulaire de\n", + "la coupe et le verdict de décomposabilité : le théorème A dit que l'identité est décomposable.\n", + "\n", + "Ce carnet monte les deux pièces qui manquent à la critique :\n", + "\n", + "- **l'outil parité** (`parity`) et ses quatre lemmes ;\n", + "- **le système broadcast-parité** (`broadcast`), dont l'image se réduit à deux états constants ;\n", + "- **le théorème B** (`broadcast_integrated`) : le broadcast est *intégré pour toute coupe* —\n", + " c'est « l'objet qui a mordu IIT » érigé en théorème ;\n", + "- **le théorème C** (`broadcast_two_cycle`) : la dynamique de ce même objet est *triviale* —\n", + " toute orbite atteint un point fixe en deux pas.\n", + "\n", + "Le couple **B et C** est le contenu formel de la critique d'Aaronson contre le proxy\n", + "d'intégration : intégration maximale, comportement nul." + ] + }, + { + "cell_type": "markdown", + "id": "d8a4fb0f", + "metadata": { + "papermill": { + "duration": 0.002369, + "end_time": "2026-10-14T03:30:05.126815+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:05.124446+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 0. Ce que ce carnet démontre\n", + "\n", + "1. La parité d'un état se calcule (outil exécutable, mesuré sur des états concrets).\n", + "2. Le broadcast uniformise : l'état suivant ne dépend que de la parité de l'état courant.\n", + "3. Un oracle par énumération mesure les orbites : point fixe atteint en au plus deux pas,\n", + " et la troisième itération égale toujours la deuxième (théorème C rendu visible).\n", + "4. Le théorème B atteste l'intégration universelle du même objet — le contraste avec le\n", + " théorème A de la marche 1 est le cœur du débat.\n", + "\n", + "Le carnet consomme le lake `iit_lean` (kernel `lean4-wsl`) **sans le modifier** : toutes les\n", + "définitions et théorèmes viennent de `IIT.Integration`." + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "0117f8d2", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:05.131556Z", + "iopub.status.busy": "2026-10-14T03:30:05.131286Z", + "iopub.status.idle": "2026-10-14T03:30:13.541277Z", + "shell.execute_reply": "2026-10-14T03:30:13.540198Z" + }, + "papermill": { + "duration": 8.413205, + "end_time": "2026-10-14T03:30:13.541993+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:05.128788+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
import IIT.Integration
\n", + "
open IIT
\n", + "
\n", + "
-- Le contrat du carnet : outil, systeme, theoremes B et C, alias figes
\n", + "
 parity : (n : Nat) → State n → Bool
\n", + "
 @broadcast : {n : Nat} → System n
\n", + "
 @broadcast_integrated : ∀ {n : Nat}, integrated broadcast
\n", + "
 @broadcast_two_cycle : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)
\n", + "
 @broadcast_trivial_dynamics : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)
\n", + "
--% env 0
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"import IIT.Integration\\nopen IIT\\n\\n-- Le contrat du carnet : outil, systeme, theoremes B et C, alias figes\\n#check @parity\\n#check @broadcast\\n#check @broadcast_integrated\\n#check @broadcast_two_cycle\\n#check @broadcast_trivial_dynamics\"}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 6},\r\n", + " \"data\": \"parity : (n : Nat) → State n → Bool\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 6, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 6, \"column\": 6},\r\n", + " \"data\": \"@broadcast : {n : Nat} → System n\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 6},\r\n", + " \"data\": \"@broadcast_integrated : ∀ {n : Nat}, integrated broadcast\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 8, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 8, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@broadcast_two_cycle : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 9, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 9, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@broadcast_trivial_dynamics : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)\"}],\r\n", + " \"env\": 0}\n", + "
\n", + " " + ], + "text/plain": [ + "import IIT.Integration\n", + "open IIT\n", + "\n", + "-- Le contrat du carnet : outil, systeme, theoremes B et C, alias figes\n", + "#check @parity\n", + "──────▶ parity : (n : Nat) → State n → Bool\n", + "#check @broadcast\n", + "──────▶ @broadcast : {n : Nat} → System n\n", + "#check @broadcast_integrated\n", + "──────▶ @broadcast_integrated : ∀ {n : Nat}, integrated broadcast\n", + "#check @broadcast_two_cycle\n", + "──────▶ @broadcast_two_cycle : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)\n", + "#check @broadcast_trivial_dynamics\n", + "──────▶ @broadcast_trivial_dynamics : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)\n", + "--% env 0\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"import IIT.Integration\\nopen IIT\\n\\n-- Le contrat du carnet : outil, systeme, theoremes B et C, alias figes\\n#check @parity\\n#check @broadcast\\n#check @broadcast_integrated\\n#check @broadcast_two_cycle\\n#check @broadcast_trivial_dynamics\"}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 6},\r\n", + " \"data\": \"parity : (n : Nat) → State n → Bool\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 6, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 6, \"column\": 6},\r\n", + " \"data\": \"@broadcast : {n : Nat} → System n\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 6},\r\n", + " \"data\": \"@broadcast_integrated : ∀ {n : Nat}, integrated broadcast\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 8, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 8, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@broadcast_two_cycle : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 9, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 9, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@broadcast_trivial_dynamics : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)\"}],\r\n", + " \"env\": 0}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "import IIT.Integration\n", + "open IIT\n", + "\n", + "-- Le contrat du carnet : outil, systeme, theoremes B et C, alias figes\n", + "#check @parity\n", + "#check @broadcast\n", + "#check @broadcast_integrated\n", + "#check @broadcast_two_cycle\n", + "#check @broadcast_trivial_dynamics" + ] + }, + { + "cell_type": "markdown", + "id": "fe9d0755", + "metadata": { + "papermill": { + "duration": 0.00192, + "end_time": "2026-10-14T03:30:13.546069+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:13.544149+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "Lecture du contrat :\n", + "\n", + "- `parity : (n : Nat) → State n → Bool` — la parité (nombre de bits vrais modulo 2),\n", + " par récurrence sur la taille ;\n", + "- `broadcast : System n` — le système : chaque bit de l'état suivant vaut la parité de\n", + " l'état courant ;\n", + "- `broadcast_integrated : integrated broadcast` — le théorème B ;\n", + "- `broadcast_two_cycle` — le théorème C : `broadcast (broadcast (broadcast s)) = broadcast (broadcast s)` ;\n", + "- `broadcast_trivial_dynamics` — l'**énoncé figé n° 3 de #18599**, alias du théorème C sous\n", + " le nom gelé dans l'issue fondatrice du lake." + ] + }, + { + "cell_type": "markdown", + "id": "efa38027", + "metadata": { + "papermill": { + "duration": 0.00177, + "end_time": "2026-10-14T03:30:13.549649+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:13.547879+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 1. L'outil parité\n", + "\n", + "Trois états témoins en taille 3, et des tuples de bits pour *voir* les états (les fonctions\n", + "`Fin n → Bool` n'ont pas d'égalité décisionnelle : on compare leurs tuples de bits)." + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "8c34a3fa", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:13.554432Z", + "iopub.status.busy": "2026-10-14T03:30:13.554258Z", + "iopub.status.idle": "2026-10-14T03:30:13.745200Z", + "shell.execute_reply": "2026-10-14T03:30:13.744275Z" + }, + "papermill": { + "duration": 0.19439, + "end_time": "2026-10-14T03:30:13.745798+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:13.551408+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Etats temoins en taille 3
\n", + "
def sOneHot : State 3 := fun j => decide (j.val = 0)
\n", + "
def sTrue3  : State 3 := fun _ => true
\n", + "
def sMix3    : State 3 := fun j => decide (j.val = 1)
\n", + "
\n", + "
-- Tuples de bits (l'egalite decisionnelle vit sur les tuples, pas sur les fonctions)
\n", + "
def bits2 (s : State 2) : Bool × Bool := (s 0, s 1)
\n", + "
def bits3 (s : State 3) : Bool × Bool × Bool := (s 0, s 1, s 2)
\n", + "
\n", + "
-- Trois mesures de parite
\n", + "
 (true, false, false)
\n", + "
 (true, true, true)
\n", + "
 (false, true, false)
\n", + "
 true
\n", + "
 true
\n", + "
 true
\n", + "
--% env 1
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Etats temoins en taille 3\\ndef sOneHot : State 3 := fun j => decide (j.val = 0)\\ndef sTrue3 : State 3 := fun _ => true\\ndef sMix3 : State 3 := fun j => decide (j.val = 1)\\n\\n-- Tuples de bits (l'egalite decisionnelle vit sur les tuples, pas sur les fonctions)\\ndef bits2 (s : State 2) : Bool \\u00d7 Bool := (s 0, s 1)\\ndef bits3 (s : State 3) : Bool \\u00d7 Bool \\u00d7 Bool := (s 0, s 1, s 2)\\n\\n-- Trois mesures de parite\\n#eval bits3 sOneHot\\n#eval bits3 sTrue3\\n#eval bits3 sMix3\\n#eval parity 3 sOneHot\\n#eval parity 3 sTrue3\\n#eval parity 3 sMix3\", \"env\": 0}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 11, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 11, \"column\": 5},\r\n", + " \"data\": \"(true, false, false)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 12, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 12, \"column\": 5},\r\n", + " \"data\": \"(true, true, true)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 13, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 13, \"column\": 5},\r\n", + " \"data\": \"(false, true, false)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 14, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 14, \"column\": 5},\r\n", + " \"data\": \"true\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 15, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 15, \"column\": 5},\r\n", + " \"data\": \"true\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 16, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 16, \"column\": 5},\r\n", + " \"data\": \"true\"}],\r\n", + " \"env\": 1}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Etats temoins en taille 3\n", + "def sOneHot : State 3 := fun j => decide (j.val = 0)\n", + "def sTrue3 : State 3 := fun _ => true\n", + "def sMix3 : State 3 := fun j => decide (j.val = 1)\n", + "\n", + "-- Tuples de bits (l'egalite decisionnelle vit sur les tuples, pas sur les fonctions)\n", + "def bits2 (s : State 2) : Bool × Bool := (s 0, s 1)\n", + "def bits3 (s : State 3) : Bool × Bool × Bool := (s 0, s 1, s 2)\n", + "\n", + "-- Trois mesures de parite\n", + "#eval bits3 sOneHot\n", + "─────▶ (true, false, false)\n", + "#eval bits3 sTrue3\n", + "─────▶ (true, true, true)\n", + "#eval bits3 sMix3\n", + "─────▶ (false, true, false)\n", + "#eval parity 3 sOneHot\n", + "─────▶ true\n", + "#eval parity 3 sTrue3\n", + "─────▶ true\n", + "#eval parity 3 sMix3\n", + "─────▶ true\n", + "--% env 1\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Etats temoins en taille 3\\ndef sOneHot : State 3 := fun j => decide (j.val = 0)\\ndef sTrue3 : State 3 := fun _ => true\\ndef sMix3 : State 3 := fun j => decide (j.val = 1)\\n\\n-- Tuples de bits (l'egalite decisionnelle vit sur les tuples, pas sur les fonctions)\\ndef bits2 (s : State 2) : Bool \\u00d7 Bool := (s 0, s 1)\\ndef bits3 (s : State 3) : Bool \\u00d7 Bool \\u00d7 Bool := (s 0, s 1, s 2)\\n\\n-- Trois mesures de parite\\n#eval bits3 sOneHot\\n#eval bits3 sTrue3\\n#eval bits3 sMix3\\n#eval parity 3 sOneHot\\n#eval parity 3 sTrue3\\n#eval parity 3 sMix3\", \"env\": 0}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 11, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 11, \"column\": 5},\r\n", + " \"data\": \"(true, false, false)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 12, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 12, \"column\": 5},\r\n", + " \"data\": \"(true, true, true)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 13, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 13, \"column\": 5},\r\n", + " \"data\": \"(false, true, false)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 14, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 14, \"column\": 5},\r\n", + " \"data\": \"true\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 15, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 15, \"column\": 5},\r\n", + " \"data\": \"true\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 16, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 16, \"column\": 5},\r\n", + " \"data\": \"true\"}],\r\n", + " \"env\": 1}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Etats temoins en taille 3\n", + "def sOneHot : State 3 := fun j => decide (j.val = 0)\n", + "def sTrue3 : State 3 := fun _ => true\n", + "def sMix3 : State 3 := fun j => decide (j.val = 1)\n", + "\n", + "-- Tuples de bits (l'egalite decisionnelle vit sur les tuples, pas sur les fonctions)\n", + "def bits2 (s : State 2) : Bool × Bool := (s 0, s 1)\n", + "def bits3 (s : State 3) : Bool × Bool × Bool := (s 0, s 1, s 2)\n", + "\n", + "-- Trois mesures de parite\n", + "#eval bits3 sOneHot\n", + "#eval bits3 sTrue3\n", + "#eval bits3 sMix3\n", + "#eval parity 3 sOneHot\n", + "#eval parity 3 sTrue3\n", + "#eval parity 3 sMix3" + ] + }, + { + "cell_type": "markdown", + "id": "30683275", + "metadata": { + "papermill": { + "duration": 0.002085, + "end_time": "2026-10-14T03:30:13.750220+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:13.748135+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "Lecture : `(true, false, false)` porte un bit vrai — parité `true` ;\n", + "`(true, true, true)` en porte trois — parité `true` ; `(false, true, false)` en porte un —\n", + "parité `true`. Les trois états témoins ont une parité impaire : la *valeur* de l'état change,\n", + "la parité capture un invariant global (la somme modulo 2 de tous les bits)." + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "a33f7d14", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:13.755092Z", + "iopub.status.busy": "2026-10-14T03:30:13.754924Z", + "iopub.status.idle": "2026-10-14T03:30:13.907574Z", + "shell.execute_reply": "2026-10-14T03:30:13.906720Z" + }, + "papermill": { + "duration": 0.156003, + "end_time": "2026-10-14T03:30:13.908156+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:13.752153+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Les quatre lemmes de l'outil parite
\n", + "
 parity_allFalse : ∀ (n : Nat) (s : State n), (∀ (i : Fin n), s i = false) → parity n s = false
\n", + "
 @parity_allTrue : ∀ {n : Nat}, (parity n fun x => true) = decide (n % 2 = 1)
\n", + "
 parity_oneHot_zero : ∀ (n : Nat), 0 < n → (parity n fun j => decide (↑j = 0)) = true
\n", + "
 parity_const : ∀ (n : Nat) (b : Bool), (parity n fun x => b) = (b && decide (n % 2 = 1))
\n", + "
--% env 2
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Les quatre lemmes de l'outil parite\\n#check @parity_allFalse\\n#check @parity_allTrue\\n#check @parity_oneHot_zero\\n#check @parity_const\", \"env\": 1}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"parity_allFalse : ∀ (n : Nat) (s : State n), (∀ (i : Fin n), s i = false) → parity n s = false\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@parity_allTrue : ∀ {n : Nat}, (parity n fun x => true) = decide (n % 2 = 1)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"parity_oneHot_zero : ∀ (n : Nat), 0 < n → (parity n fun j => decide (↑j = 0)) = true\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"parity_const : ∀ (n : Nat) (b : Bool), (parity n fun x => b) = (b && decide (n % 2 = 1))\"}],\r\n", + " \"env\": 2}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Les quatre lemmes de l'outil parite\n", + "#check @parity_allFalse\n", + "──────▶ parity_allFalse : ∀ (n : Nat) (s : State n), (∀ (i : Fin n), s i = false) → parity n s = false\n", + "#check @parity_allTrue\n", + "──────▶ @parity_allTrue : ∀ {n : Nat}, (parity n fun x => true) = decide (n % 2 = 1)\n", + "#check @parity_oneHot_zero\n", + "──────▶ parity_oneHot_zero : ∀ (n : Nat), 0 < n → (parity n fun j => decide (↑j = 0)) = true\n", + "#check @parity_const\n", + "──────▶ parity_const : ∀ (n : Nat) (b : Bool), (parity n fun x => b) = (b && decide (n % 2 = 1))\n", + "--% env 2\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Les quatre lemmes de l'outil parite\\n#check @parity_allFalse\\n#check @parity_allTrue\\n#check @parity_oneHot_zero\\n#check @parity_const\", \"env\": 1}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"parity_allFalse : ∀ (n : Nat) (s : State n), (∀ (i : Fin n), s i = false) → parity n s = false\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@parity_allTrue : ∀ {n : Nat}, (parity n fun x => true) = decide (n % 2 = 1)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"parity_oneHot_zero : ∀ (n : Nat), 0 < n → (parity n fun j => decide (↑j = 0)) = true\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"parity_const : ∀ (n : Nat) (b : Bool), (parity n fun x => b) = (b && decide (n % 2 = 1))\"}],\r\n", + " \"env\": 2}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Les quatre lemmes de l'outil parite\n", + "#check @parity_allFalse\n", + "#check @parity_allTrue\n", + "#check @parity_oneHot_zero\n", + "#check @parity_const" + ] + }, + { + "cell_type": "markdown", + "id": "e1401022", + "metadata": { + "papermill": { + "duration": 0.002145, + "end_time": "2026-10-14T03:30:13.912582+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:13.910437+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "Lecture des quatre lemmes :\n", + "\n", + "- `parity_allFalse` : un état tout-faux a une parité nulle ;\n", + "- `parity_allTrue` : un état tout-vrai code **l'imparité de la taille** `n` — la parité d'un\n", + " état uniforme dépend du nombre de bits, pas de leur valeur ;\n", + "- `parity_oneHot_zero` : un seul bit vrai (indice 0) rend la parité impaire, quelle que soit\n", + " la taille — c'est le lemme pivot de la preuve du théorème B ;\n", + "- `parity_const` : la forme générale — la parité d'un état constant vaut\n", + " `b && decide (n % 2 = 1)`." + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "56263840", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:13.917533Z", + "iopub.status.busy": "2026-10-14T03:30:13.917351Z", + "iopub.status.idle": "2026-10-14T03:30:14.085263Z", + "shell.execute_reply": "2026-10-14T03:30:14.084322Z" + }, + "papermill": { + "duration": 0.171641, + "end_time": "2026-10-14T03:30:14.086273+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:13.914632+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Mesure du lemme parity_const sur les deux tailles
\n", + "
 false
\n", + "
 true
\n", + "
--% env 3
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Mesure du lemme parity_const sur les deux tailles\\n#eval parity 4 (fun _ => true)\\n#eval parity 5 (fun _ => true)\", \"env\": 2}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 5},\r\n", + " \"data\": \"false\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 5},\r\n", + " \"data\": \"true\"}],\r\n", + " \"env\": 3}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Mesure du lemme parity_const sur les deux tailles\n", + "#eval parity 4 (fun _ => true)\n", + "─────▶ false\n", + "#eval parity 5 (fun _ => true)\n", + "─────▶ true\n", + "--% env 3\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Mesure du lemme parity_const sur les deux tailles\\n#eval parity 4 (fun _ => true)\\n#eval parity 5 (fun _ => true)\", \"env\": 2}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 5},\r\n", + " \"data\": \"false\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 5},\r\n", + " \"data\": \"true\"}],\r\n", + " \"env\": 3}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Mesure du lemme parity_const sur les deux tailles\n", + "#eval parity 4 (fun _ => true)\n", + "#eval parity 5 (fun _ => true)" + ] + }, + { + "cell_type": "markdown", + "id": "0027ba0b", + "metadata": { + "papermill": { + "duration": 0.002524, + "end_time": "2026-10-14T03:30:14.091237+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:14.088713+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "Mesure : en taille 4 (pair), l'état tout-vrai a une parité `false` ; en taille 5 (impair),\n", + "une parité `true` — exactement `decide (n % 2 = 1)`, le comportement promis par\n", + "`parity_const`. Le broadcast en taille paire ne pourra donc jamais stabiliser l'état\n", + "tout-vrai : c'est ce que l'oracle confirmera." + ] + }, + { + "cell_type": "markdown", + "id": "75d5b95c", + "metadata": { + "papermill": { + "duration": 0.002257, + "end_time": "2026-10-14T03:30:14.096182+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:14.093925+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 2. Le système broadcast : un pas\n", + "\n", + "`broadcast s` est l'état **uniforme** dont chaque bit vaut `parity n s` : l'information\n", + "globale (la parité) est diffusée partout dans l'état suivant." + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "42bc40db", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:14.101702Z", + "iopub.status.busy": "2026-10-14T03:30:14.101509Z", + "iopub.status.idle": "2026-10-14T03:30:14.281492Z", + "shell.execute_reply": "2026-10-14T03:30:14.280505Z" + }, + "papermill": { + "duration": 0.183868, + "end_time": "2026-10-14T03:30:14.282342+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:14.098474+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Un pas de broadcast sur les temoins
\n", + "
 (true, true, true)
\n", + "
 (true, true, true)
\n", + "
 (true, true, true)
\n", + "
--% env 4
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Un pas de broadcast sur les temoins\\n#eval bits3 (broadcast sOneHot)\\n#eval bits3 (broadcast sTrue3)\\n#eval bits3 (broadcast sMix3)\", \"env\": 3}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 5},\r\n", + " \"data\": \"(true, true, true)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 5},\r\n", + " \"data\": \"(true, true, true)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 5},\r\n", + " \"data\": \"(true, true, true)\"}],\r\n", + " \"env\": 4}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Un pas de broadcast sur les temoins\n", + "#eval bits3 (broadcast sOneHot)\n", + "─────▶ (true, true, true)\n", + "#eval bits3 (broadcast sTrue3)\n", + "─────▶ (true, true, true)\n", + "#eval bits3 (broadcast sMix3)\n", + "─────▶ (true, true, true)\n", + "--% env 4\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Un pas de broadcast sur les temoins\\n#eval bits3 (broadcast sOneHot)\\n#eval bits3 (broadcast sTrue3)\\n#eval bits3 (broadcast sMix3)\", \"env\": 3}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 5},\r\n", + " \"data\": \"(true, true, true)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 5},\r\n", + " \"data\": \"(true, true, true)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 5},\r\n", + " \"data\": \"(true, true, true)\"}],\r\n", + " \"env\": 4}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Un pas de broadcast sur les temoins\n", + "#eval bits3 (broadcast sOneHot)\n", + "#eval bits3 (broadcast sTrue3)\n", + "#eval bits3 (broadcast sMix3)" + ] + }, + { + "cell_type": "markdown", + "id": "fe348a7b", + "metadata": { + "papermill": { + "duration": 0.002434, + "end_time": "2026-10-14T03:30:14.287329+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:14.284895+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "Lecture : les trois états témoins (tous de parité impaire) sont envoyés sur le **même**\n", + "état uniforme `(true, true, true)`. Le broadcast oublie tout de l'état courant sauf sa\n", + "parité — c'est une projection à une bit d'information, puis une diffusion." + ] + }, + { + "cell_type": "markdown", + "id": "aee504e3", + "metadata": { + "papermill": { + "duration": 0.002389, + "end_time": "2026-10-14T03:30:14.292068+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:14.289679+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 3. Oracle : les orbites par énumération\n", + "\n", + "L'oracle énumère les `2^n` états et imprime, pour chaque état de départ, le tuple de bits\n", + "après 0, 1, 2 et 3 applications du broadcast." + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "66091f89", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:14.297859Z", + "iopub.status.busy": "2026-10-14T03:30:14.297652Z", + "iopub.status.idle": "2026-10-14T03:30:14.485884Z", + "shell.execute_reply": "2026-10-14T03:30:14.485033Z" + }, + "papermill": { + "duration": 0.192102, + "end_time": "2026-10-14T03:30:14.486573+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:14.294471+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Oracle : enumeration exhaustive des etats par leur code entier
\n", + "
def stateOfNat (n : Nat) (v : Nat) : State n := fun i => ((v >>> i.val) % 2) == 1
\n", + "
def allStates (n : Nat) : List (State n) := (List.range (2 ^ n)).map (stateOfNat n)
\n", + "
\n", + "
 [(false, false), (true, false), (false, true), (true, true)]
\n", + "
--% env 5
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Oracle : enumeration exhaustive des etats par leur code entier\\ndef stateOfNat (n : Nat) (v : Nat) : State n := fun i => ((v >>> i.val) % 2) == 1\\ndef allStates (n : Nat) : List (State n) := (List.range (2 ^ n)).map (stateOfNat n)\\n\\n#eval (allStates 2).map bits2\", \"env\": 4}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 5},\r\n", + " \"data\": \"[(false, false), (true, false), (false, true), (true, true)]\"}],\r\n", + " \"env\": 5}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Oracle : enumeration exhaustive des etats par leur code entier\n", + "def stateOfNat (n : Nat) (v : Nat) : State n := fun i => ((v >>> i.val) % 2) == 1\n", + "def allStates (n : Nat) : List (State n) := (List.range (2 ^ n)).map (stateOfNat n)\n", + "\n", + "#eval (allStates 2).map bits2\n", + "─────▶ [(false, false), (true, false), (false, true), (true, true)]\n", + "--% env 5\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Oracle : enumeration exhaustive des etats par leur code entier\\ndef stateOfNat (n : Nat) (v : Nat) : State n := fun i => ((v >>> i.val) % 2) == 1\\ndef allStates (n : Nat) : List (State n) := (List.range (2 ^ n)).map (stateOfNat n)\\n\\n#eval (allStates 2).map bits2\", \"env\": 4}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 5},\r\n", + " \"data\": \"[(false, false), (true, false), (false, true), (true, true)]\"}],\r\n", + " \"env\": 5}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Oracle : enumeration exhaustive des etats par leur code entier\n", + "def stateOfNat (n : Nat) (v : Nat) : State n := fun i => ((v >>> i.val) % 2) == 1\n", + "def allStates (n : Nat) : List (State n) := (List.range (2 ^ n)).map (stateOfNat n)\n", + "\n", + "#eval (allStates 2).map bits2" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "5226f2d2", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:14.493758Z", + "iopub.status.busy": "2026-10-14T03:30:14.493583Z", + "iopub.status.idle": "2026-10-14T03:30:14.659434Z", + "shell.execute_reply": "2026-10-14T03:30:14.658356Z" + }, + "papermill": { + "duration": 0.171136, + "end_time": "2026-10-14T03:30:14.660441+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:14.489305+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Orbites en taille 2 : (depart, pas 1, pas 2, pas 3)
\n", + "
 [((false, false), (false, false), (false, false), false, false),\n",
+       " ((true, false), (true, true), (false, false), false, false),\n",
+       " ((false, true), (true, true), (false, false), false, false),\n",
+       " ((true, true), (false, false), (false, false), false, false)]
\n", + "
  (bits2 s,
\n", + "
   bits2 (broadcast s),
\n", + "
   bits2 (broadcast (broadcast s)),
\n", + "
   bits2 (broadcast (broadcast (broadcast s)))))
\n", + "
--% env 6
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Orbites en taille 2 : (depart, pas 1, pas 2, pas 3)\\n#eval (allStates 2).map (fun s =>\\n (bits2 s,\\n bits2 (broadcast s),\\n bits2 (broadcast (broadcast s)),\\n bits2 (broadcast (broadcast (broadcast s)))))\", \"env\": 5}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 5},\r\n", + " \"data\":\r\n", + " \"[((false, false), (false, false), (false, false), false, false),\\n ((true, false), (true, true), (false, false), false, false),\\n ((false, true), (true, true), (false, false), false, false),\\n ((true, true), (false, false), (false, false), false, false)]\"}],\r\n", + " \"env\": 6}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Orbites en taille 2 : (depart, pas 1, pas 2, pas 3)\n", + "#eval (allStates 2).map (fun s =>\n", + "─────▶ [((false, false), (false, false), (false, false), false, false),\n", + " ((true, false), (true, true), (false, false), false, false),\n", + " ((false, true), (true, true), (false, false), false, false),\n", + " ((true, true), (false, false), (false, false), false, false)]\n", + " (bits2 s,\n", + " bits2 (broadcast s),\n", + " bits2 (broadcast (broadcast s)),\n", + " bits2 (broadcast (broadcast (broadcast s)))))\n", + "--% env 6\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Orbites en taille 2 : (depart, pas 1, pas 2, pas 3)\\n#eval (allStates 2).map (fun s =>\\n (bits2 s,\\n bits2 (broadcast s),\\n bits2 (broadcast (broadcast s)),\\n bits2 (broadcast (broadcast (broadcast s)))))\", \"env\": 5}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 5},\r\n", + " \"data\":\r\n", + " \"[((false, false), (false, false), (false, false), false, false),\\n ((true, false), (true, true), (false, false), false, false),\\n ((false, true), (true, true), (false, false), false, false),\\n ((true, true), (false, false), (false, false), false, false)]\"}],\r\n", + " \"env\": 6}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Orbites en taille 2 : (depart, pas 1, pas 2, pas 3)\n", + "#eval (allStates 2).map (fun s =>\n", + " (bits2 s,\n", + " bits2 (broadcast s),\n", + " bits2 (broadcast (broadcast s)),\n", + " bits2 (broadcast (broadcast (broadcast s)))))" + ] + }, + { + "cell_type": "markdown", + "id": "de71e1aa", + "metadata": { + "papermill": { + "duration": 0.002826, + "end_time": "2026-10-14T03:30:14.666170+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:14.663344+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "Lecture de la table (taille 2, paire) :\n", + "\n", + "- chaque ligne converge vers `(false, false)` — l'unique point fixe en taille paire\n", + " (l'état tout-vrai a une parité nulle, cf. la mesure de `parity_const` en taille 4) ;\n", + "- `(false, true)` et `(true, false)` passent par `(true, true)` au pas 1 puis atteignent\n", + " leur point fixe au pas 2 : convergence en **au plus deux pas** ;\n", + "- **les colonnes 3 et 4 sont identiques partout** : la troisième itération ne change rien —\n", + " le théorème C est déjà visible dans la mesure." + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "id": "0e76309a", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:14.673368Z", + "iopub.status.busy": "2026-10-14T03:30:14.673194Z", + "iopub.status.idle": "2026-10-14T03:30:14.844451Z", + "shell.execute_reply": "2026-10-14T03:30:14.843361Z" + }, + "papermill": { + "duration": 0.176015, + "end_time": "2026-10-14T03:30:14.845021+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:14.669006+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Orbites en taille 3 : (depart, pas 1, pas 2, pas 3)
\n", + "
 [((false, false, false), (false, false, false), (false, false, false), false, false, false),\n",
+       " ((true, false, false), (true, true, true), (true, true, true), true, true, true),\n",
+       " ((false, true, false), (true, true, true), (true, true, true), true, true, true),\n",
+       " ((true, true, false), (false, false, false), (false, false, false), false, false, false),\n",
+       " ((false, false, true), (true, true, true), (true, true, true), true, true, true),\n",
+       " ((true, false, true), (false, false, false), (false, false, false), false, false, false),\n",
+       " ((false, true, true), (false, false, false), (false, false, false), false, false, false),\n",
+       " ((true, true, true), (true, true, true), (true, true, true), true, true, true)]
\n", + "
  (bits3 s,
\n", + "
   bits3 (broadcast s),
\n", + "
   bits3 (broadcast (broadcast s)),
\n", + "
   bits3 (broadcast (broadcast (broadcast s)))))
\n", + "
--% env 7
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Orbites en taille 3 : (depart, pas 1, pas 2, pas 3)\\n#eval (allStates 3).map (fun s =>\\n (bits3 s,\\n bits3 (broadcast s),\\n bits3 (broadcast (broadcast s)),\\n bits3 (broadcast (broadcast (broadcast s)))))\", \"env\": 6}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 5},\r\n", + " \"data\":\r\n", + " \"[((false, false, false), (false, false, false), (false, false, false), false, false, false),\\n ((true, false, false), (true, true, true), (true, true, true), true, true, true),\\n ((false, true, false), (true, true, true), (true, true, true), true, true, true),\\n ((true, true, false), (false, false, false), (false, false, false), false, false, false),\\n ((false, false, true), (true, true, true), (true, true, true), true, true, true),\\n ((true, false, true), (false, false, false), (false, false, false), false, false, false),\\n ((false, true, true), (false, false, false), (false, false, false), false, false, false),\\n ((true, true, true), (true, true, true), (true, true, true), true, true, true)]\"}],\r\n", + " \"env\": 7}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Orbites en taille 3 : (depart, pas 1, pas 2, pas 3)\n", + "#eval (allStates 3).map (fun s =>\n", + "─────▶ [((false, false, false), (false, false, false), (false, false, false), false, false, false),\n", + " ((true, false, false), (true, true, true), (true, true, true), true, true, true),\n", + " ((false, true, false), (true, true, true), (true, true, true), true, true, true),\n", + " ((true, true, false), (false, false, false), (false, false, false), false, false, false),\n", + " ((false, false, true), (true, true, true), (true, true, true), true, true, true),\n", + " ((true, false, true), (false, false, false), (false, false, false), false, false, false),\n", + " ((false, true, true), (false, false, false), (false, false, false), false, false, false),\n", + " ((true, true, true), (true, true, true), (true, true, true), true, true, true)]\n", + " (bits3 s,\n", + " bits3 (broadcast s),\n", + " bits3 (broadcast (broadcast s)),\n", + " bits3 (broadcast (broadcast (broadcast s)))))\n", + "--% env 7\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Orbites en taille 3 : (depart, pas 1, pas 2, pas 3)\\n#eval (allStates 3).map (fun s =>\\n (bits3 s,\\n bits3 (broadcast s),\\n bits3 (broadcast (broadcast s)),\\n bits3 (broadcast (broadcast (broadcast s)))))\", \"env\": 6}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 5},\r\n", + " \"data\":\r\n", + " \"[((false, false, false), (false, false, false), (false, false, false), false, false, false),\\n ((true, false, false), (true, true, true), (true, true, true), true, true, true),\\n ((false, true, false), (true, true, true), (true, true, true), true, true, true),\\n ((true, true, false), (false, false, false), (false, false, false), false, false, false),\\n ((false, false, true), (true, true, true), (true, true, true), true, true, true),\\n ((true, false, true), (false, false, false), (false, false, false), false, false, false),\\n ((false, true, true), (false, false, false), (false, false, false), false, false, false),\\n ((true, true, true), (true, true, true), (true, true, true), true, true, true)]\"}],\r\n", + " \"env\": 7}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Orbites en taille 3 : (depart, pas 1, pas 2, pas 3)\n", + "#eval (allStates 3).map (fun s =>\n", + " (bits3 s,\n", + " bits3 (broadcast s),\n", + " bits3 (broadcast (broadcast s)),\n", + " bits3 (broadcast (broadcast (broadcast s)))))" + ] + }, + { + "cell_type": "markdown", + "id": "6e7d9d41", + "metadata": { + "papermill": { + "duration": 0.002723, + "end_time": "2026-10-14T03:30:14.850683+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:14.847960+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "Lecture de la table (taille 3, impaire) : **deux** points fixes cette fois.\n", + "\n", + "- Les états de parité paire (0 ou 2 bits vrais) convergent vers `(false, false, false)`.\n", + "- Les états de parité impaire (1 ou 3 bits vrais) convergent vers `(true, true, true)` —\n", + " qui est lui-même un point fixe : en taille impaire, la parité de l'état tout-vrai vaut\n", + " `true`, l'état se diffuse à lui-même.\n", + "- Colonnes 3 = 4 partout, convergence en au plus deux pas : le théorème C tient pour\n", + " les deux tailles." + ] + }, + { + "cell_type": "markdown", + "id": "a034a3d5", + "metadata": { + "papermill": { + "duration": 0.00311, + "end_time": "2026-10-14T03:30:14.856593+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:14.853483+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 4. Théorème C — la dynamique est triviale" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "id": "b7515ac2", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:14.863529Z", + "iopub.status.busy": "2026-10-14T03:30:14.863359Z", + "iopub.status.idle": "2026-10-14T03:30:15.018195Z", + "shell.execute_reply": "2026-10-14T03:30:15.017052Z" + }, + "papermill": { + "duration": 0.159273, + "end_time": "2026-10-14T03:30:15.018844+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:14.859571+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Theoreme C et son alias figé
\n", + "
 @broadcast_two_cycle : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)
\n", + "
 'IIT.broadcast_two_cycle' depends on axioms: [propext, Quot.sound]
\n", + "
 @broadcast_trivial_dynamics : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)
\n", + "
 'IIT.broadcast_trivial_dynamics' depends on axioms: [propext, Quot.sound]
\n", + "
--% env 8
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Theoreme C et son alias fig\\u00e9\\n#check @broadcast_two_cycle\\n#print axioms broadcast_two_cycle\\n#check @broadcast_trivial_dynamics\\n#print axioms broadcast_trivial_dynamics\", \"env\": 7}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@broadcast_two_cycle : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'IIT.broadcast_two_cycle' depends on axioms: [propext, Quot.sound]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@broadcast_trivial_dynamics : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'IIT.broadcast_trivial_dynamics' depends on axioms: [propext, Quot.sound]\"}],\r\n", + " \"env\": 8}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Theoreme C et son alias figé\n", + "#check @broadcast_two_cycle\n", + "──────▶ @broadcast_two_cycle : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)\n", + "#print axioms broadcast_two_cycle\n", + "──────▶ 'IIT.broadcast_two_cycle' depends on axioms: [propext, Quot.sound]\n", + "#check @broadcast_trivial_dynamics\n", + "──────▶ @broadcast_trivial_dynamics : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)\n", + "#print axioms broadcast_trivial_dynamics\n", + "──────▶ 'IIT.broadcast_trivial_dynamics' depends on axioms: [propext, Quot.sound]\n", + "--% env 8\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Theoreme C et son alias fig\\u00e9\\n#check @broadcast_two_cycle\\n#print axioms broadcast_two_cycle\\n#check @broadcast_trivial_dynamics\\n#print axioms broadcast_trivial_dynamics\", \"env\": 7}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@broadcast_two_cycle : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'IIT.broadcast_two_cycle' depends on axioms: [propext, Quot.sound]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@broadcast_trivial_dynamics : ∀ {n : Nat} (s : State n), broadcast (broadcast (broadcast s)) = broadcast (broadcast s)\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'IIT.broadcast_trivial_dynamics' depends on axioms: [propext, Quot.sound]\"}],\r\n", + " \"env\": 8}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Theoreme C et son alias figé\n", + "#check @broadcast_two_cycle\n", + "#print axioms broadcast_two_cycle\n", + "#check @broadcast_trivial_dynamics\n", + "#print axioms broadcast_trivial_dynamics" + ] + }, + { + "cell_type": "markdown", + "id": "82320532", + "metadata": { + "papermill": { + "duration": 0.003127, + "end_time": "2026-10-14T03:30:15.025380+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.022253+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "L'énoncé : `broadcast (broadcast (broadcast s)) = broadcast (broadcast s)` pour tout état\n", + "`s`. Toute orbite atteint un point fixe en deux pas — la **dynamique est triviale** :\n", + "l'information globale est préservée (la parité), mais il ne se « passe » plus rien.\n", + "L'alias `broadcast_trivial_dynamics` porte le nom figé par l'issue #18599 : le lake garantit\n", + "cet énoncé sous ce nom, quelle que soit l'évolution des preuves internes." + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "id": "be10a2df", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:15.033547Z", + "iopub.status.busy": "2026-10-14T03:30:15.033352Z", + "iopub.status.idle": "2026-10-14T03:30:15.185643Z", + "shell.execute_reply": "2026-10-14T03:30:15.184689Z" + }, + "papermill": { + "duration": 0.157382, + "end_time": "2026-10-14T03:30:15.186151+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.028769+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Temoin concret : le theorique C mesure sur un etat
\n", + "
 true
\n", + "
--% env 9
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Temoin concret : le theorique C mesure sur un etat\\n#eval bits3 (broadcast (broadcast (broadcast sOneHot))) == bits3 (broadcast (broadcast sOneHot))\", \"env\": 8}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 5},\r\n", + " \"data\": \"true\"}],\r\n", + " \"env\": 9}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Temoin concret : le theorique C mesure sur un etat\n", + "#eval bits3 (broadcast (broadcast (broadcast sOneHot))) == bits3 (broadcast (broadcast sOneHot))\n", + "─────▶ true\n", + "--% env 9\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Temoin concret : le theorique C mesure sur un etat\\n#eval bits3 (broadcast (broadcast (broadcast sOneHot))) == bits3 (broadcast (broadcast sOneHot))\", \"env\": 8}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 5},\r\n", + " \"data\": \"true\"}],\r\n", + " \"env\": 9}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Temoin concret : le theorique C mesure sur un etat\n", + "#eval bits3 (broadcast (broadcast (broadcast sOneHot))) == bits3 (broadcast (broadcast sOneHot))" + ] + }, + { + "cell_type": "markdown", + "id": "821669f2", + "metadata": { + "papermill": { + "duration": 0.002855, + "end_time": "2026-10-14T03:30:15.192222+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.189367+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "Le témoin rend `true` : sur l'état témoin, la troisième itération est byte-identique à la\n", + "deuxième. La mesure de l'oracle (colonnes 3 = 4) et le théorème C disent la même chose —\n", + "l'un pour `2^n` états mesurés, l'autre pour tous les états de toutes les tailles." + ] + }, + { + "cell_type": "markdown", + "id": "8a08347a", + "metadata": { + "papermill": { + "duration": 0.005974, + "end_time": "2026-10-14T03:30:15.201069+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.195095+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 5. Théorème B — le broadcast est intégré pour toute coupe" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "id": "2660c135", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:15.208704Z", + "iopub.status.busy": "2026-10-14T03:30:15.208529Z", + "iopub.status.idle": "2026-10-14T03:30:15.356537Z", + "shell.execute_reply": "2026-10-14T03:30:15.355391Z" + }, + "papermill": { + "duration": 0.153026, + "end_time": "2026-10-14T03:30:15.357395+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.204369+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Theoreme B : l'objet qui a mordu IIT, en theoreme
\n", + "
 @broadcast_integrated : ∀ {n : Nat}, integrated broadcast
\n", + "
 'IIT.broadcast_integrated' depends on axioms: [propext]
\n", + "
 @integrated : {n : Nat} → System n → Prop
\n", + "
--% env 10
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Theoreme B : l'objet qui a mordu IIT, en theoreme\\n#check @broadcast_integrated\\n#print axioms broadcast_integrated\\n#check @integrated\", \"env\": 9}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\": \"@broadcast_integrated : ∀ {n : Nat}, integrated broadcast\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\": \"'IIT.broadcast_integrated' depends on axioms: [propext]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 6},\r\n", + " \"data\": \"@integrated : {n : Nat} → System n → Prop\"}],\r\n", + " \"env\": 10}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Theoreme B : l'objet qui a mordu IIT, en theoreme\n", + "#check @broadcast_integrated\n", + "──────▶ @broadcast_integrated : ∀ {n : Nat}, integrated broadcast\n", + "#print axioms broadcast_integrated\n", + "──────▶ 'IIT.broadcast_integrated' depends on axioms: [propext]\n", + "#check @integrated\n", + "──────▶ @integrated : {n : Nat} → System n → Prop\n", + "--% env 10\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Theoreme B : l'objet qui a mordu IIT, en theoreme\\n#check @broadcast_integrated\\n#print axioms broadcast_integrated\\n#check @integrated\", \"env\": 9}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\": \"@broadcast_integrated : ∀ {n : Nat}, integrated broadcast\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\": \"'IIT.broadcast_integrated' depends on axioms: [propext]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 4, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 4, \"column\": 6},\r\n", + " \"data\": \"@integrated : {n : Nat} → System n → Prop\"}],\r\n", + " \"env\": 10}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Theoreme B : l'objet qui a mordu IIT, en theoreme\n", + "#check @broadcast_integrated\n", + "#print axioms broadcast_integrated\n", + "#check @integrated" + ] + }, + { + "cell_type": "markdown", + "id": "1754e174", + "metadata": { + "papermill": { + "duration": 0.003086, + "end_time": "2026-10-14T03:30:15.363974+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.360888+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "Lecture du théorème B : pour **toute coupe non triviale** (`c.ha` et `c.hb` attestent que\n", + "les deux côtés existent), le couple de motifs — côté A diffusé *vrai* **et** côté B diffusé\n", + "*faux* — n'est **jamais réalisé ensemble**, alors que chaque motif l'est séparément.\n", + "\n", + "Autrement dit : aucune coupe ne découpe le broadcast en deux moitiés indépendantes. Le\n", + "système est **intégré au sens du proxy, universellement** — c'est exactement « l'objet qui a\n", + "mordu IIT » (l'exemple qui a fait réaliser à la communauté que le proxy d'intégration\n", + "récompensait cet objet), désormais un théorème du lake." + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "id": "baec7421", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:15.371717Z", + "iopub.status.busy": "2026-10-14T03:30:15.371551Z", + "iopub.status.idle": "2026-10-14T03:30:15.520128Z", + "shell.execute_reply": "2026-10-14T03:30:15.519335Z" + }, + "papermill": { + "duration": 0.153634, + "end_time": "2026-10-14T03:30:15.520674+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.367040+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Rappel marche 1 : le contraste A vs B
\n", + "
 @cutIndep_of_sides_independent : ∀ {n : Nat} (c : Cut n) (f : System n),\n",
+       "  (∀ (s s' : State n), (∀ (i : Fin n), c.sel i = true → s i = s' i) → ∀ (i : Fin n), c.sel i = true → f s i = f s' i) →\n",
+       "    (∀ (s s' : State n),\n",
+       "        (∀ (i : Fin n), c.sel i = false → s i = s' i) → ∀ (i : Fin n), c.sel i = false → f s i = f s' i) →\n",
+       "      cutIndep c f
\n", + "
 @product_decomposable : ∀ {n : Nat} (c : Cut n) (f : System n),\n",
+       "  (∀ (s s' : State n), (∀ (i : Fin n), c.sel i = true → s i = s' i) → ∀ (i : Fin n), c.sel i = true → f s i = f s' i) →\n",
+       "    (∀ (s s' : State n),\n",
+       "        (∀ (i : Fin n), c.sel i = false → s i = s' i) → ∀ (i : Fin n), c.sel i = false → f s i = f s' i) →\n",
+       "      decomposable f
\n", + "
--% env 11
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Rappel marche 1 : le contraste A vs B\\n#check @cutIndep_of_sides_independent\\n#check @product_decomposable\", \"env\": 10}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@cutIndep_of_sides_independent : ∀ {n : Nat} (c : Cut n) (f : System n),\\n (∀ (s s' : State n), (∀ (i : Fin n), c.sel i = true → s i = s' i) → ∀ (i : Fin n), c.sel i = true → f s i = f s' i) →\\n (∀ (s s' : State n),\\n (∀ (i : Fin n), c.sel i = false → s i = s' i) → ∀ (i : Fin n), c.sel i = false → f s i = f s' i) →\\n cutIndep c f\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@product_decomposable : ∀ {n : Nat} (c : Cut n) (f : System n),\\n (∀ (s s' : State n), (∀ (i : Fin n), c.sel i = true → s i = s' i) → ∀ (i : Fin n), c.sel i = true → f s i = f s' i) →\\n (∀ (s s' : State n),\\n (∀ (i : Fin n), c.sel i = false → s i = s' i) → ∀ (i : Fin n), c.sel i = false → f s i = f s' i) →\\n decomposable f\"}],\r\n", + " \"env\": 11}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Rappel marche 1 : le contraste A vs B\n", + "#check @cutIndep_of_sides_independent\n", + "──────▶ @cutIndep_of_sides_independent : ∀ {n : Nat} (c : Cut n) (f : System n),\n", + " (∀ (s s' : State n), (∀ (i : Fin n), c.sel i = true → s i = s' i) → ∀ (i : Fin n), c.sel i = true → f s i = f s' i) →\n", + " (∀ (s s' : State n),\n", + " (∀ (i : Fin n), c.sel i = false → s i = s' i) → ∀ (i : Fin n), c.sel i = false → f s i = f s' i) →\n", + " cutIndep c f\n", + "#check @product_decomposable\n", + "──────▶ @product_decomposable : ∀ {n : Nat} (c : Cut n) (f : System n),\n", + " (∀ (s s' : State n), (∀ (i : Fin n), c.sel i = true → s i = s' i) → ∀ (i : Fin n), c.sel i = true → f s i = f s' i) →\n", + " (∀ (s s' : State n),\n", + " (∀ (i : Fin n), c.sel i = false → s i = s' i) → ∀ (i : Fin n), c.sel i = false → f s i = f s' i) →\n", + " decomposable f\n", + "--% env 11\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Rappel marche 1 : le contraste A vs B\\n#check @cutIndep_of_sides_independent\\n#check @product_decomposable\", \"env\": 10}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@cutIndep_of_sides_independent : ∀ {n : Nat} (c : Cut n) (f : System n),\\n (∀ (s s' : State n), (∀ (i : Fin n), c.sel i = true → s i = s' i) → ∀ (i : Fin n), c.sel i = true → f s i = f s' i) →\\n (∀ (s s' : State n),\\n (∀ (i : Fin n), c.sel i = false → s i = s' i) → ∀ (i : Fin n), c.sel i = false → f s i = f s' i) →\\n cutIndep c f\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"@product_decomposable : ∀ {n : Nat} (c : Cut n) (f : System n),\\n (∀ (s s' : State n), (∀ (i : Fin n), c.sel i = true → s i = s' i) → ∀ (i : Fin n), c.sel i = true → f s i = f s' i) →\\n (∀ (s s' : State n),\\n (∀ (i : Fin n), c.sel i = false → s i = s' i) → ∀ (i : Fin n), c.sel i = false → f s i = f s' i) →\\n decomposable f\"}],\r\n", + " \"env\": 11}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Rappel marche 1 : le contraste A vs B\n", + "#check @cutIndep_of_sides_independent\n", + "#check @product_decomposable" + ] + }, + { + "cell_type": "markdown", + "id": "c05eb711", + "metadata": { + "papermill": { + "duration": 0.00316, + "end_time": "2026-10-14T03:30:15.527381+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.524221+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "Le contraste des deux théorèmes, dans le même vocabulaire :\n", + "\n", + "| | système | verdict |\n", + "|---|---|---|\n", + "| **Théorème A** (`cutIndep_of_sides_independent`) | l'identité | **décomposable** : chaque moitié vit sa vie |\n", + "| **Théorème B** (`broadcast_integrated`) | le broadcast | **intégré pour toute coupe** : aucune moitié ne vit sa vie |\n", + "\n", + "L'identité — le système le plus « riche » en comportement local — est décomposable ; le\n", + "broadcast — qui ne fait que diffuser un bit — est universellement intégré. Le proxy inverse\n", + "l'intuition." + ] + }, + { + "cell_type": "markdown", + "id": "161e14fb", + "metadata": { + "papermill": { + "duration": 0.002953, + "end_time": "2026-10-14T03:30:15.533586+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.530633+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 6. La critique d'Aaronson : B et C ensemble\n", + "\n", + "Le couple est la critique :\n", + "\n", + "- **B** : le broadcast est intégré pour toute coupe — information globalement liée ;\n", + "- **C** : sa dynamique est triviale — point fixe en deux pas, plus rien ne se passe.\n", + "\n", + "Si un proxy d'intégration attache une valeur maximale à un objet dont le comportement se\n", + "réduit à « stabiliser la parité », il ne mesure pas le *calcul* — il mesure un artefact de\n", + "la définition. C'est le contenu formel de la critique d'Aaronson contre les théories\n", + "de l'information intégrée, et c'est la raison pour laquelle le lake livre les deux\n", + "théorèmes **sous le même toit** : l'un sans l'autre ne prouve rien." + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "id": "874f5867", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:15.541117Z", + "iopub.status.busy": "2026-10-14T03:30:15.540949Z", + "iopub.status.idle": "2026-10-14T03:30:15.684659Z", + "shell.execute_reply": "2026-10-14T03:30:15.683833Z" + }, + "papermill": { + "duration": 0.148645, + "end_time": "2026-10-14T03:30:15.685357+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.536712+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Les deux theoremes ne dependent que des axiomes standard
\n", + "
 'IIT.broadcast_integrated' depends on axioms: [propext]
\n", + "
 'IIT.broadcast_two_cycle' depends on axioms: [propext, Quot.sound]
\n", + "
--% env 12
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Les deux theoremes ne dependent que des axiomes standard\\n#print axioms broadcast_integrated\\n#print axioms broadcast_two_cycle\", \"env\": 11}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\": \"'IIT.broadcast_integrated' depends on axioms: [propext]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'IIT.broadcast_two_cycle' depends on axioms: [propext, Quot.sound]\"}],\r\n", + " \"env\": 12}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Les deux theoremes ne dependent que des axiomes standard\n", + "#print axioms broadcast_integrated\n", + "──────▶ 'IIT.broadcast_integrated' depends on axioms: [propext]\n", + "#print axioms broadcast_two_cycle\n", + "──────▶ 'IIT.broadcast_two_cycle' depends on axioms: [propext, Quot.sound]\n", + "--% env 12\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Les deux theoremes ne dependent que des axiomes standard\\n#print axioms broadcast_integrated\\n#print axioms broadcast_two_cycle\", \"env\": 11}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 2, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 2, \"column\": 6},\r\n", + " \"data\": \"'IIT.broadcast_integrated' depends on axioms: [propext]\"},\r\n", + " {\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 3, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 3, \"column\": 6},\r\n", + " \"data\":\r\n", + " \"'IIT.broadcast_two_cycle' depends on axioms: [propext, Quot.sound]\"}],\r\n", + " \"env\": 12}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Les deux theoremes ne dependent que des axiomes standard\n", + "#print axioms broadcast_integrated\n", + "#print axioms broadcast_two_cycle" + ] + }, + { + "cell_type": "markdown", + "id": "7db197ca", + "metadata": { + "papermill": { + "duration": 0.003109, + "end_time": "2026-10-14T03:30:15.691803+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.688694+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "Mesure des dépendances : le théorème B ne dépend que de `propext` — même pas de\n", + "l'extensionnalité des fonctions ; le théorème C ajoute `Quot.sound` (qui porte `funext`,\n", + "utilisée par sa conclusion point à point). Aucune des deux preuves ne repose sur un axiome\n", + "ajouté ni sur un `sorry` : le couple B et C est aussi fort que le langage le permet." + ] + }, + { + "cell_type": "markdown", + "id": "519fd22d", + "metadata": { + "papermill": { + "duration": 0.003102, + "end_time": "2026-10-14T03:30:15.698167+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.695065+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 7. Exercices\n", + "\n", + "Trois exercices, du calcul à la prédiction d'orbite. Les cellules s'exécutent telles\n", + "quelles (rien à casser) : compléter le TODO puis re-exécuter." + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "id": "5eecaf0e", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:15.705327Z", + "iopub.status.busy": "2026-10-14T03:30:15.705158Z", + "iopub.status.idle": "2026-10-14T03:30:15.861582Z", + "shell.execute_reply": "2026-10-14T03:30:15.860175Z" + }, + "papermill": { + "duration": 0.161353, + "end_time": "2026-10-14T03:30:15.862601+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.701248+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Exercice 1 : la parite a la main
\n", + "
-- TODO etudiant : predire (sans #eval parity) la parite de l'etat ci-dessous,
\n", + "
-- en comptant les bits vrais, puis verifier en decommentant la ligne de controle.
\n", + "
-- Etape 1 : ecrire la valeur attendue (true ou false) en commentaire
\n", + "
-- Etape 2 : decommenter et executer la ligne de controle
\n", + "
def sExo1 : State 3 := fun j => decide (j.val = 2)
\n", + "
 \"Exercice 1 a completer\"
\n", + "
-- #eval parity 3 sExo1
\n", + "
--% env 13
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Exercice 1 : la parite a la main\\n-- TODO etudiant : predire (sans #eval parity) la parite de l'etat ci-dessous,\\n-- en comptant les bits vrais, puis verifier en decommentant la ligne de controle.\\n-- Etape 1 : ecrire la valeur attendue (true ou false) en commentaire\\n-- Etape 2 : decommenter et executer la ligne de controle\\ndef sExo1 : State 3 := fun j => decide (j.val = 2)\\n#eval \\\"Exercice 1 a completer\\\"\\n-- #eval parity 3 sExo1\", \"env\": 12}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 5},\r\n", + " \"data\": \"\\\"Exercice 1 a completer\\\"\"}],\r\n", + " \"env\": 13}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Exercice 1 : la parite a la main\n", + "-- TODO etudiant : predire (sans #eval parity) la parite de l'etat ci-dessous,\n", + "-- en comptant les bits vrais, puis verifier en decommentant la ligne de controle.\n", + "-- Etape 1 : ecrire la valeur attendue (true ou false) en commentaire\n", + "-- Etape 2 : decommenter et executer la ligne de controle\n", + "def sExo1 : State 3 := fun j => decide (j.val = 2)\n", + "#eval \"Exercice 1 a completer\"\n", + "─────▶ \"Exercice 1 a completer\"\n", + "-- #eval parity 3 sExo1\n", + "--% env 13\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Exercice 1 : la parite a la main\\n-- TODO etudiant : predire (sans #eval parity) la parite de l'etat ci-dessous,\\n-- en comptant les bits vrais, puis verifier en decommentant la ligne de controle.\\n-- Etape 1 : ecrire la valeur attendue (true ou false) en commentaire\\n-- Etape 2 : decommenter et executer la ligne de controle\\ndef sExo1 : State 3 := fun j => decide (j.val = 2)\\n#eval \\\"Exercice 1 a completer\\\"\\n-- #eval parity 3 sExo1\", \"env\": 12}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 7, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 7, \"column\": 5},\r\n", + " \"data\": \"\\\"Exercice 1 a completer\\\"\"}],\r\n", + " \"env\": 13}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Exercice 1 : la parite a la main\n", + "-- TODO etudiant : predire (sans #eval parity) la parite de l'etat ci-dessous,\n", + "-- en comptant les bits vrais, puis verifier en decommentant la ligne de controle.\n", + "-- Etape 1 : ecrire la valeur attendue (true ou false) en commentaire\n", + "-- Etape 2 : decommenter et executer la ligne de controle\n", + "def sExo1 : State 3 := fun j => decide (j.val = 2)\n", + "#eval \"Exercice 1 a completer\"\n", + "-- #eval parity 3 sExo1" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "id": "f0640f4d", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:15.871349Z", + "iopub.status.busy": "2026-10-14T03:30:15.871174Z", + "iopub.status.idle": "2026-10-14T03:30:16.018692Z", + "shell.execute_reply": "2026-10-14T03:30:16.017656Z" + }, + "papermill": { + "duration": 0.153102, + "end_time": "2026-10-14T03:30:16.019604+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:15.866502+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Exercice 2 : la taille gouverne le point fixe
\n", + "
-- TODO etudiant : d'apres le lemme parity_const (et la mesure en taille 4 et 5),
\n", + "
-- predire si l'etat tout-vrai de taille 6 est un point fixe du broadcast.
\n", + "
-- Repondre en commentaire : point fixe ou non, et pourquoi (le role de 6 % 2).
\n", + "
 \"Exercice 2 a completer\"
\n", + "
\n", + "
--% env 14
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Exercice 2 : la taille gouverne le point fixe\\n-- TODO etudiant : d'apres le lemme parity_const (et la mesure en taille 4 et 5),\\n-- predire si l'etat tout-vrai de taille 6 est un point fixe du broadcast.\\n-- Repondre en commentaire : point fixe ou non, et pourquoi (le role de 6 % 2).\\n#eval \\\"Exercice 2 a completer\\\"\\n\", \"env\": 13}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 5},\r\n", + " \"data\": \"\\\"Exercice 2 a completer\\\"\"}],\r\n", + " \"env\": 14}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Exercice 2 : la taille gouverne le point fixe\n", + "-- TODO etudiant : d'apres le lemme parity_const (et la mesure en taille 4 et 5),\n", + "-- predire si l'etat tout-vrai de taille 6 est un point fixe du broadcast.\n", + "-- Repondre en commentaire : point fixe ou non, et pourquoi (le role de 6 % 2).\n", + "#eval \"Exercice 2 a completer\"\n", + "─────▶ \"Exercice 2 a completer\"\n", + "\n", + "--% env 14\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Exercice 2 : la taille gouverne le point fixe\\n-- TODO etudiant : d'apres le lemme parity_const (et la mesure en taille 4 et 5),\\n-- predire si l'etat tout-vrai de taille 6 est un point fixe du broadcast.\\n-- Repondre en commentaire : point fixe ou non, et pourquoi (le role de 6 % 2).\\n#eval \\\"Exercice 2 a completer\\\"\\n\", \"env\": 13}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 5, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 5, \"column\": 5},\r\n", + " \"data\": \"\\\"Exercice 2 a completer\\\"\"}],\r\n", + " \"env\": 14}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Exercice 2 : la taille gouverne le point fixe\n", + "-- TODO etudiant : d'apres le lemme parity_const (et la mesure en taille 4 et 5),\n", + "-- predire si l'etat tout-vrai de taille 6 est un point fixe du broadcast.\n", + "-- Repondre en commentaire : point fixe ou non, et pourquoi (le role de 6 % 2).\n", + "#eval \"Exercice 2 a completer\"\n" + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "id": "4f791290", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-14T03:30:16.028691Z", + "iopub.status.busy": "2026-10-14T03:30:16.028521Z", + "iopub.status.idle": "2026-10-14T03:30:16.187145Z", + "shell.execute_reply": "2026-10-14T03:30:16.186149Z" + }, + "papermill": { + "duration": 0.16455, + "end_time": "2026-10-14T03:30:16.187855+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:16.023305+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
\n", + " 
-- Exercice 3 : l'orbite d'un etat donne
\n", + "
-- TODO etudiant : pour n = 2, decrire l'orbite complete de l'etat (true, false) :
\n", + "
-- Etape 1 : donner les etats successifs (pas 1, pas 2, pas 3)
\n", + "
-- Etape 2 : donner le point fixe atteint et le nombre de pas
\n", + "
-- Etape 3 : verifier avec l'oracle (reutiliser la table de la section 3)
\n", + "
 \"Exercice 3 a completer\"
\n", + "
\n", + "
--% env 15
\n", + "
\n", + "
\n", + " Raw input\n", + " {\"cmd\": \"-- Exercice 3 : l'orbite d'un etat donne\\n-- TODO etudiant : pour n = 2, decrire l'orbite complete de l'etat (true, false) :\\n-- Etape 1 : donner les etats successifs (pas 1, pas 2, pas 3)\\n-- Etape 2 : donner le point fixe atteint et le nombre de pas\\n-- Etape 3 : verifier avec l'oracle (reutiliser la table de la section 3)\\n#eval \\\"Exercice 3 a completer\\\"\\n\", \"env\": 14}\n", + "
\n", + "
\n", + " Raw output\n", + " {\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 6, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 6, \"column\": 5},\r\n", + " \"data\": \"\\\"Exercice 3 a completer\\\"\"}],\r\n", + " \"env\": 15}\n", + "
\n", + " " + ], + "text/plain": [ + "-- Exercice 3 : l'orbite d'un etat donne\n", + "-- TODO etudiant : pour n = 2, decrire l'orbite complete de l'etat (true, false) :\n", + "-- Etape 1 : donner les etats successifs (pas 1, pas 2, pas 3)\n", + "-- Etape 2 : donner le point fixe atteint et le nombre de pas\n", + "-- Etape 3 : verifier avec l'oracle (reutiliser la table de la section 3)\n", + "#eval \"Exercice 3 a completer\"\n", + "─────▶ \"Exercice 3 a completer\"\n", + "\n", + "--% env 15\n", + "\n", + "Raw input:\n", + "{\"cmd\": \"-- Exercice 3 : l'orbite d'un etat donne\\n-- TODO etudiant : pour n = 2, decrire l'orbite complete de l'etat (true, false) :\\n-- Etape 1 : donner les etats successifs (pas 1, pas 2, pas 3)\\n-- Etape 2 : donner le point fixe atteint et le nombre de pas\\n-- Etape 3 : verifier avec l'oracle (reutiliser la table de la section 3)\\n#eval \\\"Exercice 3 a completer\\\"\\n\", \"env\": 14}\n", + "Raw output:\n", + "{\"messages\":\r\n", + " [{\"severity\": \"info\",\r\n", + " \"pos\": {\"line\": 6, \"column\": 0},\r\n", + " \"endPos\": {\"line\": 6, \"column\": 5},\r\n", + " \"data\": \"\\\"Exercice 3 a completer\\\"\"}],\r\n", + " \"env\": 15}" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "-- Exercice 3 : l'orbite d'un etat donne\n", + "-- TODO etudiant : pour n = 2, decrire l'orbite complete de l'etat (true, false) :\n", + "-- Etape 1 : donner les etats successifs (pas 1, pas 2, pas 3)\n", + "-- Etape 2 : donner le point fixe atteint et le nombre de pas\n", + "-- Etape 3 : verifier avec l'oracle (reutiliser la table de la section 3)\n", + "#eval \"Exercice 3 a completer\"\n" + ] + }, + { + "cell_type": "markdown", + "id": "971caa1d", + "metadata": { + "papermill": { + "duration": 0.003779, + "end_time": "2026-10-14T03:30:16.195852+00:00", + "exception": false, + "start_time": "2026-10-14T03:30:16.192073+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## Conclusion — vers le capstone\n", + "\n", + "La marche 2 est en place : l'outil parité (4 lemmes), le système broadcast, le théorème B\n", + "(intégration universelle) et le théorème C (dynamique triviale), tous deux rendus par le\n", + "noyau et mesurés par l'oracle d'orbites. La marche 3 (capstone, `IIT-09`) assemblera le\n", + "contraste complet : côté Python, le proxy calculé sur des systèmes concrets ; côté Lean,\n", + "le couple B et C comme garde-fou formel — ce que le proxy récompense vs ce qu'il\n", + "devrait récompenser." + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Lean 4 (WSL)", + "language": "lean4", + "name": "lean4-wsl" + }, + "language_info": { + "codemirror_mode": "lean4", + "file_extension": ".lean", + "mimetype": "text/x-lean4", + "name": "lean4" + }, + "papermill": { + "default_parameters": {}, + "duration": 12.495455, + "end_time": "2026-10-14T03:30:16.416234+00:00", + "environment_variables": {}, + "exception": null, + "input_path": "IIT-08-Parite-et-Broadcast-Lean.ipynb", + "output_path": "IIT-08-Parite-et-Broadcast-Lean.ipynb", + "parameters": {}, + "start_time": "2026-10-14T03:30:03.920779+00:00", + "version": "2.7.0" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} \ No newline at end of file From 68a9d4ec9f062cc5e359396d7001682801bf3f1c Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 17 Oct 2026 06:00:42 +0200 Subject: [PATCH 2/4] docs(iit,#20649): suivi post-merge 20419 -- ligne 8 README IIT-08 + inventaire iit_lean cale 2 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Périmètre différé du body de la PR, dû depuis le merge de #20419 (2026-10-15) : #20419 a apporté le carnet IIT-07 et le README mais pas le bump d'inventaire (vivant sur #20645 fermée). Cette passe aligne les deux surfaces sur l'état post-marche-2 : ligne table 8, parcours, section détaillée et arbre README ; inventaire iit_lean cablé 0->2 (IIT-07 + IIT-08), suivi + #20414. Co-Authored-By: Claude Sonnet 5.5 --- MyIA.AI.Notebooks/IIT/README.md | 23 ++++++++++++++++++- .../SymbolicAI/Lean/LEAN_INVENTORY.md | 2 +- 2 files changed, 23 insertions(+), 2 deletions(-) diff --git a/MyIA.AI.Notebooks/IIT/README.md b/MyIA.AI.Notebooks/IIT/README.md index 3d7caf3eef..ed1b9fbbcc 100644 --- a/MyIA.AI.Notebooks/IIT/README.md +++ b/MyIA.AI.Notebooks/IIT/README.md @@ -35,6 +35,7 @@ Le premier notebook couvre le spectre fondamental : construction de graphes caus | 5 | [IIT-05-Lentilles-et-Dissociations-Python](IIT-05-Lentilles-et-Dissociations-Python.ipynb) | Six théories de la conscience (GWT, GNW, FEP, AST, SMT, HOT) comme mesures exécutables sur un même substrat : dissociation accès vs autoréférence, orthogonalité AST/SMT, contre-claim FEP | 60-75 min | | 6 | [IIT-06-L-Objet-qui-a-Mordu-IIT-Python](IIT-06-L-Objet-qui-a-Mordu-IIT-Python.ipynb) | L'échange Aaronson/Tononi (2014) exécuté : Vandermonde et le hack W en Φ_DM sur F_p, grille/ligne/feedforward en Φ 3.0 (PyPhi), les deux positions citées avec leurs grades | 75-90 min | | 7 | [IIT-07-Integration-Par-Coupes-Lean](IIT-07-Integration-Par-Coupes-Lean.ipynb) | Marche 1 de l'escalier Lean du lake `iit_lean` : coupe et motifs (`projT`/`projF`), verdict relationnel `cutIndep`/`decomposable`/`integrated`, `product_decomposable` instancié sur un système concret, la butée du broadcast | 45-60 min | +| 8 | [IIT-08-Parite-et-Broadcast-Lean](IIT-08-Parite-et-Broadcast-Lean.ipynb) | Marche 2 de l'escalier Lean du lake `iit_lean` : l'outil `parity`, le système `broadcast`, oracle d'orbites par énumération (point fixe en au plus deux pas), théorème B (`broadcast_integrated`) et théorème C (`broadcast_two_cycle`) — le couple qui a mordu IIT | 45-60 min | ## Parcours recommandés @@ -58,6 +59,9 @@ Notebook 6 (L'objet qui a mordu IIT) | v Notebook 7 (La coupe et le verdict — Lean) + | + v +Notebook 8 (Parité et broadcast — Lean) ``` | Objectif | Parcours | @@ -70,6 +74,7 @@ Notebook 7 (La coupe et le verdict — Lean) | Focus théories rivales | Notebook 1 + Notebook 5 (six lentilles, contre-claims exécutés) | | Focus controverse fondatrice | Notebook 1 + Notebook 6 (l'objection Aaronson exécutée, la réponse assumée mesurée) | | Focus moitié formelle | Notebook 6 puis 7 (l'objection Aaronson : mesurée en Φ_DM/PyPhi, puis énoncée en Lean — première marche de l'escalier du lake `iit_lean`) | +| Focus le couple qui a mordu IIT | Notebook 7 puis 8 (la coupe et le verdict, puis le broadcast : B intégré pour toute coupe + C à dynamique triviale, l'artefact du proxy mis en équation) | ### Parcours d'apprentissage @@ -267,6 +272,21 @@ Marche 1 de l'escalier qui expose le lake [`iit_lean`](../SymbolicAI/Lean/iit_le | Grade | le proxy relationnel contre Φ (MIP, perturbation, valeur numérique) — ce que le carnet ne claim pas | | Exercices | écrire une coupe (`selPairs`), reconstruire le motif d'un côté (`motifA`), reconstruire la parité (`pariteA4`) | +### IIT-08-Parite-et-Broadcast-Lean.ipynb + +Marche 2 de l'escalier du lake [`iit_lean`](../SymbolicAI/Lean/iit_lean/README.md) (issue #20649, moitié formelle de l'objection Aaronson, Epic #16781) — kernel `lean4-wsl`, sans Mathlib. + +| Section | Contenu | +|---------|---------| +| Environnement | `import IIT.Integration`, contrat du carnet par `#check` (`parity`, `broadcast`, théorèmes B et C) | +| Outil parité | `parity : (n : Nat) → State n → Bool` par récurrence sur la taille, trois états témoins en n=3, tuples de bits pour voir les états | +| Système broadcast | `broadcast : System n` — chaque bit de l'état suivant vaut la parité de l'état courant | +| Oracle | les orbites par énumération : point fixe atteint en au plus deux pas, la troisième itération égale toujours la deuxième | +| Théorème C | `broadcast_two_cycle` — la dynamique est triviale, rendue visible par l'oracle | +| Théorème B | `broadcast_integrated` — le broadcast est intégré pour toute coupe | +| La critique | B et C sous le même toit : intégration universelle et dynamique triviale ensemble — ce qu'un proxy d'intégration récompense vs ce qu'il devrait récompenser | +| Exercices | la parité à la main (`sExo1`), le rôle de la taille dans le point fixe (`parity_const`, le rôle de 6 % 2), l'orbite complète d'un état en n=2 | + ## Théorie IIT La Théorie de l'Information Intégrée (IIT) propose une approche mathématique de la conscience : @@ -375,6 +395,7 @@ IIT/ ├── IIT-05-Lentilles-et-Dissociations-Python.ipynb # Notebook 5 : six théories de la conscience comme bancs de dissociation ├── IIT-06-L-Objet-qui-a-Mordu-IIT-Python.ipynb # Notebook 6 : l'échange Aaronson/Tononi exécuté (Φ_DM + PyPhi) ├── IIT-07-Integration-Par-Coupes-Lean.ipynb # Notebook 7 : la coupe et le verdict — lake iit_lean (Lean 4) +├── IIT-08-Parite-et-Broadcast-Lean.ipynb # Notebook 8 : parité et broadcast — théorèmes B et C, lake iit_lean (Lean 4) ├── ICT-Series/ # Extension expérimentale ICT (Epic #4588) — voir son README │ ├── ICT-0-Framing.md # Cadrage de la série ICT │ ├── ICT-0-Annexe-IntegratedComplexityTheory.md # Annexe théorique (complexité intégrée) @@ -514,7 +535,7 @@ Voir la licence du repository principal. --- -*Version 1.4.0 — Octobre 2026* +*Version 1.5.0 — Octobre 2026*