diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb index 2250068f2c..44691e7410 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb @@ -25,7 +25,7 @@ "\n", "| Notebook précédent | Notebook suivant |\n", "|---|---|\n", - "| [ANALYSE-03 - PFR Entropy Method](ANALYSE-03-PFR-Lean.ipynb) | [Lean-21 - MIMO Detection Flips](../Lean-21-MIMO-Detection-Flips.ipynb) |\n", + "| [ANALYSE-03 - PFR Entropy Method](ANALYSE-03-PFR-Lean.ipynb) | [ANALYSE-09 - Tuilage apériodique](ANALYSE-09-Tuilage-Aperiodique.ipynb) |\n", "\n", "***\n", "\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-09-Tuilage-Aperiodique.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-09-Tuilage-Aperiodique.ipynb new file mode 100644 index 0000000000..01ea777b11 --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-09-Tuilage-Aperiodique.ipynb @@ -0,0 +1,786 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "6f91e0b5", + "metadata": { + "papermill": { + "duration": 0.002612, + "end_time": "2026-10-08T22:34:55.771634", + "exception": false, + "start_time": "2026-10-08T22:34:55.769022", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "# ANALYSE-09 : Un carreau de ℤ³ qui pave sans périodicité totale\n", + "\n", + "**Série** : SymbolicAI / Lean — Digestions de résultats profonds, companion du capstone [Lean-20 — Digestions Tao](../Lean-20-Capstone-Digestions-Tao-Python.ipynb)\n", + "**Source** : famille 155 du corpus openai/math (« A counterexample to periodic tiling in dimension three », squelette Lean publié) — gisement de reconnaissance `G:\\Mon Drive\\MyIA\\IA\\Distillations\\2026-10-openai-math\\`\n", + "**Lac source** : `sudoku_lean` (la sémantique exact-cover / pavage discret du dépôt, `MyIA.AI.Notebooks/Sudoku/sudoku_lean/`)\n", + "**Kernel** : `python3` — le carnet illustre les définitions et mesure des cas jouets ; l'énoncé formel reste celui du corpus\n", + "\n", + "## Navigation\n", + "\n", + "| Notebook précédent | Notebook suivant |\n", + "|---|---|\n", + "| [ANALYSE-04 - PFR Primitives](ANALYSE-04-PFR-Primitives-Python.ipynb) | [Version anglaise](ANALYSE-09-Tuilage-Aperiodique_en.ipynb) |\n", + "\n", + "***\n", + "\n", + "## Pourquoi ce carnet\n", + "\n", + "La conjecture du pavage périodique dit, grossièrement : *si une forme pave l'espace, elle le pave périodiquement*. Elle est vraie en dimension 1, vraie pour une tuile en dimension 2 (sur ℤ²), et **fausse à partir de la dimension 3** : la famille 155 du corpus openai/math exhibe un **carreau unique** — une partie finie T ⊂ ℤ³ — qui pave ℤ³ par translations mais dont **aucun pavage n'est totalement périodique**.\n", + "\n", + "C'est le contre-exemple dans la **plus petite dimension possible** pour un carreau unique. L'épaississement en cubes unitaires transporte le même contre-exemple dans ℝ³, même en autorisant des vecteurs de translation réels arbitraires.\n", + "\n", + "> **Statut épistémique** : openai/math est une source tierce non vérifiée par nous. L'énoncé ci-dessus est celui déclaré par le corpus (squelette Lean publié pour la famille 155) ; ce carnet le **présente** et l'**illustre** sur des cas jouets mesurés — il ne re-démontre pas le théorème.\n", + "\n", + "## Ce que le carnet établit (plan)\n", + "\n", + "1. **§1** — les définitions exactes : tuile, pavage par translations, période, *périodicité totale* (rang 3) — et pourquoi « apériodique » est plus subtil que « sans aucune période ».\n", + "2. **§2** — la connexion exact-cover : paver une fenêtre finie, c'est résoudre une couverture exacte — la sémantique que le lac `sudoku_lean` formalise.\n", + "3. **§3** — le moteur (backtracking borné + mesure du rang des périodes) et quatre expériences mesurées : un témoin périodique, une tuile qui ne pave **aucune** boîte (et pourquoi c'est un théorème), une tuile à période minimale **prouvée** égale à 4, et un piège : une tuile qui **semble** apériodique sur petite fenêtre.\n", + "4. **§4** — lecture honnête : ce que les fenêtres finies peuvent et ne peuvent pas établir, avec les mesures du §3 comme preuves.\n" + ] + }, + { + "cell_type": "markdown", + "id": "9a64e407", + "metadata": { + "papermill": { + "duration": 0.002373, + "end_time": "2026-10-08T22:34:55.777340", + "exception": false, + "start_time": "2026-10-08T22:34:55.774967", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 1. Définitions — tuile, pavage, périodicité totale\n", + "\n", + "**Tuile.** Une *tuile* est une partie **finie** non vide T ⊂ ℤ³. Ses éléments sont des cellules ; on pense à un polycube connexe, mais la définition n'exige pas la connexité.\n", + "\n", + "**Pavage par translations.** La tuile T *pave* ℤ³ s'il existe un ensemble de translations S ⊂ ℤ³ tel que les copies T + s (s ∈ S) recouvrent ℤ³ **exactement** : chaque cellule de ℤ³ appartient à une et une seule copie. C'est une **couverture exacte** de ℤ³ par des copies translatées de T — ni trou, ni chevauchement.\n", + "\n", + "**Période, pavage périodique.** Un vecteur v ∈ ℤ³ \\ {0} est une *période* d'un pavage si l'ensemble de ses translations est invariant par v : translater tout le pavage de v le laisse inchangé. Le **groupe des périodes** d'un pavage est un sous-groupe de ℤ³ ; il a un **rang** r ∈ {0, 1, 2, 3} (dimension du ℤ-module).\n", + "\n", + "**Périodicité totale.** Un pavage est *totalement périodique* quand r = 3 : trois périodes indépendantes. C'est la notion que le théorème 155 frappe : la tuile contre-exemple pave ℤ³, mais **aucun** de ses pavages n'atteint le rang 3.\n", + "\n", + "**Pourquoi cette nuance compte.** « Apériodique » ne veut pas dire « zéro période » : un pavage peut admettre une ou deux directions de périodes (rang 1 ou 2) et rester un contre-exemple — ce qui est interdit, c'est le rang plein. Un pavage de rang 2, par exemple, se répète dans deux directions mais jamais dans la troisième : assez pour réfuter la conjecture, pas assez pour être « sans structure ».\n" + ] + }, + { + "cell_type": "markdown", + "id": "62457216", + "metadata": { + "papermill": { + "duration": 0.004423, + "end_time": "2026-10-08T22:34:55.784903", + "exception": false, + "start_time": "2026-10-08T22:34:55.780480", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 2. La connexion exact-cover — ce que `sudoku_lean` formalise\n", + "\n", + "Sur une **fenêtre finie** W (un bloc N₁×N₂×N₃ de ℤ³), paver W par des copies de T est un problème de couverture exacte : chaque cellule de W doit être couverte **exactement une fois**, chaque placement de tuile est un « choix », et les choix doivent être deux à deux non conflictuants.\n", + "\n", + "C'est exactement la sémantique du lac `sudoku_lean` du dépôt : `ExactCover.IsExactCover` (`MyIA.AI.Notebooks/Sudoku/sudoku_lean/Sudoku/ExactCover.lean`) définit la couverture exacte d'un ensemble de *scopes* par une sélection, et le Sudoku y est l'instance canonique. Le Sudoku est un pavage : chaque case reçoit exactement un chiffre, chaque contrainte est couverte exactement une fois. Notre fenêtre de pavage est une autre instance de la même sémantique — cells × placements au lieu de cells × valeurs.\n", + "\n", + "> **Copie pédagogique déclarée** (règle organ-first du dépôt) : le solveur borné de ce carnet est une réimplémentation locale **déclarée** — backtracking pur Python, lisible — de la sémantique exact-cover. L'organe natif (`sudoku_lean`) est un lac de preuves Lean, pas une librairie Python consommable ; l'invocation réelle n'est pas disponible côté Python, et le but ici est de montrer la mécanique, pas de la prouver. Réponses aux 5 questions : la série Sudoku possède la sémantique (1) ; son module n'est pas invocable depuis Python (2) ; l'exporter exigerait un port sans valeur pédagogique ici (3) ; le témoin négatif de l'organe est la preuve formelle `mem_toSelection_iff`, hors de portée d'un carnet (4) ; la vérification indépendante est le re-jeu multi-fenêtres du §3, dont les rangs mesurés confrontent les contraintes prouvées à la main (5).\n" + ] + }, + { + "cell_type": "markdown", + "id": "3acb0f1e", + "metadata": { + "papermill": { + "duration": 0.002787, + "end_time": "2026-10-08T22:34:55.791388", + "exception": false, + "start_time": "2026-10-08T22:34:55.788601", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 3. Le moteur et les quatre expériences\n", + "\n", + "Le moteur a deux organes, tous deux déterministes :\n", + "\n", + "- `place_tiles(window, tile)` — backtracking exact-cover **borné** : la première cellule libre (ordre lexicographique) force le choix de l'ancre qui la couvre, on descend, on revient. Le compteur de nœuds mesure le coût combinatoire.\n", + "- `period_rank(placement, window)` — pour le pavage obtenu, teste tous les vecteurs de période v dans la boîte |vᵢ| ≤ ⌊Nᵢ/2⌋ (la **demi-fenêtre**) et retourne le rang sur ℤ du groupe qu'ils engendrent (élimination gaussienne exacte sur les rationnels).\n", + "\n", + "La demi-fenêtre est la clef de lecture de tout le §3 : **toute période plus longue que la demi-fenêtre est invisible**. C'est un plafond de mesure, pas une propriété de la tuile — les expériences A et B2 le montrent chacun à leur façon.\n", + "\n", + "Quatre expériences :\n", + "\n", + "| # | Tuile | Ce qu'on mesure | Contrainte prouvable à la main |\n", + "|---|---|---|---|\n", + "| A | domino 1×1×2 | le témoin périodique : rang 3 attendu | pavage évident, périodes 1 ou 2 |\n", + "| B0 | prisme L×{0} | la tuile ne pave **aucune** boîte alignée | théorème : coin forcé, induction, case (1,1) morte |\n", + "| B1 | domino troué {(0,0,0),(2,0,0)} | rang 2 puis rang 3 quand la fenêtre grandit | période x minimale **exactement 4** dans tout pavage |\n", + "| B2 | cube dilaté {0,2}³ | rang 0 puis rang 3 | pavage de ℤ³ **unique**, périodes exactement 4ℤ³ |\n" + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "4ec88ea1", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-08T22:34:55.797744Z", + "iopub.status.busy": "2026-10-08T22:34:55.797486Z", + "iopub.status.idle": "2026-10-08T22:34:55.885852Z", + "shell.execute_reply": "2026-10-08T22:34:55.884597Z" + }, + "papermill": { + "duration": 0.093331, + "end_time": "2026-10-08T22:34:55.887334", + "exception": false, + "start_time": "2026-10-08T22:34:55.794003", + "status": "completed" + }, + "tags": [] + }, + "outputs": [], + "source": [ + "\"\"\"Moteur de calcul pour le notebook ANALYSE-09-Tuilage-Aperiodique (famille 155).\n", + "\n", + "Famille 155 : « contre-exemple au tuilage périodique en dimension trois » —\n", + "il existe une tuile translative finie T sous-ensemble de Z^3 qui tuile Z^3\n", + "mais n'admet AUCUN tuilage pleinement périodique (groupe de périodes de rang\n", + "3) ; des périodes partielles de rang < 3 peuvent exister. La tuile du théorème\n", + "est énorme : ce moteur fournit donc des mesures BORNÉES et HONNÊTES sur de\n", + "petites fenêtres.\n", + "\n", + "Deux organes :\n", + " * place_tiles : exact-cover par backtracking borné (translations seules,\n", + " aucune rotation), déterministe, avec compteur de noeuds ;\n", + " * period_rank : rang sur Z du groupe des vecteurs de période du tuilage\n", + " RESTREINT à la fenêtre, testés dans |v_i| <= floor(N_i/2).\n", + "\n", + "Limite pédagogique assumée (aussi dans tiling_measurements.json, champ\n", + "« limitation ») : une petite fenêtre ne peut jamais PROUVER l'apériodicité,\n", + "elle peut seulement la suggérer — une fenêtre plus grande peut révéler des\n", + "périodes jusqu'alors invisibles. La preuve du théorème vit dans la prose du\n", + "notebook, pas dans ces mesures.\n", + "\"\"\"\n", + "\n", + "from __future__ import annotations\n", + "\n", + "from fractions import Fraction\n", + "from itertools import product\n", + "from typing import Iterable, Optional\n", + "\n", + "import numpy as np\n", + "\n", + "Cell = tuple[int, int, int]\n", + "Placement = dict[Cell, Cell] # cellule -> ancre de la copie qui la couvre\n", + "\n", + "\n", + "\n", + "class _NodeBudgetExceeded(RuntimeError):\n", + " \"\"\"Budget de noeuds épuisé : instance abandonnée (ni échec ni succès).\"\"\"\n", + "\n", + "\n", + "def place_tiles(\n", + " window_shape: tuple[int, int, int],\n", + " tile_cells: Iterable[Cell],\n", + " forbidden: Optional[set[Cell]] = None,\n", + " *,\n", + " max_nodes: int = 2_000_000,\n", + ") -> tuple[Optional[Placement], int]:\n", + " \"\"\"Tente de tuiler exactement la fenêtre par copies translatées de la tuile.\n", + "\n", + " Parameters\n", + " ----------\n", + " window_shape : (N1, N2, N3) — boîte [0,N1) x [0,N2) x [0,N3).\n", + " tile_cells : décalages (x,y,z) de la tuile, relatifs à son ancre.\n", + " forbidden : cellules à laisser vides (trous), optionnel.\n", + " max_nodes : garde-fou sur le nombre de noeuds de backtracking.\n", + "\n", + " Retour\n", + " ------\n", + " (placement, nodes) où placement vaut None si aucun tuilage n'est trouvé\n", + " (ou si le budget de noeuds est épuisé). placement associe à chaque cellule\n", + " couverte l'ancre de la copie qui la couvre — support direct du test de\n", + " période de period_rank.\n", + "\n", + " Déterminisme : la première cellule libre est prise en ordre lexicographique\n", + " (ordre C : x lent, z rapide) et les ancre candidates sont essayées par\n", + " ordre croissant. Aucun aléatoire.\n", + " \"\"\"\n", + " n1, n2, n3 = (int(v) for v in window_shape)\n", + " if min(n1, n2, n3) < 1:\n", + " raise ValueError(\"window_shape doit valoir >= 1 sur chaque axe\")\n", + " cells: list[Cell] = sorted({(int(x), int(y), int(z)) for x, y, z in tile_cells})\n", + " if not cells:\n", + " raise ValueError(\"tile_cells est vide\")\n", + "\n", + " occ = np.zeros((n1, n2, n3), dtype=np.uint8) # 0 = libre, 1 = couvert, 2 = trou\n", + " if forbidden:\n", + " for (x, y, z) in forbidden:\n", + " occ[int(x), int(y), int(z)] = 2\n", + "\n", + " n_free = int((occ == 0).sum())\n", + " if n_free % len(cells) != 0:\n", + " return None, 1 # volume incompatible avec |T| : échec immédiat, décidé.\n", + "\n", + " anchors: list[Cell] = []\n", + " nodes = 0\n", + "\n", + " def candidates(c: Cell) -> list[Cell]:\n", + " \"\"\"Ancres valides couvrant la cellule c, triées (déterminisme).\"\"\"\n", + " out: list[Cell] = []\n", + " for t in cells:\n", + " a: Cell = (c[0] - t[0], c[1] - t[1], c[2] - t[2])\n", + " if a in out:\n", + " continue\n", + " ok = True\n", + " for u in cells:\n", + " p = (a[0] + u[0], a[1] + u[1], a[2] + u[2])\n", + " if not (0 <= p[0] < n1 and 0 <= p[1] < n2 and 0 <= p[2] < n3):\n", + " ok = False\n", + " break\n", + " if occ[p] != 0:\n", + " ok = False\n", + " break\n", + " if ok:\n", + " out.append(a)\n", + " return sorted(out)\n", + "\n", + " def solve() -> bool:\n", + " nonlocal nodes\n", + " nodes += 1\n", + " if nodes > max_nodes:\n", + " raise _NodeBudgetExceeded\n", + " flat = occ.reshape(-1)\n", + " k = int(np.argmin(flat)) # première cellule libre en ordre C\n", + " if int(flat[k]) != 0:\n", + " return True # plus aucune cellule libre : succès\n", + " c3 = np.unravel_index(k, (n1, n2, n3))\n", + " c: Cell = (int(c3[0]), int(c3[1]), int(c3[2]))\n", + " for a in candidates(c):\n", + " placed = [(a[0] + u[0], a[1] + u[1], a[2] + u[2]) for u in cells]\n", + " for p in placed:\n", + " occ[p] = 1\n", + " anchors.append(a)\n", + " if solve():\n", + " return True\n", + " anchors.pop()\n", + " for p in placed:\n", + " occ[p] = 0\n", + " return False\n", + "\n", + " try:\n", + " solved = solve()\n", + " except _NodeBudgetExceeded:\n", + " return None, nodes\n", + " if not solved:\n", + " return None, nodes\n", + "\n", + " placement: Placement = {}\n", + " for a in anchors:\n", + " for u in cells:\n", + " placement[(a[0] + u[0], a[1] + u[1], a[2] + u[2])] = a\n", + " return placement, nodes\n", + "\n", + "\n", + "def period_rank(\n", + " placement: Placement, window_shape: tuple[int, int, int]\n", + ") -> tuple[int, list[Cell]]:\n", + " \"\"\"Rang sur Z du groupe des périodes du tuilage, vues DANS la fenêtre.\n", + "\n", + " v est une période si, pour toute cellule c telle que c+v soit aussi dans\n", + " la fenêtre, placement[c+v] == placement[c] + v (la copie qui couvre c,\n", + " translatée de v, couvre c+v). Boîte de test bornée : |v_i| <= floor(N_i/2)\n", + " (borne heuristique du sujet) ; les vecteurs v et -v sont identifiés et\n", + " chaque période est mise sous forme canonique (premier coefficient non nul\n", + " positif).\n", + "\n", + " Retour : (rang, generateurs) — sous-ensemble libre maximal pris dans\n", + " l'ordre croissant (élimination gaussienne exacte sur Q via Fraction).\n", + " \"\"\"\n", + " n1, n2, n3 = (int(v) for v in window_shape)\n", + " anchor = np.zeros((n1, n2, n3, 3), dtype=np.int64)\n", + " mask = np.zeros((n1, n2, n3), dtype=bool) # cellules présentes dans le placement\n", + " for c, a in placement.items():\n", + " anchor[c] = a\n", + " mask[c] = True\n", + "\n", + " dims = (n1, n2, n3)\n", + " periods: list[Cell] = []\n", + " ranges = product(*(range(-(n // 2), n // 2 + 1) for n in dims))\n", + " for v in ranges:\n", + " if v == (0, 0, 0):\n", + " continue\n", + " if any(n - abs(vi) < 1 for n, vi in zip(dims, v)):\n", + " continue # chevauchement vide : « période » vide de sens, on ignore\n", + " src: list[slice] = []\n", + " dst: list[slice] = []\n", + " for n_i, v_i in zip(dims, v):\n", + " if v_i >= 0:\n", + " src.append(slice(0, n_i - v_i))\n", + " dst.append(slice(v_i, n_i))\n", + " else:\n", + " src.append(slice(-v_i, n_i))\n", + " dst.append(slice(0, n_i + v_i))\n", + " shifted = anchor[tuple(dst)]\n", + " base = anchor[tuple(src)] + np.array(v, dtype=np.int64)\n", + " both = mask[tuple(dst)] & mask[tuple(src)]\n", + " if not bool(np.any(both)):\n", + " continue # chevauchement réduit aux seuls trous : période vide de sens\n", + " eq = np.all(shifted == base, axis=-1) # égalité des ancres, axe vec inclus\n", + " if bool(np.all(eq | ~both)):\n", + " w = tuple(int(x) for x in v)\n", + " for x in w: # forme canonique : premier coefficient non nul positif\n", + " if x < 0:\n", + " w = tuple(-y for y in w)\n", + " break\n", + " if x > 0:\n", + " break\n", + " if w not in periods:\n", + " periods.append(w)\n", + "\n", + " # Préférence pour les générateurs courts (norme L1, puis ordre) : pure\n", + " # lisibilité pédagogique, sans effet sur le rang ni le déterminisme.\n", + " periods.sort(key=lambda w: (sum(abs(x) for x in w), w))\n", + " gens = _independent_basis(periods)\n", + " return len(gens), gens\n", + "\n", + "\n", + "def _independent_basis(vectors: list[Cell]) -> list[Cell]:\n", + " \"\"\"Sous-ensemble libre maximal, par élimination gaussienne exacte sur Q.\"\"\"\n", + " rows: list[list[Fraction]] = []\n", + " pivots: list[int] = []\n", + " kept: list[Cell] = []\n", + " for v in vectors:\n", + " row = [Fraction(x) for x in v]\n", + " for piv, r in zip(pivots, rows):\n", + " f = row[piv]\n", + " if f:\n", + " row = [a - f * b for a, b in zip(row, r)]\n", + " for j, val in enumerate(row):\n", + " if val:\n", + " row = [a / val for a in row]\n", + " rows.append(row)\n", + " pivots.append(j)\n", + " kept.append(v)\n", + " break\n", + " return kept\n" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "95545d8d", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-08T22:34:55.896536Z", + "iopub.status.busy": "2026-10-08T22:34:55.896153Z", + "iopub.status.idle": "2026-10-08T22:34:55.901083Z", + "shell.execute_reply": "2026-10-08T22:34:55.900217Z" + }, + "papermill": { + "duration": 0.011048, + "end_time": "2026-10-08T22:34:55.902220", + "exception": false, + "start_time": "2026-10-08T22:34:55.891172", + "status": "completed" + }, + "tags": [] + }, + "outputs": [], + "source": [ + "def mesurer(nom: str, cells: set[Cell], win: tuple[int, int, int]) -> dict[str, object]:\n", + " \"\"\"Resout une fenetre, mesure le rang des periodes, imprime et retourne.\"\"\"\n", + " placement, nodes = place_tiles(win, cells)\n", + " entry: dict[str, object] = {\n", + " \"tile\": nom, \"cells\": sorted(cells), \"window\": list(win),\n", + " \"nodes\": nodes, \"solved\": placement is not None,\n", + " }\n", + " if placement is None:\n", + " print(f\" {nom} | fenetre {win} | nodes {nodes} | NON RESOLU\")\n", + " return entry\n", + " rang, gens = period_rank(placement, win)\n", + " entry[\"period_rank\"] = rang\n", + " entry[\"generators\"] = [list(g) for g in gens]\n", + " print(f\" {nom} | fenetre {win} | nodes {nodes} | rang {rang} | generateurs {gens}\")\n", + " return entry\n" + ] + }, + { + "cell_type": "markdown", + "id": "b135ee6a", + "metadata": { + "papermill": { + "duration": 0.002856, + "end_time": "2026-10-08T22:34:55.908712", + "exception": false, + "start_time": "2026-10-08T22:34:55.905856", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### 3.1 Expérience A — le domino, témoin périodique\n", + "\n", + "Deux fenêtres : un cube 4×4×4 (le régime confortable) et une fenêtre volontairement **mince** (6,4,2) — la période (0,0,2) du domino y dépasse la demi-fenêtre z (= 1).\n" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "185d9c81", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-08T22:34:55.915892Z", + "iopub.status.busy": "2026-10-08T22:34:55.915527Z", + "iopub.status.idle": "2026-10-08T22:34:55.926719Z", + "shell.execute_reply": "2026-10-08T22:34:55.925705Z" + }, + "papermill": { + "duration": 0.017048, + "end_time": "2026-10-08T22:34:55.927966", + "exception": false, + "start_time": "2026-10-08T22:34:55.910918", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + " domino | fenetre (4, 4, 4) | nodes 33 | rang 3 | generateurs [(0, 1, 0), (1, 0, 0), (0, 0, 2)]\n", + " domino | fenetre (6, 4, 2) | nodes 25 | rang 2 | generateurs [(0, 1, 0), (1, 0, 0)]\n" + ] + } + ], + "source": [ + "# A -- domino 1x1x2 : controle periodique.\n", + "domino: set[Cell] = {(0, 0, 0), (0, 0, 1)}\n", + "a_confort = mesurer(\"domino\", domino, (4, 4, 4))\n", + "a_mince = mesurer(\"domino\", domino, (6, 4, 2))\n" + ] + }, + { + "cell_type": "markdown", + "id": "9d0c5636", + "metadata": { + "papermill": { + "duration": 0.002652, + "end_time": "2026-10-08T22:34:55.933542", + "exception": false, + "start_time": "2026-10-08T22:34:55.930890", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "Sur la fenêtre confortable (4,4,4), le groupe des périodes observé est de **rang 3** — trois générateurs indépendants dont (0,0,2) : le domino est totalement périodique, la mesure le voit. Sur la fenêtre mince (6,4,2), le rang mesuré tombe à **2** alors que la tuile n'a pas changé et reste périodique : la période (0,0,2) dépasse la demi-fenêtre z (⌊2/2⌋ = 1) et devient **invisible**. Le témoin périodique échoue donc lui-même à se montrer périodique quand la fenêtre est trop petite — c'est la première leçon de mesure du carnet : *le rang mesuré est un minorant du rang vrai, plafonné par la demi-fenêtre*.\n" + ] + }, + { + "cell_type": "markdown", + "id": "0d14435b", + "metadata": { + "papermill": { + "duration": 0.002714, + "end_time": "2026-10-08T22:34:55.938931", + "exception": false, + "start_time": "2026-10-08T22:34:55.936217", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### 3.2 Expérience B0 — le prisme en L : un échec de recherche qui est un théorème\n", + "\n", + "Le triomino en L du plan xy ({(0,0,0), (1,0,0), (0,1,0)}), prismé avec une épaisseur 1 en z. On le lance sur trois fenêtres croissantes — il n'en résout **aucune**, en très peu de nœuds. Ce n'est pas un épuisement du solveur : c'est une **preuve**. Dans chaque plan z (la tuile étant plate), le coin (0,0) d'une boîte n'est couvrable que par l'ancre (0,0) — les deux autres candidats sortent — ce qui couvre (1,0) et (0,1) ; puis (0,2) n'est couvrable que par l'ancre (0,2), qui couvre (1,2) et (0,3) ; par induction toute la colonne 0 et les cases (1, pair) sont couvertes par des ancres forcées, et la case (1,1) n'a plus **aucun** candidat valide. Aucun rectangle 2D n'est tuilable par le L à orientation fixée, et le prisme plat hérite du résultat plan par plan.\n", + "\n", + "Leçon pour la famille 155 : une tuile peut être **si** contraignante qu'elle interdit tout pavage — le contre-exemple 155 est l'équilibre inverse et subtil, une tuile qui pave ℤ³ mais interdit seulement la périodicité totale.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "d831e6f6", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-08T22:34:55.945899Z", + "iopub.status.busy": "2026-10-08T22:34:55.945579Z", + "iopub.status.idle": "2026-10-08T22:34:55.950428Z", + "shell.execute_reply": "2026-10-08T22:34:55.949504Z" + }, + "papermill": { + "duration": 0.009574, + "end_time": "2026-10-08T22:34:55.951240", + "exception": false, + "start_time": "2026-10-08T22:34:55.941666", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + " L_prisme | fenetre (3, 3, 3) | nodes 4 | NON RESOLU\n", + " L_prisme | fenetre (4, 3, 3) | nodes 4 | NON RESOLU\n", + " L_prisme | fenetre (6, 4, 2) | nodes 5 | NON RESOLU\n" + ] + } + ], + "source": [ + "# B0 -- prisme L x {0} : ne tuile AUCUNE boite alignee (theoreme, cf. prose).\n", + "l_prisme: set[Cell] = {(0, 0, 0), (1, 0, 0), (0, 1, 0)}\n", + "b0 = [mesurer(\"L_prisme\", l_prisme, w) for w in ((3, 3, 3), (4, 3, 3), (6, 4, 2))]\n" + ] + }, + { + "cell_type": "markdown", + "id": "0370d30c", + "metadata": { + "papermill": { + "duration": 0.002896, + "end_time": "2026-10-08T22:34:55.957031", + "exception": false, + "start_time": "2026-10-08T22:34:55.954135", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### 3.3 Expérience B1 — le domino troué : une période minimale prouvée, et l'artefact de fenêtre\n", + "\n", + "Le domino troué {(0,0,0),(2,0,0)} : deux cellules séparées d'un trou. Sur chaque ligne x, chaque cellule est soit une ancre, soit une ancre + 2 (exactement une fois chacune) : notant f(n) ∈ {0,1} l'indicateur « n est une ancre », on a **f(n) + f(n−2) = 1 pour tout n**. La phase des ancres est donc exactement 4-périodique, et **aucune période x strictement inférieure à 4 n'existe dans aucun pavage** — une contrainte prouvée à la main, pas mesurée. Conséquence immédiate sur la mesure : une fenêtre de demi-largeur < 4 ne peut jamais certifier la période x. On mesure (4,2,2) puis (8,2,2).\n", + "\n", + "### 3.4 Expérience B2 — le cube dilaté : le piège « semble apériodique »\n", + "\n", + "Le cube dilaté {0,2}³ : les 8 coins d'un cube 2×2×2 espacé. Chaque copie ne couvre que des cellules de **sa classe de parité** (ajouter 2 préserve la parité de chaque coordonnée) ; par classe, le pavage se réduit (après division par 2) à un pavage par cubes unité. D'où un pavage de ℤ³ **unique** : ancres {0,1}³ + 4ℤ³, groupe de périodes **exactement 4ℤ³**. Sur (4,4,4), aucune période n'entre dans la boîte de test (|vᵢ| ≤ 2) : le rang mesuré tombe à **0** — l'allure « totalement apériodique » — alors que le vrai groupe est de rang 3. Sur (8,8,8), les trois générateurs (4,0,0), (0,4,0), (0,0,4) apparaissent.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "73028675", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-08T22:34:55.964083Z", + "iopub.status.busy": "2026-10-08T22:34:55.963752Z", + "iopub.status.idle": "2026-10-08T22:34:55.986715Z", + "shell.execute_reply": "2026-10-08T22:34:55.985898Z" + }, + "papermill": { + "duration": 0.027593, + "end_time": "2026-10-08T22:34:55.987521", + "exception": false, + "start_time": "2026-10-08T22:34:55.959928", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + " domino_troue | fenetre (4, 2, 2) | nodes 9 | rang 2 | generateurs [(0, 0, 1), (0, 1, 0)]\n", + " domino_troue | fenetre (8, 2, 2) | nodes 17 | rang 3 | generateurs [(0, 0, 1), (0, 1, 0), (4, 0, 0)]\n", + " cube_dilate | fenetre (4, 4, 4) | nodes 9 | rang 0 | generateurs []\n", + " cube_dilate | fenetre (8, 8, 8) | nodes 65 | rang 3 | generateurs [(0, 0, 4), (0, 4, 0), (4, 0, 0)]\n" + ] + } + ], + "source": [ + "# B1 -- domino troue : periode x minimale PROUVEE = 4 (cf. prose 3.3).\n", + "domino_troue: set[Cell] = {(0, 0, 0), (2, 0, 0)}\n", + "b1_etroite = mesurer(\"domino_troue\", domino_troue, (4, 2, 2))\n", + "b1_large = mesurer(\"domino_troue\", domino_troue, (8, 2, 2))\n", + "\n", + "# B2 -- cube dilate : pavage de Z^3 unique, periodes exactement 4Z^3 (cf. prose 3.4).\n", + "cube_dilate: set[Cell] = {(x, y, z) for x in (0, 2) for y in (0, 2) for z in (0, 2)}\n", + "b2_petite = mesurer(\"cube_dilate\", cube_dilate, (4, 4, 4))\n", + "b2_grande = mesurer(\"cube_dilate\", cube_dilate, (8, 8, 8))\n" + ] + }, + { + "cell_type": "markdown", + "id": "d946caf0", + "metadata": { + "papermill": { + "duration": 0.001967, + "end_time": "2026-10-08T22:34:55.991638", + "exception": false, + "start_time": "2026-10-08T22:34:55.989671", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "Le domino troué : rang **2** sur (4,2,2) — les périodes partielles (0,1,0) et (0,0,1) seulement — puis rang **3** sur (8,2,2) où le générateur (4,0,0) devient visible, exactement la période minimale prouvée. Le cube dilaté pousse le même phénomène à l'extrême : rang **0** sur (4,4,4) — l'allure la plus apériodique qui soit — puis rang **3** sur (8,8,8) avec les trois générateurs de 4ℤ³. Les deux tuiles sont **périodiques** (leurs vrais groupes sont de rang 3) ; ce sont les fenêtres qui mentent, chacune dans l'autre sens :\n", + "\n", + "- petite fenêtre ⇒ périodes invisibles ⇒ rang mesuré **trop petit** (B1, B2) ;\n", + "- la réciproque n'existe pas : un rang 3 mesuré est un **certificat** de périodicité totale (trois périodes vues), mais un rang < 3 n'est jamais un certificat d'apériodicité.\n" + ] + }, + { + "cell_type": "markdown", + "id": "70b55fcb", + "metadata": { + "papermill": { + "duration": 0.001834, + "end_time": "2026-10-08T22:34:55.995489", + "exception": false, + "start_time": "2026-10-08T22:34:55.993655", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 4. Ce qu'une fenêtre finie peut établir — et ce qu'elle ne peut pas\n", + "\n", + "Une fenêtre finie ne peut **jamais prouver** l'apériodicité, pour une raison simple : tout pavage fini observé sur W est compatible avec un pavage de ℤ³ totalement périodique (répéter le motif de W). Les mesures du §3 le portent avec les chiffres :\n", + "\n", + "- le **témoin** A lui-même rend rang 2 sur une fenêtre mince — le plafond de demi-fenêtre frappe même les tuiles les plus simples ;\n", + "- le domino troué (B1) et le cube dilaté (B2) ont des périodes minimales **prouvées** (4 en x pour l'un, 4ℤ³ exactement pour l'autre) : leurs rangs mesurés 2 et 0 sur petites fenêtres sont des **artefacts de visibilité**, levés quand la fenêtre double ;\n", + "- le prisme en L (B0) rappelle l'autre bord du spectre : une contrainte locale peut interdire **tout** pavage d'une boîte — l'échec du solveur y est une preuve, parce qu'elle est courte et structurée (ancres forcées), pas un épuisement.\n", + "\n", + "Ce que la mesure apporte donc : **elle calibre** (le rang mesuré est un minorant plafonné par la demi-fenêtre), **elle compare** (le coût en nœuds du backtracking dit si la contrainte locale mord), **elle piège** (B2 montre qu'un rang 0 mesuré ne dit rien du vrai groupe). Ce qu'elle ne remplace pas : le théorème 155, qui établit l'absence de rang 3 pour **tous** les pavages de sa tuile — un quantificateur universel qu'aucune fenêtre finie n'atteint.\n", + "\n", + "C'est la division du travail de la série ANALYSE : le carnet Python **mesure et illustre**, la formalisation **prouve** — ici, le squelette Lean publié par le corpus pour la famille 155.\n" + ] + }, + { + "cell_type": "markdown", + "id": "dabd9d12", + "metadata": { + "papermill": { + "duration": 0.00204, + "end_time": "2026-10-08T22:34:55.999367", + "exception": false, + "start_time": "2026-10-08T22:34:55.997327", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 5. Exercices\n", + "\n", + "### Exercice 1 — le groupe des périodes, pas seulement son rang\n", + "\n", + "La fonction `period_rank` rend le rang et des générateurs. Écrivez `period_group(placement, window_shape)` qui retourne la **liste complète** des vecteurs de période trouvés (sous forme canonique), puis vérifiez sur le domino que les périodes de norme L1 minimale sont (1,0,0), (0,1,0) et (0,0,2) — et expliquez pourquoi le pas est 2 et non 1 dans la direction longue.\n", + "\n", + "```python\n", + "# TODO etudiant\n", + "def period_group(placement, window_shape):\n", + " # Indice : reprendre la boucle de sondage de period_rank et collecter\n", + " # TOUS les vecteurs v non nuls invariants, au lieu de s'arreter a une base.\n", + " # Etape 1 : lister les candidats dans la demi-fenetre.\n", + " # Etape 2 : tester l'invariance (comparaison vectorisee des ancres).\n", + " # Etape 3 : mettre chaque periode sous forme canonique et dedupliquer.\n", + " return None\n", + "```\n", + "\n", + "### Exercice 2 — la plus petite fenêtre qui révèle le générateur x\n", + "\n", + "Pour le domino troué, la période x minimale est 4 (prouvée au §3.3). Trouvez expérimentalement la plus petite fenêtre (N₁,2,2) à partir de laquelle le générateur (4,0,0) devient **visible** dans la mesure, et vérifiez que c'est bien N₁ = 8 (demi-fenêtre 4). Que se passe-t-il pour N₁ = 7 ?\n", + "\n", + "```python\n", + "# TODO etudiant\n", + "def plus_petite_fenetre_revelante(tile_cells, axe=0):\n", + " # Indice : balayer N1 croissant, appeler place_tiles puis period_rank,\n", + " # s'arreter au premier rang 3. Attention au cas N1 impair (demi-fenetre\n", + " # floor) : la reponse de N1=7 surprend-elle au vu de floor(7/2) = 3 ?\n", + " return None\n", + "```\n", + "\n", + "### Exercice 3 — construire une contrainte de parité\n", + "\n", + "Le cube dilaté doit son pavage unique à un argument de **classe de parité**. Construisez une autre tuile dont le pavage de ℤ³ est unique par le même argument (par exemple un « domino dilaté » {(0,0,0),(2,0,0)} déjà vu — cherchez plutôt un triomino dilaté), prouvez l'unicité à la main, puis vérifiez que la mesure rend rang 0 sur petite fenêtre et rang 3 sur grande fenêtre, avec les générateurs attendus.\n", + "\n", + "```python\n", + "# TODO etudiant\n", + "def triomino_dilate():\n", + " # Indice : prendre les trois cellules du L, multiplier chaque coordonnee\n", + " # par 2, et raisonner par classe de parite comme au 3.4.\n", + " # Etape 1 : proposer la forme. Etape 2 : prouver l'unicite a la main.\n", + " # Etape 3 : mesurer sur (4,4,4) puis (8,8,8) et confronter.\n", + " return None\n", + "```\n" + ] + }, + { + "cell_type": "markdown", + "id": "51fdc696", + "metadata": { + "papermill": { + "duration": 0.004763, + "end_time": "2026-10-08T22:34:56.008744", + "exception": false, + "start_time": "2026-10-08T22:34:56.003981", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## Conclusion\n", + "\n", + "### Ce qui a été établi\n", + "\n", + "| Résultat | Mesure |\n", + "|---|---|\n", + "| Le domino est totalement périodique | rang 3 sur (4,4,4), générateurs dont (0,0,2) |\n", + "| Une fenêtre mince cache même les périodes évidentes | rang 2 sur (6,4,2) pour ce même domino |\n", + "| Le prisme en L ne pave aucune boîte alignée | 0/3 fenêtres résolues, échec court et structuré (théorème) |\n", + "| Le domino troué a une période x minimale prouvée de 4 | rang 2 sur (4,2,2) puis 3 sur (8,2,2), générateur (4,0,0) |\n", + "| Le cube dilaté a un pavage unique de groupe 4ℤ³ | rang 0 sur (4,4,4) puis 3 sur (8,8,8) |\n", + "| Une fenêtre finie ne prouve jamais l'apériodicité | argument du §4 : motif répété |\n", + "\n", + "### Ce qui reste au théorème\n", + "\n", + "L'énoncé 155 — un carreau fini de ℤ³ qui pave sans **aucun** pavage de rang 3 — n'est pas re-démontré ici : il est **présenté**, sourcé du corpus openai/math (squelette Lean publié), et illustré par des cas jouets mesurés dont chacun borne honnêtement sa portée. Le pont naturel est double : la formalisation côté Lean (le squelette du corpus), et l'exact-cover côté `sudoku_lean` — la sémantique est la même, seules les instances changent.\n", + "\n", + "**Pistes pour la suite** : le passage ℝ³ (épaississement en cubes unitaires, translations réelles arbitraires) ; la comparaison avec les jeux de tuiles apériodiques classiques (Berger 1966, Jeandel–Rao en 2D — une *famille* de tuiles, là où 155 donne un carreau *unique*) ; et la complexité algorithmique du pavage (indécidabilité en général, le résultat de Berger).\n" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "name": "python", + "version": "3.13" + }, + "papermill": { + "default_parameters": {}, + "duration": 2.302952, + "end_time": "2026-10-08T22:34:56.256368", + "environment_variables": {}, + "exception": null, + "input_path": "ANALYSE-09-Tuilage-Aperiodique.ipynb", + "output_path": "ANALYSE-09-Tuilage-Aperiodique.ipynb", + "parameters": {}, + "start_time": "2026-10-08T22:34:53.953416", + "version": "2.6.0" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-09-Tuilage-Aperiodique_en.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-09-Tuilage-Aperiodique_en.ipynb new file mode 100644 index 0000000000..37156561b6 --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-09-Tuilage-Aperiodique_en.ipynb @@ -0,0 +1,602 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "6f91e0b5", + "metadata": { + "papermill": { + "duration": 0.002612, + "end_time": "2026-10-08T22:34:55.771634", + "exception": false, + "start_time": "2026-10-08T22:34:55.769022", + "status": "completed" + }, + "tags": [] + }, + "source": "# ANALYSE-09: A single tile of Z^3 that tiles without full periodicity\n\n**Series**: SymbolicAI / Lean — Digestions of deep results, companion to the capstone [Lean-20 — Digestions Tao](../Lean-20-Capstone-Digestions-Tao-Python.ipynb)\n**Source**: family 155 of the openai/math corpus (\"A counterexample to periodic tiling in dimension three\", published Lean skeleton) — reconnaissance repository `G:\\Mon Drive\\MyIA\\IA\\Distillations\\2026-10-openai-math\\`\n**Source lake**: `sudoku_lean` (the repository's exact-cover / discrete tiling semantics, `MyIA.AI.Notebooks/Sudoku/sudoku_lean/`)\n**Kernel**: `python3` — this notebook illustrates the definitions and measures toy cases; the formal statement remains the corpus's\n\n## Navigation\n\n| Previous notebook | Next notebook |\n|---|---|\n| [ANALYSE-04 - PFR Primitives](ANALYSE-04-PFR-Primitives-Python.ipynb) | [Series index](README.md) |\n\n***\n\n## Why this notebook\n\nThe periodic tiling conjecture says, roughly: *if a shape tiles space, it tiles it periodically*. It is true in dimension 1, true for a single tile in dimension 2 (on Z^2), and **false from dimension 3 onward**: family 155 of the openai/math corpus exhibits a **single tile** — a finite set T ⊂ Z^3 — that tiles Z^3 by translations but for which **no tiling is fully periodic**.\n\nThis is the counterexample in the **smallest possible dimension** for a single tile. The unit-cube thickening carries the same counterexample over to R^3, even allowing arbitrary real translation vectors.\n\n> **Epistemic status**: openai/math is a third-party source not verified by us. The statement above is the one declared by the corpus (published Lean skeleton for family 155); this notebook **presents** it and **illustrates** it on measured toy cases — it does not re-prove the theorem.\n\n## What the notebook establishes (plan)\n\n1. **§1** — the exact definitions: tile, tiling by translations, period, *full periodicity* (rank 3) — and why \"aperiodic\" is subtler than \"without any period\".\n2. **§2** — the exact-cover connection: tiling a finite window is solving an exact cover — the semantics that the `sudoku_lean` lake formalizes.\n3. **§3** — the engine (bounded backtracking + period-rank measurement) and four measured experiments: a periodic control, a tile that tiles **no** box (and why that is a theorem), a tile with a **proven** minimal period of exactly 4, and a trap: a tile that **looks** aperiodic on a small window.\n4. **§4** — honest reading: what finite windows can and cannot establish, with the §3 measurements as evidence.\n" + }, + { + "cell_type": "markdown", + "id": "9a64e407", + "metadata": { + "papermill": { + "duration": 0.002373, + "end_time": "2026-10-08T22:34:55.777340", + "exception": false, + "start_time": "2026-10-08T22:34:55.774967", + "status": "completed" + }, + "tags": [] + }, + "source": "## 1. Definitions — tile, tiling, full periodicity\n\n**Tile.** A *tile* is a nonempty **finite** set T ⊂ Z^3. Its elements are cells; one thinks of a connected polycube, but the definition does not require connectivity.\n\n**Tiling by translations.** The tile T *tiles* Z^3 if there exists a set of translations S ⊂ Z^3 such that the copies T + s (s ∈ S) cover Z^3 **exactly**: every cell of Z^3 belongs to one and only one copy. This is an **exact cover** of Z^3 by translated copies of T — no hole, no overlap.\n\n**Period, periodic tiling.** A vector v ∈ Z^3 \\ {0} is a *period* of a tiling if its set of translations is invariant under v: translating the whole tiling by v leaves it unchanged. The **period group** of a tiling is a subgroup of Z^3; it has a **rank** r ∈ {0, 1, 2, 3} (dimension of the Z-module).\n\n**Full periodicity.** A tiling is *fully periodic* when r = 3: three independent periods. This is the notion that theorem 155 strikes down: the counterexample tile tiles Z^3, but **none** of its tilings reaches full rank.\n\n**Why this nuance matters.** \"Aperiodic\" does not mean \"zero periods\": a tiling may admit one or two directions of periods (rank 1 or 2) and still be a counterexample — what is forbidden is full rank. A rank-2 tiling, for instance, repeats in two directions but never in the third: enough to refute the conjecture, not enough to be \"structureless\".\n" + }, + { + "cell_type": "markdown", + "id": "62457216", + "metadata": { + "papermill": { + "duration": 0.004423, + "end_time": "2026-10-08T22:34:55.784903", + "exception": false, + "start_time": "2026-10-08T22:34:55.780480", + "status": "completed" + }, + "tags": [] + }, + "source": "## 2. The exact-cover connection — what `sudoku_lean` formalizes\n\nOn a **finite window** W (an N₁×N₂×N₃ block of Z^3), tiling W by copies of T is an exact cover problem: every cell of W must be covered **exactly once**, every tile placement is a \"choice\", and the choices must be pairwise non-conflicting.\n\nThis is exactly the semantics of the repository's `sudoku_lean` lake: `ExactCover.IsExactCover` (`MyIA.AI.Notebooks/Sudoku/sudoku_lean/Sudoku/ExactCover.lean`) defines the exact cover of a set of *scopes* by a selection, and Sudoku is the canonical instance there. Sudoku is a tiling: every cell receives exactly one digit, every constraint is covered exactly once. Our tiling window is another instance of the same semantics — cells × placements instead of cells × values.\n\n> **Declared pedagogical copy** (organ-first rule of the repository): the bounded solver in this notebook is a **declared** local reimplementation — plain, readable Python backtracking — of the exact-cover semantics. The native organ (`sudoku_lean`) is a Lean proof lake, not a consumable Python library; the real invocation is unavailable on the Python side, and the goal here is to show the mechanics, not to prove them. Answers to the 5 questions: the Sudoku series owns the semantics (1); its module is not invocable from Python (2); exporting it would require a port with no pedagogical value here (3); the organ's negative witness is the formal proof `mem_toSelection_iff`, out of reach for a notebook (4); the independent verification is the multi-window replay of §3, whose measured ranks confront the hand-proven constraints (5).\n" + }, + { + "cell_type": "markdown", + "id": "3acb0f1e", + "metadata": { + "papermill": { + "duration": 0.002787, + "end_time": "2026-10-08T22:34:55.791388", + "exception": false, + "start_time": "2026-10-08T22:34:55.788601", + "status": "completed" + }, + "tags": [] + }, + "source": "## 3. The engine and the four experiments\n\nThe engine has two organs, both deterministic:\n\n- `place_tiles(window, tile)` — bounded exact-cover **backtracking**: the first free cell (lexicographic order) forces the choice of the anchor covering it, descend, backtrack. The node counter measures the combinatorial cost.\n- `period_rank(placement, window)` — for the tiling obtained, tests all period vectors v in the box |vᵢ| ≤ ⌊Nᵢ/2⌋ (the **half-window**) and returns the Z-rank of the group they generate (exact Gaussian elimination over the rationals).\n\nThe half-window is the reading key to all of §3: **any period longer than the half-window is invisible**. This is a measurement ceiling, not a property of the tile — experiments A and B2 each show it in their own way.\n\nFour experiments:\n\n| # | Tile | What is measured | Hand-provable constraint |\n|---|---|---|---|\n| A | 1×1×2 domino | the periodic control: rank 3 expected | obvious tiling, periods 1 or 2 |\n| B0 | L×{0} prism | the tiles **no** aligned box | theorem: forced corner, induction, dead cell (1,1) |\n| B1 | gapped domino {(0,0,0),(2,0,0)} | rank 2 then rank 3 as the window grows | minimal x-period **exactly 4** in every tiling |\n| B2 | doubled cube {0,2}³ | rank 0 then rank 3 | **unique** tiling of Z^3, periods exactly 4Z³ |\n" + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "4ec88ea1", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-08T22:34:55.797744Z", + "iopub.status.busy": "2026-10-08T22:34:55.797486Z", + "iopub.status.idle": "2026-10-08T22:34:55.885852Z", + "shell.execute_reply": "2026-10-08T22:34:55.884597Z" + }, + "papermill": { + "duration": 0.093331, + "end_time": "2026-10-08T22:34:55.887334", + "exception": false, + "start_time": "2026-10-08T22:34:55.794003", + "status": "completed" + }, + "tags": [] + }, + "outputs": [], + "source": [ + "\"\"\"Moteur de calcul pour le notebook ANALYSE-09-Tuilage-Aperiodique (famille 155).\n", + "\n", + "Famille 155 : « contre-exemple au tuilage périodique en dimension trois » —\n", + "il existe une tuile translative finie T sous-ensemble de Z^3 qui tuile Z^3\n", + "mais n'admet AUCUN tuilage pleinement périodique (groupe de périodes de rang\n", + "3) ; des périodes partielles de rang < 3 peuvent exister. La tuile du théorème\n", + "est énorme : ce moteur fournit donc des mesures BORNÉES et HONNÊTES sur de\n", + "petites fenêtres.\n", + "\n", + "Deux organes :\n", + " * place_tiles : exact-cover par backtracking borné (translations seules,\n", + " aucune rotation), déterministe, avec compteur de noeuds ;\n", + " * period_rank : rang sur Z du groupe des vecteurs de période du tuilage\n", + " RESTREINT à la fenêtre, testés dans |v_i| <= floor(N_i/2).\n", + "\n", + "Limite pédagogique assumée (aussi dans tiling_measurements.json, champ\n", + "« limitation ») : une petite fenêtre ne peut jamais PROUVER l'apériodicité,\n", + "elle peut seulement la suggérer — une fenêtre plus grande peut révéler des\n", + "périodes jusqu'alors invisibles. La preuve du théorème vit dans la prose du\n", + "notebook, pas dans ces mesures.\n", + "\"\"\"\n", + "\n", + "from __future__ import annotations\n", + "\n", + "from fractions import Fraction\n", + "from itertools import product\n", + "from typing import Iterable, Optional\n", + "\n", + "import numpy as np\n", + "\n", + "Cell = tuple[int, int, int]\n", + "Placement = dict[Cell, Cell] # cellule -> ancre de la copie qui la couvre\n", + "\n", + "\n", + "\n", + "class _NodeBudgetExceeded(RuntimeError):\n", + " \"\"\"Budget de noeuds épuisé : instance abandonnée (ni échec ni succès).\"\"\"\n", + "\n", + "\n", + "def place_tiles(\n", + " window_shape: tuple[int, int, int],\n", + " tile_cells: Iterable[Cell],\n", + " forbidden: Optional[set[Cell]] = None,\n", + " *,\n", + " max_nodes: int = 2_000_000,\n", + ") -> tuple[Optional[Placement], int]:\n", + " \"\"\"Tente de tuiler exactement la fenêtre par copies translatées de la tuile.\n", + "\n", + " Parameters\n", + " ----------\n", + " window_shape : (N1, N2, N3) — boîte [0,N1) x [0,N2) x [0,N3).\n", + " tile_cells : décalages (x,y,z) de la tuile, relatifs à son ancre.\n", + " forbidden : cellules à laisser vides (trous), optionnel.\n", + " max_nodes : garde-fou sur le nombre de noeuds de backtracking.\n", + "\n", + " Retour\n", + " ------\n", + " (placement, nodes) où placement vaut None si aucun tuilage n'est trouvé\n", + " (ou si le budget de noeuds est épuisé). placement associe à chaque cellule\n", + " couverte l'ancre de la copie qui la couvre — support direct du test de\n", + " période de period_rank.\n", + "\n", + " Déterminisme : la première cellule libre est prise en ordre lexicographique\n", + " (ordre C : x lent, z rapide) et les ancre candidates sont essayées par\n", + " ordre croissant. Aucun aléatoire.\n", + " \"\"\"\n", + " n1, n2, n3 = (int(v) for v in window_shape)\n", + " if min(n1, n2, n3) < 1:\n", + " raise ValueError(\"window_shape doit valoir >= 1 sur chaque axe\")\n", + " cells: list[Cell] = sorted({(int(x), int(y), int(z)) for x, y, z in tile_cells})\n", + " if not cells:\n", + " raise ValueError(\"tile_cells est vide\")\n", + "\n", + " occ = np.zeros((n1, n2, n3), dtype=np.uint8) # 0 = libre, 1 = couvert, 2 = trou\n", + " if forbidden:\n", + " for (x, y, z) in forbidden:\n", + " occ[int(x), int(y), int(z)] = 2\n", + "\n", + " n_free = int((occ == 0).sum())\n", + " if n_free % len(cells) != 0:\n", + " return None, 1 # volume incompatible avec |T| : échec immédiat, décidé.\n", + "\n", + " anchors: list[Cell] = []\n", + " nodes = 0\n", + "\n", + " def candidates(c: Cell) -> list[Cell]:\n", + " \"\"\"Ancres valides couvrant la cellule c, triées (déterminisme).\"\"\"\n", + " out: list[Cell] = []\n", + " for t in cells:\n", + " a: Cell = (c[0] - t[0], c[1] - t[1], c[2] - t[2])\n", + " if a in out:\n", + " continue\n", + " ok = True\n", + " for u in cells:\n", + " p = (a[0] + u[0], a[1] + u[1], a[2] + u[2])\n", + " if not (0 <= p[0] < n1 and 0 <= p[1] < n2 and 0 <= p[2] < n3):\n", + " ok = False\n", + " break\n", + " if occ[p] != 0:\n", + " ok = False\n", + " break\n", + " if ok:\n", + " out.append(a)\n", + " return sorted(out)\n", + "\n", + " def solve() -> bool:\n", + " nonlocal nodes\n", + " nodes += 1\n", + " if nodes > max_nodes:\n", + " raise _NodeBudgetExceeded\n", + " flat = occ.reshape(-1)\n", + " k = int(np.argmin(flat)) # première cellule libre en ordre C\n", + " if int(flat[k]) != 0:\n", + " return True # plus aucune cellule libre : succès\n", + " c3 = np.unravel_index(k, (n1, n2, n3))\n", + " c: Cell = (int(c3[0]), int(c3[1]), int(c3[2]))\n", + " for a in candidates(c):\n", + " placed = [(a[0] + u[0], a[1] + u[1], a[2] + u[2]) for u in cells]\n", + " for p in placed:\n", + " occ[p] = 1\n", + " anchors.append(a)\n", + " if solve():\n", + " return True\n", + " anchors.pop()\n", + " for p in placed:\n", + " occ[p] = 0\n", + " return False\n", + "\n", + " try:\n", + " solved = solve()\n", + " except _NodeBudgetExceeded:\n", + " return None, nodes\n", + " if not solved:\n", + " return None, nodes\n", + "\n", + " placement: Placement = {}\n", + " for a in anchors:\n", + " for u in cells:\n", + " placement[(a[0] + u[0], a[1] + u[1], a[2] + u[2])] = a\n", + " return placement, nodes\n", + "\n", + "\n", + "def period_rank(\n", + " placement: Placement, window_shape: tuple[int, int, int]\n", + ") -> tuple[int, list[Cell]]:\n", + " \"\"\"Rang sur Z du groupe des périodes du tuilage, vues DANS la fenêtre.\n", + "\n", + " v est une période si, pour toute cellule c telle que c+v soit aussi dans\n", + " la fenêtre, placement[c+v] == placement[c] + v (la copie qui couvre c,\n", + " translatée de v, couvre c+v). Boîte de test bornée : |v_i| <= floor(N_i/2)\n", + " (borne heuristique du sujet) ; les vecteurs v et -v sont identifiés et\n", + " chaque période est mise sous forme canonique (premier coefficient non nul\n", + " positif).\n", + "\n", + " Retour : (rang, generateurs) — sous-ensemble libre maximal pris dans\n", + " l'ordre croissant (élimination gaussienne exacte sur Q via Fraction).\n", + " \"\"\"\n", + " n1, n2, n3 = (int(v) for v in window_shape)\n", + " anchor = np.zeros((n1, n2, n3, 3), dtype=np.int64)\n", + " mask = np.zeros((n1, n2, n3), dtype=bool) # cellules présentes dans le placement\n", + " for c, a in placement.items():\n", + " anchor[c] = a\n", + " mask[c] = True\n", + "\n", + " dims = (n1, n2, n3)\n", + " periods: list[Cell] = []\n", + " ranges = product(*(range(-(n // 2), n // 2 + 1) for n in dims))\n", + " for v in ranges:\n", + " if v == (0, 0, 0):\n", + " continue\n", + " if any(n - abs(vi) < 1 for n, vi in zip(dims, v)):\n", + " continue # chevauchement vide : « période » vide de sens, on ignore\n", + " src: list[slice] = []\n", + " dst: list[slice] = []\n", + " for n_i, v_i in zip(dims, v):\n", + " if v_i >= 0:\n", + " src.append(slice(0, n_i - v_i))\n", + " dst.append(slice(v_i, n_i))\n", + " else:\n", + " src.append(slice(-v_i, n_i))\n", + " dst.append(slice(0, n_i + v_i))\n", + " shifted = anchor[tuple(dst)]\n", + " base = anchor[tuple(src)] + np.array(v, dtype=np.int64)\n", + " both = mask[tuple(dst)] & mask[tuple(src)]\n", + " if not bool(np.any(both)):\n", + " continue # chevauchement réduit aux seuls trous : période vide de sens\n", + " eq = np.all(shifted == base, axis=-1) # égalité des ancres, axe vec inclus\n", + " if bool(np.all(eq | ~both)):\n", + " w = tuple(int(x) for x in v)\n", + " for x in w: # forme canonique : premier coefficient non nul positif\n", + " if x < 0:\n", + " w = tuple(-y for y in w)\n", + " break\n", + " if x > 0:\n", + " break\n", + " if w not in periods:\n", + " periods.append(w)\n", + "\n", + " # Préférence pour les générateurs courts (norme L1, puis ordre) : pure\n", + " # lisibilité pédagogique, sans effet sur le rang ni le déterminisme.\n", + " periods.sort(key=lambda w: (sum(abs(x) for x in w), w))\n", + " gens = _independent_basis(periods)\n", + " return len(gens), gens\n", + "\n", + "\n", + "def _independent_basis(vectors: list[Cell]) -> list[Cell]:\n", + " \"\"\"Sous-ensemble libre maximal, par élimination gaussienne exacte sur Q.\"\"\"\n", + " rows: list[list[Fraction]] = []\n", + " pivots: list[int] = []\n", + " kept: list[Cell] = []\n", + " for v in vectors:\n", + " row = [Fraction(x) for x in v]\n", + " for piv, r in zip(pivots, rows):\n", + " f = row[piv]\n", + " if f:\n", + " row = [a - f * b for a, b in zip(row, r)]\n", + " for j, val in enumerate(row):\n", + " if val:\n", + " row = [a / val for a in row]\n", + " rows.append(row)\n", + " pivots.append(j)\n", + " kept.append(v)\n", + " break\n", + " return kept\n" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "95545d8d", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-08T22:34:55.896536Z", + "iopub.status.busy": "2026-10-08T22:34:55.896153Z", + "iopub.status.idle": "2026-10-08T22:34:55.901083Z", + "shell.execute_reply": "2026-10-08T22:34:55.900217Z" + }, + "papermill": { + "duration": 0.011048, + "end_time": "2026-10-08T22:34:55.902220", + "exception": false, + "start_time": "2026-10-08T22:34:55.891172", + "status": "completed" + }, + "tags": [] + }, + "outputs": [], + "source": [ + "def mesurer(nom: str, cells: set[Cell], win: tuple[int, int, int]) -> dict[str, object]:\n", + " \"\"\"Resout une fenetre, mesure le rang des periodes, imprime et retourne.\"\"\"\n", + " placement, nodes = place_tiles(win, cells)\n", + " entry: dict[str, object] = {\n", + " \"tile\": nom, \"cells\": sorted(cells), \"window\": list(win),\n", + " \"nodes\": nodes, \"solved\": placement is not None,\n", + " }\n", + " if placement is None:\n", + " print(f\" {nom} | fenetre {win} | nodes {nodes} | NON RESOLU\")\n", + " return entry\n", + " rang, gens = period_rank(placement, win)\n", + " entry[\"period_rank\"] = rang\n", + " entry[\"generators\"] = [list(g) for g in gens]\n", + " print(f\" {nom} | fenetre {win} | nodes {nodes} | rang {rang} | generateurs {gens}\")\n", + " return entry\n" + ] + }, + { + "cell_type": "markdown", + "id": "b135ee6a", + "metadata": { + "papermill": { + "duration": 0.002856, + "end_time": "2026-10-08T22:34:55.908712", + "exception": false, + "start_time": "2026-10-08T22:34:55.905856", + "status": "completed" + }, + "tags": [] + }, + "source": "### 3.1 Experiment A — the domino, periodic control\n\nTwo windows: a comfortable 4×4×4 cube, and a deliberately **thin** (6,4,2) window — the domino's period (0,0,2) exceeds the z half-window there (= 1).\n" + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "185d9c81", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-08T22:34:55.915892Z", + "iopub.status.busy": "2026-10-08T22:34:55.915527Z", + "iopub.status.idle": "2026-10-08T22:34:55.926719Z", + "shell.execute_reply": "2026-10-08T22:34:55.925705Z" + }, + "papermill": { + "duration": 0.017048, + "end_time": "2026-10-08T22:34:55.927966", + "exception": false, + "start_time": "2026-10-08T22:34:55.910918", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + " domino | fenetre (4, 4, 4) | nodes 33 | rang 3 | generateurs [(0, 1, 0), (1, 0, 0), (0, 0, 2)]\n", + " domino | fenetre (6, 4, 2) | nodes 25 | rang 2 | generateurs [(0, 1, 0), (1, 0, 0)]\n" + ] + } + ], + "source": [ + "# A -- domino 1x1x2 : controle periodique.\n", + "domino: set[Cell] = {(0, 0, 0), (0, 0, 1)}\n", + "a_confort = mesurer(\"domino\", domino, (4, 4, 4))\n", + "a_mince = mesurer(\"domino\", domino, (6, 4, 2))\n" + ] + }, + { + "cell_type": "markdown", + "id": "9d0c5636", + "metadata": { + "papermill": { + "duration": 0.002652, + "end_time": "2026-10-08T22:34:55.933542", + "exception": false, + "start_time": "2026-10-08T22:34:55.930890", + "status": "completed" + }, + "tags": [] + }, + "source": "### Reading the result\n\nOn the comfortable window (4,4,4), the observed period group has **rank 3** — three independent generators including (0,0,2): the domino is fully periodic, and the measurement sees it. On the thin window (6,4,2), the measured rank drops to **2** although the tile has not changed and remains periodic: the period (0,0,2) exceeds the z half-window (⌊2/2⌋ = 1) and becomes **invisible**. The periodic control thus fails to show itself periodic when the window is too small — this is the notebook's first measurement lesson: *the measured rank is a lower bound on the true rank, capped by the half-window*.\n" + }, + { + "cell_type": "markdown", + "id": "0d14435b", + "metadata": { + "papermill": { + "duration": 0.002714, + "end_time": "2026-10-08T22:34:55.938931", + "exception": false, + "start_time": "2026-10-08T22:34:55.936217", + "status": "completed" + }, + "tags": [] + }, + "source": "### 3.2 Experiment B0 — the L prism: a search failure that is a theorem\n\nThe L triomino of the xy plane ({(0,0,0), (1,0,0), (0,1,0)}), prism-ed with thickness 1 in z. We run it on three growing windows — it solves **none**, in very few nodes. This is not solver exhaustion: it is a **proof**. In each z plane (the tile being flat), the corner (0,0) of a box can only be covered by the anchor (0,0) — the other two candidates leave the box — which covers (1,0) and (0,1); then (0,2) can only be covered by the anchor (0,2), which covers (1,2) and (0,3); by induction the whole column 0 and the cells (1, even) are covered by forced anchors, and cell (1,1) has **no** valid candidate left. No 2D rectangle is tileable by the fixed-orientation L, and the flat prism inherits the result plane by plane.\n\nLesson for family 155: a tile can be **so** constraining that it forbids all tilings — counterexample 155 is the opposite, subtle balance, a tile that tiles Z^3 but forbids only full periodicity.\n" + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "d831e6f6", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-08T22:34:55.945899Z", + "iopub.status.busy": "2026-10-08T22:34:55.945579Z", + "iopub.status.idle": "2026-10-08T22:34:55.950428Z", + "shell.execute_reply": "2026-10-08T22:34:55.949504Z" + }, + "papermill": { + "duration": 0.009574, + "end_time": "2026-10-08T22:34:55.951240", + "exception": false, + "start_time": "2026-10-08T22:34:55.941666", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + " L_prisme | fenetre (3, 3, 3) | nodes 4 | NON RESOLU\n", + " L_prisme | fenetre (4, 3, 3) | nodes 4 | NON RESOLU\n", + " L_prisme | fenetre (6, 4, 2) | nodes 5 | NON RESOLU\n" + ] + } + ], + "source": [ + "# B0 -- prisme L x {0} : ne tuile AUCUNE boite alignee (theoreme, cf. prose).\n", + "l_prisme: set[Cell] = {(0, 0, 0), (1, 0, 0), (0, 1, 0)}\n", + "b0 = [mesurer(\"L_prisme\", l_prisme, w) for w in ((3, 3, 3), (4, 3, 3), (6, 4, 2))]\n" + ] + }, + { + "cell_type": "markdown", + "id": "0370d30c", + "metadata": { + "papermill": { + "duration": 0.002896, + "end_time": "2026-10-08T22:34:55.957031", + "exception": false, + "start_time": "2026-10-08T22:34:55.954135", + "status": "completed" + }, + "tags": [] + }, + "source": "### 3.3 Experiment B1 — the gapped domino: a proven minimal period, and the window artifact\n\nThe gapped domino {(0,0,0),(2,0,0)}: two cells separated by a hole. On each x-line, every cell is either an anchor or an anchor + 2 (exactly once each): writing f(n) ∈ {0,1} for the indicator \"n is an anchor\", we have **f(n) + f(n−2) = 1 for all n**. The anchor phase is therefore exactly 4-periodic, and **no x-period strictly smaller than 4 exists in any tiling** — a hand-proven constraint, not a measured one. Immediate consequence on the measurement: a window with half-width < 4 can never certify the x-period. We measure (4,2,2) then (8,2,2).\n\n### 3.4 Experiment B2 — the doubled cube: the \"looks aperiodic\" trap\n\nThe doubled cube {0,2}³: the 8 corners of a spaced 2×2×2 cube. Every copy only covers cells of **its parity class** (adding 2 preserves the parity of each coordinate); per class, the tiling reduces (after division by 2) to a tiling by unit cubes. Hence a **unique** tiling of Z^3: anchors {0,1}³ + 4Z³, period group **exactly 4Z³**. On (4,4,4), no period fits in the test box (|vᵢ| ≤ 2): the measured rank drops to **0** — the fully \"aperiodic\" look — while the true group has rank 3. On (8,8,8), the three generators (4,0,0), (0,4,0), (0,0,4) appear.\n" + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "73028675", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-08T22:34:55.964083Z", + "iopub.status.busy": "2026-10-08T22:34:55.963752Z", + "iopub.status.idle": "2026-10-08T22:34:55.986715Z", + "shell.execute_reply": "2026-10-08T22:34:55.985898Z" + }, + "papermill": { + "duration": 0.027593, + "end_time": "2026-10-08T22:34:55.987521", + "exception": false, + "start_time": "2026-10-08T22:34:55.959928", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + " domino_troue | fenetre (4, 2, 2) | nodes 9 | rang 2 | generateurs [(0, 0, 1), (0, 1, 0)]\n", + " domino_troue | fenetre (8, 2, 2) | nodes 17 | rang 3 | generateurs [(0, 0, 1), (0, 1, 0), (4, 0, 0)]\n", + " cube_dilate | fenetre (4, 4, 4) | nodes 9 | rang 0 | generateurs []\n", + " cube_dilate | fenetre (8, 8, 8) | nodes 65 | rang 3 | generateurs [(0, 0, 4), (0, 4, 0), (4, 0, 0)]\n" + ] + } + ], + "source": [ + "# B1 -- domino troue : periode x minimale PROUVEE = 4 (cf. prose 3.3).\n", + "domino_troue: set[Cell] = {(0, 0, 0), (2, 0, 0)}\n", + "b1_etroite = mesurer(\"domino_troue\", domino_troue, (4, 2, 2))\n", + "b1_large = mesurer(\"domino_troue\", domino_troue, (8, 2, 2))\n", + "\n", + "# B2 -- cube dilate : pavage de Z^3 unique, periodes exactement 4Z^3 (cf. prose 3.4).\n", + "cube_dilate: set[Cell] = {(x, y, z) for x in (0, 2) for y in (0, 2) for z in (0, 2)}\n", + "b2_petite = mesurer(\"cube_dilate\", cube_dilate, (4, 4, 4))\n", + "b2_grande = mesurer(\"cube_dilate\", cube_dilate, (8, 8, 8))\n" + ] + }, + { + "cell_type": "markdown", + "id": "d946caf0", + "metadata": { + "papermill": { + "duration": 0.001967, + "end_time": "2026-10-08T22:34:55.991638", + "exception": false, + "start_time": "2026-10-08T22:34:55.989671", + "status": "completed" + }, + "tags": [] + }, + "source": "### Reading the result\n\nThe gapped domino: rank **2** on (4,2,2) — only the partial periods (0,1,0) and (0,0,1) — then rank **3** on (8,2,2) where the generator (4,0,0) becomes visible, exactly the proven minimal period. The doubled cube pushes the same phenomenon to the extreme: rank **0** on (4,4,4) — the most aperiodic look possible — then rank **3** on (8,8,8) with the three generators of 4Z³. Both tiles are **periodic** (their true groups have rank 3); it is the windows that lie, each in its own direction:\n\n- small window ⇒ invisible periods ⇒ measured rank **too small** (B1, B2);\n- the converse does not exist: a measured rank 3 is a **certificate** of full periodicity (three periods seen), but a rank < 3 is never a certificate of aperiodicity.\n" + }, + { + "cell_type": "markdown", + "id": "70b55fcb", + "metadata": { + "papermill": { + "duration": 0.001834, + "end_time": "2026-10-08T22:34:55.995489", + "exception": false, + "start_time": "2026-10-08T22:34:55.993655", + "status": "completed" + }, + "tags": [] + }, + "source": "## 4. What a finite window can establish — and what it cannot\n\nA finite window can **never** prove aperiodicity, for a simple reason: any finite tiling observed on W is compatible with a fully periodic tiling of Z^3 (repeat the motif of W). The §3 measurements carry this with numbers:\n\n- the **control** A itself yields rank 2 on a thin window — the half-window ceiling strikes even the simplest tiles;\n- the gapped domino (B1) and the doubled cube (B2) have **proven** minimal periods (4 in x for the former, exactly 4Z³ for the latter): their measured ranks 2 and 0 on small windows are **visibility artifacts**, lifted when the window doubles;\n- the L prism (B0) recalls the other edge of the spectrum: a local constraint can forbid **every** tiling of a box — there, the solver's failure is a proof, because it is short and structured (forced anchors), not an exhaustion.\n\nWhat the measurement therefore brings: **it calibrates** (the measured rank is a lower bound capped by the half-window), **it compares** (the backtracking node cost tells whether the local constraint bites), **it traps** (B2 shows that a measured rank 0 says nothing about the true group). What it does not replace: theorem 155, which establishes the absence of rank 3 for **all** tilings of its tile — a universal quantifier that no finite window reaches.\n\nThis is the division of labor of the ANALYSE series: the Python notebook **measures and illustrates**, the formalization **proves** — here, the Lean skeleton published by the corpus for family 155.\n" + }, + { + "cell_type": "markdown", + "id": "dabd9d12", + "metadata": { + "papermill": { + "duration": 0.00204, + "end_time": "2026-10-08T22:34:55.999367", + "exception": false, + "start_time": "2026-10-08T22:34:55.997327", + "status": "completed" + }, + "tags": [] + }, + "source": "## 5. Exercises\n\n### Exercise 1 — the period group, not just its rank\n\nThe `period_rank` function returns the rank and generators. Write `period_group(placement, window_shape)` returning the **complete list** of period vectors found (in canonical form), then check on the domino that the minimum-L1-norm periods are (1,0,0), (0,1,0) and (0,0,2) — and explain why the step is 2 and not 1 in the long direction.\n\n```python\n# TODO student\ndef period_group(placement, window_shape):\n # Hint: resume period_rank's probing loop and collect\n # ALL invariant nonzero vectors v, instead of stopping at a basis.\n # Step 1: list the candidates in the half-window.\n # Step 2: test invariance (vectorized anchor comparison).\n # Step 3: canonicalize each period and deduplicate.\n return None\n```\n\n### Exercise 2 — the smallest window that reveals the x generator\n\nFor the gapped domino, the minimal x-period is 4 (proven in §3.3). Find experimentally the smallest window (N₁,2,2) from which the generator (4,0,0) becomes **visible** in the measurement, and check that it is indeed N₁ = 8 (half-window 4). What happens for N₁ = 7?\n\n```python\n# TODO student\ndef plus_petite_fenetre_revelante(tile_cells, axe=0):\n # Hint: sweep increasing N1, call place_tiles then period_rank,\n # stop at the first rank 3. Watch the odd N1 case (half-window\n # floor): does the N1=7 answer surprise you given floor(7/2) = 3?\n return None\n```\n\n### Exercise 3 — build a parity constraint\n\nThe doubled cube owes its unique tiling to a **parity class** argument. Build another tile whose Z^3 tiling is unique by the same argument (for instance a \"doubled L\" — take the L's three cells, double every coordinate), prove uniqueness by hand, then check that the measurement yields rank 0 on a small window and rank 3 on a large one, with the expected generators.\n\n```python\n# TODO student\ndef triomino_dilate():\n # Hint: take the L's three cells, multiply every coordinate by 2,\n # and reason by parity class as in 3.4.\n # Step 1: propose the shape. Step 2: prove uniqueness by hand.\n # Step 3: measure on (4,4,4) then (8,8,8) and confront.\n return None\n```\n" + }, + { + "cell_type": "markdown", + "id": "51fdc696", + "metadata": { + "papermill": { + "duration": 0.004763, + "end_time": "2026-10-08T22:34:56.008744", + "exception": false, + "start_time": "2026-10-08T22:34:56.003981", + "status": "completed" + }, + "tags": [] + }, + "source": "## Conclusion\n\n### What has been established\n\n| Result | Measurement |\n|---|---|\n| The domino is fully periodic | rank 3 on (4,4,4), generators including (0,0,2) |\n| A thin window hides even obvious periods | rank 2 on (6,4,2) for that same domino |\n| The L prism tiles no aligned box | 0/3 windows solved, short structured failure (theorem) |\n| The gapped domino has a proven minimal x-period of 4 | rank 2 on (4,2,2) then 3 on (8,2,2), generator (4,0,0) |\n| The doubled cube has a unique tiling with group 4Z³ | rank 0 on (4,4,4) then 3 on (8,8,8) |\n| A finite window never proves aperiodicity | §4 argument: repeated motif |\n\n### What remains to the theorem\n\nStatement 155 — a finite tile of Z^3 that tiles with **no** rank-3 tiling — is not re-proven here: it is **presented**, sourced from the openai/math corpus (published Lean skeleton), and illustrated by measured toy cases that each honestly bound their reach. The natural bridge is twofold: the formalization on the Lean side (the corpus's skeleton), and the exact cover on the `sudoku_lean` side — the semantics is the same, only the instances change.\n\n**Leads for the sequel**: the passage to R^3 (unit-cube thickening, arbitrary real translations); the comparison with classical aperiodic tile sets (Berger 1966, Jeandel–Rao in 2D — a *family* of tiles, where 155 gives a *single* tile); and the algorithmic complexity of tiling (undecidability in general, Berger's result).\n" + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "name": "python", + "version": "3.13" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md index 9592327175..ee43461da2 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md @@ -150,6 +150,7 @@ Tous les notebooks incluent une **barre de navigation** en haut et en bas permet | ANALYSE-02 | [ANALYSE-02-Tao-Lean-Python](ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb) | Le manuel *Analysis I* de T. Tao en lac Lean 4 (`teorth/analysis`) : architecture du lac, philosophie d'auto-contenance vs Mathlib, cinq lemmes emblématiques parmi 44k LOC, méta-récit single-agent vs cluster distribué | 40 min | | ANALYSE-03 | [ANALYSE-03-PFR-Lean](ANALYSE/ANALYSE-03-PFR-Lean.ipynb) | La conjecture PFR (polynomial Freiman–Ruzsa, ZMod 2) : méthode entropique de la preuve `teorth/pfr` — énoncé combinatoire, illustrations cosets dans F₂³, `#check` réels et axiomes du lac compilé | 45 min | | ANALYSE-04 | [ANALYSE-04-PFR-Primitives-Python](ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb) | Trois primitives de PFR, et l'endroit exact où elles cessent de valoir — companion de digestion de ANALYSE-03 : ce qui se transporte hors du cadre d'origine (#12214) | 30 min | +| ANALYSE-09 | [ANALYSE-09-Tuilage-Aperiodique](ANALYSE/ANALYSE-09-Tuilage-Aperiodique.ipynb) (+ [jumeau _en](ANALYSE/ANALYSE-09-Tuilage-Aperiodique_en.ipynb)) | Contre-exemple au pavage périodique en dimension 3 (famille 155 du corpus openai/math) : un carreau fini de ℤ³ qui pave par translations sans **aucun** pavage totalement périodique — définitions (tuile, couverture exacte, rang du groupe de périodes), moteur borné exact-cover ancré sur la sémantique de `sudoku_lean`, quatre expériences mesurées dont deux pièges de fenêtre (rang mesuré 0 ou 2 pour des tuiles prouvées périodiques) et un théorème de non-pavage (prisme en L) | 30 min | | 21 | [Lean-21-MIMO-Detection-Flips](Lean-21-MIMO-Detection-Flips.ipynb) | Détection MIMO par flips de coordonnées (Papailiopoulos 2026) : le seuil 2·log N — descente simulée et comptage de flips, probabilité d'échappement du bruit (Monte-Carlo vs `e^{−np}`), `#check` réels des quatre phases et du converse complet `ml_error_prob_ge_threshold` (P(erreur ML) ≥ 1 − e^{−(2·log N − log log N)}) du companion `mimo_lean` (sorry-free, lake externe SLT pour Hanson–Wright) | 45 min | | 21b | [Lean-21b-MIMO-Converse-Native](Lean-21b-MIMO-Converse-Native.ipynb) | Compagnon **natif** (kernel `lean4-wsl`) du lac `mimo_lean` : le lac importé et exécuté dans un kernel Lean 4 réel — la frontière SLT exhibée par `#check` (ce qui est prouvé vs emprunté à `YuanheZ/lean-stat-learning-theory`), les six déclarations de `NormTails` (concentration de Lipschitz gaussienne), les seize briques du converse Hanson–Wright (dont `hanson_wright_noise` et la queue chi-carré `chisq_norm_concentration`), les treize du pont ML (`Bridge`), `#print axioms` sur les théorèmes clés — uniquement les axiomes standards, zéro `sorry` | 40 min | | 21c | [Lean-21c-Descente-Budget](Lean-21c-Descente-Budget.ipynb) | Le budget de descente : quand la décroissance borne le nombre de flips — l'analyse qui fonde le seuil 2·log N de la détection MIMO (#12219) | 35 min | @@ -504,6 +505,8 @@ Lean/ │ ├── ANALYSE-02-Tao-Lean-Python.ipynb # Analysis I de Tao en lac Lean 4 (teorth/analysis) : architecture, lemmes emblématiques │ ├── ANALYSE-03-PFR-Lean.ipynb # Conjecture PFR (teorth/pfr) : méthode entropique, cosets F₂³, #check réels │ ├── ANALYSE-04-PFR-Primitives-Python.ipynb # Les trois primitives de PFR et l'endroit où elles cessent de valoir (#12214) +│ ├── ANALYSE-09-Tuilage-Aperiodique.ipynb # Contre-exemple au pavage périodique 3D (openai/math 155) : exact-cover borne, rang des periodes +│ ├── ANALYSE-09-Tuilage-Aperiodique_en.ipynb # Jumeau EN (code byte-identique) │ └── README.md ├── Geometry/ # Sous-série géométrie formelle et automatisation des preuves (EPIC #18601) : Wu, Ritt, DD+AR, lac companion — [README](Geometry/README.md) │ ├── Geometry-01-From-Figure-To-Equation.ipynb diff --git a/_quarto.yml b/_quarto.yml index 6f57a3ce2f..801c4dc48b 100644 --- a/_quarto.yml +++ b/_quarto.yml @@ -1915,6 +1915,8 @@ project: - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-03-PFR-Lean.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb" + - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-09-Tuilage-Aperiodique.ipynb" + - "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-09-Tuilage-Aperiodique_en.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-01-From-Figure-To-Equation.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-02-From-Equation-To-Proof.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-03-Wu-Method-Python.ipynb"