Lean-12c : algèbre TPR — binding, unbinding et constituent surgery dans le noyau Lean

Série : SymbolicAI/Lean | Précédent : Lean-12b — Sensitivity natif | Suivant : Lean-13 — Kochen-Specker | Jumeau empirique : SL-13 — DISCOVER/TPR

Référence : R. Thomas McCoy, Paul Soulos, Tal Linzen, Paul Smolensky, The Emergent Symbolic Structure of Artificial Neural Networks, arXiv:2608.29530. Modèle TPR : Smolensky (1990).

Ce notebook est le companion formel du module Sensitivity/TensorProductRepresentation.lean du lake sensitivity_lean — grain G7 de l’EPIC #14366. Là où SL-13 mesure (sur des GRU CPU) dans quelle mesure des états cachés sont proches d’une représentation par produit tensoriel, ce notebook exhibe dans le kernel Lean l’algèbre exacte du modèle TPR : ce qui est vrai, sans erreur ni approximation, à l’intérieur du modèle — et l’ensemble des hypothèses sous lesquelles c’est vrai.

Objectifs d’apprentissage

À la fin de ce notebook, vous saurez :

  1. lire les définitions du modèle TPR (tprBind, tprSuperpos, tprUnbind) directement dans leurs types Lean ;
  2. expliquer pourquoi l’unbinding est exact sous l’hypothèse d’indépendance (orthonormalité) des rôles (RoleFamily) ;
  3. dérouler l’identité algébrique de la constituent surgery (remplacer un constituant, relire) ;
  4. distinguer les hypothèses (projection affine tprReadout, approximation TprApproxEntrywise) des théorèmes qui en dépendent ;
  5. délimiter la frontière épistémique : ce que le modèle prouve, ce qu’un réseau réel satisfait ou non, et ce que personne n’affirme ici.

Position dans la série

Lean-12c approfondit le palier Lean-12 : même lake (sensitivity_lean), même cérémonie d’interrogation du compilateur (#check, #print axioms) que Lean-12b — mais pour le versant TPR du lake, qui formalise McCoy et al. plutôt que Huang 2019. La lettre dit « ceci approfondit », et l’argument est le suivant : le lake sensitivity_lean porte désormais deux corpus (Huang + TPR), et le TPR est le pendant formel du diagnostic empirique de SL-13 — le refermer dans Lean-12b laisserait le module TPR invisible du parcours pédagogique.

Prérequis

  • Lean-12b — la cérémonie #check / #print axioms (kernel lean4-wsl) ;
  • recommandé : SL-13 pour le versant empirique (non requis) ;
  • algèbre linéaire de base : produit matrice-vecteur, produit scalaire.

Durée estimée : 35 minutes

Crédits : module TensorProductRepresentation.lean — grain G7 de l’EPIC #14366 (McCoy et al., arXiv:2608.29530) ; notebook compagnon exécuté sur kernel lean4-wsl.

1. Import du module

Le kernel lean4-wsl persiste l’environnement Lean d’une cellule à l’autre : tous les imports vivent dans la première cellule code, les suivantes n’utilisent que #check / #print axioms / #eval et des définitions. Le module s’appelle Sensitivity.TensorProductRepresentation (fichier Sensitivity/TensorProductRepresentation.lean du lake) et son espace de noms est Sensitivity.TPR.

L’import déclenche la résolution de la chaîne Mathlib du lake sensitivity_lean (toolchain v4.33.0, oleans pré-builds) : c’est la même mécanique que Lean-12b pour import Sensitivity. Le module importe ce dont l’algèbre a besoin (Matrix, gros opérateurs, tactiques) — rien de plus.

import Sensitivity.TensorProductRepresentation

import Sensitivity.TensorProductRepresentation
--% env 0
Raw input {"cmd": "import Sensitivity.TensorProductRepresentation\n"}
Raw output {"env": 0}

Contrôle positif — l’import a-t-il vraiment résolu ?

Le kernel peut rendre un environnement vide sans erreur visible si un import manque son olean : une cellule #check qui suit immédiatement l’import doit donc résoudre à la fois un nom du cœur de Lean et un nom du lake. Si les deux s’affichent, l’import a réellement chargé le module ; sinon, tout ce qui suit serait empoisonné. C’est le garde-fou standard de la série (introduit dans Lean-13c).

-- Contrôle positif : le cœur du kernel répond 4, et le nom du lake résolve.
#eval 2 + 2
#check @Sensitivity.TPR.tprBind
#check @Sensitivity.TPR.tprUnbind

-- Contrôle positif : le cœur du kernel répond 4, et le nom du lake résolve.
 4
 @Sensitivity.TPR.tprBind : {p q : ℕ} → (Fin p → ℝ) → (Fin q → ℝ) → Matrix (Fin p) (Fin q) ℝ
 @Sensitivity.TPR.tprUnbind : {p q : ℕ} → Matrix (Fin p) (Fin q) ℝ → (Fin q → ℝ) → Fin p → ℝ
--% env 1
Raw input {"cmd": "-- Contr\u00f4le positif : le c\u0153ur du kernel r\u00e9pond 4, et le nom du lake r\u00e9solve.\n#eval 2 + 2\n#check @Sensitivity.TPR.tprBind\n#check @Sensitivity.TPR.tprUnbind\n", "env": 0}
Raw output {"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 5}, "data": "4"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "@Sensitivity.TPR.tprBind : {p q : ℕ} → (Fin p → ℝ) → (Fin q → ℝ) → Matrix (Fin p) (Fin q) ℝ"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "@Sensitivity.TPR.tprUnbind : {p q : ℕ} → Matrix (Fin p) (Fin q) ℝ → (Fin q → ℝ) → Fin p → ℝ"}], "env": 1}

Lecture du résultat — deux définitions, deux types

Le contrôle a rendu 4 (le cœur du kernel est sain) et deux signatures du lake :

  • tprBind prend un filler f : Fin p → ℝ et un rôle r : Fin q → ℝ et rend une matrice Matrix (Fin p) (Fin q) ℝ — le produit tensoriel f ⊗ r, dont l’entrée (i, j) vaut f i * r j ;
  • tprUnbind prend une matrice T (un état TPR) et un rôle r, et rend un vecteur Fin p → ℝ — le produit matrice-vecteur T *ᵥ r, la « lecture » du filler au rôle r.

Le vocabulaire est celui de Smolensky : le filler porte le contenu (quel symbole), le rôle porte la fonction grammaticale (à quelle position). SL-13 mesure ces objets dans un GRU ; ici, ce sont les objets premiers du modèle, définis par leurs types.

2. Le vocabulaire complet du modèle — deux définitions, deux hypothèses

Le modèle a six pièces. Deux complètent le vocabulaire :

  • tprSuperpos fs rs : la superposition \(T = \sum_i f_i \otimes r_i\) — l’état TPR d’une séquence entière (une matrice p × q, somme des bindings) ;
  • RoleFamily rs : l’indépendance des rôles — la famille rs est orthonormale pour le produit scalaire canonique : \(r_i \cdot r_j = \delta_{ij}\). C’est la condition sous laquelle la lecture est exacte.

Et deux sont des hypothèses explicites, pas des théorèmes — le lake les étiquette comme telles :

  • tprReadout A b T r : l’hypothèse de projection affine — le décodeur lit un rôle de l’état puis applique la carte affine \(x \mapsto A \cdot x + b\). Le décodeur des réseaux étudiés par McCoy et al. est supposé affine ; c’est une hypothèse qu’un réseau satisfait ou non ;
  • TprApproxEntrywise S T ε : l’hypothèse d’approximation — l’état réel S (ce que le réseau fait réellement) est proche, entrée par entrée, d’une superposition TPR T : \(|S_{ij} - T_{ij}| \le \epsilon\).

La cellule suivante demande au compilateur les quatre types. Lisez-les comme le contrat du modèle : deux définitions non contraintes, deux propriétés qu’il faudra fournir pour conclure.

-- Les quatre pièces restantes du modèle : deux définitions, deux hypothèses.
#check @Sensitivity.TPR.tprSuperpos
#check @Sensitivity.TPR.RoleFamily
#check @Sensitivity.TPR.tprReadout
#check @Sensitivity.TPR.TprApproxEntrywise

-- Les quatre pièces restantes du modèle : deux définitions, deux hypothèses.
 @Sensitivity.TPR.tprSuperpos : {p q m : ℕ} → (Fin m → Fin p → ℝ) → (Fin m → Fin q → ℝ) → Matrix (Fin p) (Fin q) ℝ
 @Sensitivity.TPR.RoleFamily : {q m : ℕ} → (Fin m → Fin q → ℝ) → Prop
 @Sensitivity.TPR.tprReadout : {p q k : ℕ} →
  Matrix (Fin k) (Fin p) ℝ → (Fin k → ℝ) → Matrix (Fin p) (Fin q) ℝ → (Fin q → ℝ) → Fin k → ℝ
 @Sensitivity.TPR.TprApproxEntrywise : {p q : ℕ} → Matrix (Fin p) (Fin q) ℝ → Matrix (Fin p) (Fin q) ℝ → ℝ → Prop
--% env 2
Raw input {"cmd": "-- Les quatre pi\u00e8ces restantes du mod\u00e8le : deux d\u00e9finitions, deux hypoth\u00e8ses.\n#check @Sensitivity.TPR.tprSuperpos\n#check @Sensitivity.TPR.RoleFamily\n#check @Sensitivity.TPR.tprReadout\n#check @Sensitivity.TPR.TprApproxEntrywise\n", "env": 1}
Raw output {"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "@Sensitivity.TPR.tprSuperpos : {p q m : ℕ} → (Fin m → Fin p → ℝ) → (Fin m → Fin q → ℝ) → Matrix (Fin p) (Fin q) ℝ"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "@Sensitivity.TPR.RoleFamily : {q m : ℕ} → (Fin m → Fin q → ℝ) → Prop"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "@Sensitivity.TPR.tprReadout : {p q k : ℕ} →\n Matrix (Fin k) (Fin p) ℝ → (Fin k → ℝ) → Matrix (Fin p) (Fin q) ℝ → (Fin q → ℝ) → Fin k → ℝ"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "@Sensitivity.TPR.TprApproxEntrywise : {p q : ℕ} → Matrix (Fin p) (Fin q) ℝ → Matrix (Fin p) (Fin q) ℝ → ℝ → Prop"}], "env": 2}

Lecture du résultat — le contrat du modèle

Pièce Type rendu par le kernel Statut
tprSuperpos une matrice p × q, somme des bindings définition
RoleFamily une Prop : \(r_i \cdot r_j = 1\) si \(i = j\), \(0\) sinon hypothèse d’indépendance
tprReadout un vecteur Fin k → ℝ : A *ᵥ (tprUnbind T r) + b hypothèse de décodeur affine
TprApproxEntrywise une Prop : \(\forall i\, j,\ |S_{ij} - T_{ij}| \le \epsilon\) hypothèse d’approximation

Points clés :

  1. RoleFamily n’est pas prouvé pour une famille quelconque : des rôles presque colinéaires violent l’hypothèse, et l’unbinding devient alors approximatif — c’est exactement la marge que la thèse « limitiviste » de McCoy et al. exploite (structure approchée).
  2. tprReadout parle du décodeur, pas du modèle TPR : dire qu’un réseau réel a un décodeur affine est une affirmation empirique, jamais un théorème d’algèbre.
  3. TprApproxEntrywise est le pont entre le réseau réel (S) et le modèle (T) : tout ce que le lake conclura sur un réseau passera par cette hypothèse.

3. Exemple guidé 1 — l’unbinding est exact sous indépendance des rôles

L’énoncé mathématique. Si les rôles \(r_0, \dots, r_{m-1}\) sont orthonormaux et si \(T = \sum_i f_i \otimes r_i\), alors la lecture au rôle \(r_j\) rend exactement le filler \(f_j\) :

\[T \cdot r_j = \sum_i f_i \, (r_i \cdot r_j) = f_j.\]

Pourquoi c’est vrai. Le produit matrice-vecteur se distribue sur la somme (tprUnbind_sum), et sur un binding isolé la lecture vaut \(f \, (r \cdot r')\) (tprUnbind_bind) : chaque terme $ i j$ est tué par \(r_i \cdot r_j = 0\), et le terme \(i = j\) survit avec \(r_j \cdot r_j = 1\). L’hypothèse RoleFamily est utilisée deux fois, exactement pour ces deux tueries — sans elle, rien ne tient.

Hypothèses explicites : h : RoleFamily rs (indépendance) et j : Fin m (le constituant lu). Aucune autre.

-- Les deux briques de linéarité, puis le théorème d'unbinding exact.
#check @Sensitivity.TPR.tprUnbind_bind
#check @Sensitivity.TPR.tprUnbind_sum
#check @Sensitivity.TPR.tprUnbind_superpos
#print axioms Sensitivity.TPR.tprUnbind_superpos

-- Les deux briques de linéarité, puis le théorème d'unbinding exact.
 @Sensitivity.TPR.tprUnbind_bind : ∀ {p q : ℕ} (f : Fin p → ℝ) (r r' : Fin q → ℝ),
  Sensitivity.TPR.tprUnbind (Sensitivity.TPR.tprBind f r) r' = fun κ => f κ * r ⬝ᵥ r'
 @Sensitivity.TPR.tprUnbind_sum : ∀ {p q m : ℕ} (Ts : Fin m → Matrix (Fin p) (Fin q) ℝ) (r : Fin q → ℝ),
  Sensitivity.TPR.tprUnbind (∑ i, Ts i) r = ∑ i, Sensitivity.TPR.tprUnbind (Ts i) r
 @Sensitivity.TPR.tprUnbind_superpos : ∀ {p q m : ℕ} {fs : Fin m → Fin p → ℝ} {rs : Fin m → Fin q → ℝ},
  Sensitivity.TPR.RoleFamily rs →
    ∀ (j : Fin m), Sensitivity.TPR.tprUnbind (Sensitivity.TPR.tprSuperpos fs rs) (rs j) = fs j
 'Sensitivity.TPR.tprUnbind_superpos' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 3
Raw input {"cmd": "-- Les deux briques de lin\u00e9arit\u00e9, puis le th\u00e9or\u00e8me d'unbinding exact.\n#check @Sensitivity.TPR.tprUnbind_bind\n#check @Sensitivity.TPR.tprUnbind_sum\n#check @Sensitivity.TPR.tprUnbind_superpos\n#print axioms Sensitivity.TPR.tprUnbind_superpos\n", "env": 2}
Raw output {"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "@Sensitivity.TPR.tprUnbind_bind : ∀ {p q : ℕ} (f : Fin p → ℝ) (r r' : Fin q → ℝ),\n Sensitivity.TPR.tprUnbind (Sensitivity.TPR.tprBind f r) r' = fun κ => f κ * r ⬝ᵥ r'"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "@Sensitivity.TPR.tprUnbind_sum : ∀ {p q m : ℕ} (Ts : Fin m → Matrix (Fin p) (Fin q) ℝ) (r : Fin q → ℝ),\n Sensitivity.TPR.tprUnbind (∑ i, Ts i) r = ∑ i, Sensitivity.TPR.tprUnbind (Ts i) r"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "@Sensitivity.TPR.tprUnbind_superpos : ∀ {p q m : ℕ} {fs : Fin m → Fin p → ℝ} {rs : Fin m → Fin q → ℝ},\n Sensitivity.TPR.RoleFamily rs →\n ∀ (j : Fin m), Sensitivity.TPR.tprUnbind (Sensitivity.TPR.tprSuperpos fs rs) (rs j) = fs j"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "'Sensitivity.TPR.tprUnbind_superpos' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 3}

Lecture du résultat — une égalité exacte, des axiomes standards

La signature de tprUnbind_superpos se lit : pour toute famille de fillers fs, toute famille de rôles rs vérifiant RoleFamily rs, et tout indice j, la lecture de la superposition au rôle rs j égale le filler fs j — l’égalité est exacte (pas une borne, pas un ε).

Le #print axioms rend l’empreinte standard [propext, Classical.choice, Quot.sound] : les trois axiomes du cœur de Lean 4, et aucun sorryAx — la preuve est close. C’est le même certificat que pour huang_degree_theorem dans Lean-12b : la commande audite récursivement la chaîne de preuves, un sorry caché dans un lemme distant y serait visible.

4. Exemple guidé 2 — constituent surgery : l’identité centrale

L’intervention de McCoy et al. La constituent surgery remplace, dans l’état, le binding d’un constituant : on retranche \(f_j \otimes r_j\), on ajoute \(f' \otimes r_j\), puis on relit au rôle \(r_j\) :

\[(T - f_j \otimes r_j + f' \otimes r_j) \cdot r_j = f'.\]

Pourquoi c’est vrai. Par linéarité (tprUnbind_add, tprUnbind_sub), la lecture se répartit sur les trois termes ; le premier donne \(f_j\) par le théorème 1, qui s’annule avec le binding retranché, et il reste \(f' \, (r_j \cdot r_j) = f'\). Les autres constituants ne contribuent pas : chacun est tué par l’orthonormalité, comme au théorème 1.

Hypothèses explicites : h : RoleFamily rs, l’indice j du constituant remplacé, et le nouveau filler f'. Rien d’autre — c’est une identité du modèle, et McCoy et al. l’utilisent comme prédiction testable : si un réseau implémente (approximativement) ce modèle, l’intervention doit transférer (approximativement). SL-13 mesure ce transfert sur un GRU ; le lake, lui, prouve l’identité exacte que l’approximation vise.

-- Les briques additives de la chirurgie, puis l'identité centrale.
#check @Sensitivity.TPR.tprUnbind_sub
#check @Sensitivity.TPR.tprUnbind_add
#check @Sensitivity.TPR.tprSurgery
#print axioms Sensitivity.TPR.tprSurgery

-- Les briques additives de la chirurgie, puis l'identité centrale.
 @Sensitivity.TPR.tprUnbind_sub : ∀ {p q : ℕ} (T T' : Matrix (Fin p) (Fin q) ℝ) (r : Fin q → ℝ),
  Sensitivity.TPR.tprUnbind (T - T') r = Sensitivity.TPR.tprUnbind T r - Sensitivity.TPR.tprUnbind T' r
 @Sensitivity.TPR.tprUnbind_add : ∀ {p q : ℕ} (T T' : Matrix (Fin p) (Fin q) ℝ) (r : Fin q → ℝ),
  Sensitivity.TPR.tprUnbind (T + T') r = Sensitivity.TPR.tprUnbind T r + Sensitivity.TPR.tprUnbind T' r
 @Sensitivity.TPR.tprSurgery : ∀ {p q m : ℕ} {fs : Fin m → Fin p → ℝ} {rs : Fin m → Fin q → ℝ},
  Sensitivity.TPR.RoleFamily rs →
    ∀ (j : Fin m) (f' : Fin p → ℝ),
      Sensitivity.TPR.tprUnbind
          (Sensitivity.TPR.tprSuperpos fs rs - Sensitivity.TPR.tprBind (fs j) (rs j) +
            Sensitivity.TPR.tprBind f' (rs j))
          (rs j) =
        f'
 'Sensitivity.TPR.tprSurgery' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 4
Raw input {"cmd": "-- Les briques additives de la chirurgie, puis l'identit\u00e9 centrale.\n#check @Sensitivity.TPR.tprUnbind_sub\n#check @Sensitivity.TPR.tprUnbind_add\n#check @Sensitivity.TPR.tprSurgery\n#print axioms Sensitivity.TPR.tprSurgery\n", "env": 3}
Raw output {"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "@Sensitivity.TPR.tprUnbind_sub : ∀ {p q : ℕ} (T T' : Matrix (Fin p) (Fin q) ℝ) (r : Fin q → ℝ),\n Sensitivity.TPR.tprUnbind (T - T') r = Sensitivity.TPR.tprUnbind T r - Sensitivity.TPR.tprUnbind T' r"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "@Sensitivity.TPR.tprUnbind_add : ∀ {p q : ℕ} (T T' : Matrix (Fin p) (Fin q) ℝ) (r : Fin q → ℝ),\n Sensitivity.TPR.tprUnbind (T + T') r = Sensitivity.TPR.tprUnbind T r + Sensitivity.TPR.tprUnbind T' r"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "@Sensitivity.TPR.tprSurgery : ∀ {p q m : ℕ} {fs : Fin m → Fin p → ℝ} {rs : Fin m → Fin q → ℝ},\n Sensitivity.TPR.RoleFamily rs →\n ∀ (j : Fin m) (f' : Fin p → ℝ),\n Sensitivity.TPR.tprUnbind\n (Sensitivity.TPR.tprSuperpos fs rs - Sensitivity.TPR.tprBind (fs j) (rs j) +\n Sensitivity.TPR.tprBind f' (rs j))\n (rs j) =\n f'"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "'Sensitivity.TPR.tprSurgery' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 4}

Lecture du résultat — remplacer un constituant ne déplace que sa lecture

Le type de tprSurgery est l’égalité complète : tprUnbind (tprSuperpos fs rs - tprBind (fs j) (rs j) + tprBind f' (rs j)) (rs j) = f'. L’état chirurgical relit exactement le filler de remplacement — et, par le théorème 1, la lecture aux autres rôles est inchangée (chaque autre constituant garde son binding et son rôle orthogonal). C’est la forme algébrique de « la chirurgie d’un constituant change la lecture de ce constituant et d’aucun autre ».

Le #print axioms rend à nouveau [propext, Classical.choice, Quot.sound], sans sorryAx : l’identité est prouvée, pas conjecturée. Ce qu’un réseau réel approche de cette identité est une question empirique — mesurée dans SL-13, jamais affirmée par le lake.

5. Exemple guidé 3 — projection affine : ce que voit le décodeur

L’hypothèse de décodeur. McCoy et al. supposent le décodeur affine : la sortie est tprReadout A b T r = A *ᵥ (T *ᵥ r) + b. Le lake encode ce choix comme une définition paramétrée par A et b — le statut d’hypothèse vit dans la prose du module et dans l’usage : rien ne prouve qu’un réseau particulier a un décodeur affine.

Le théorème. Sous RoleFamily (et pour un décodeur affine quelconque), la sortie de l’état chirurgical au rôle j diffère de la sortie originale par exactement \(A \cdot (f' - f_j)\) :

\[\mathrm{readout}(T') = \mathrm{readout}(T) + A \cdot (f' - f_j).\]

Le terme de différence ne dépend que du constituant remplacé — ni des autres fillers, ni des autres rôles, ni du biais b (qui s’annule dans la différence). C’est ce qui rend l’intervention chirurgicale : localisée sur un constituant, prévisible dans son effet sur la sortie.

-- Le décodeur affine, puis l'identité de chirurgie vue par ce décodeur.
#check @Sensitivity.TPR.tprReadout
#check @Sensitivity.TPR.tprSurgery_readout
#print axioms Sensitivity.TPR.tprSurgery_readout

-- Le décodeur affine, puis l'identité de chirurgie vue par ce décodeur.
 @Sensitivity.TPR.tprReadout : {p q k : ℕ} →
  Matrix (Fin k) (Fin p) ℝ → (Fin k → ℝ) → Matrix (Fin p) (Fin q) ℝ → (Fin q → ℝ) → Fin k → ℝ
 @Sensitivity.TPR.tprSurgery_readout : ∀ {p q k m : ℕ} {fs : Fin m → Fin p → ℝ} {rs : Fin m → Fin q → ℝ},
  Sensitivity.TPR.RoleFamily rs →
    ∀ (j : Fin m) (f' : Fin p → ℝ) (A : Matrix (Fin k) (Fin p) ℝ) (b : Fin k → ℝ),
      Sensitivity.TPR.tprReadout A b
          (Sensitivity.TPR.tprSuperpos fs rs - Sensitivity.TPR.tprBind (fs j) (rs j) +
            Sensitivity.TPR.tprBind f' (rs j))
          (rs j) =
        Sensitivity.TPR.tprReadout A b (Sensitivity.TPR.tprSuperpos fs rs) (rs j) + A.mulVec (f' - fs j)
 'Sensitivity.TPR.tprSurgery_readout' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 5
Raw input {"cmd": "-- Le d\u00e9codeur affine, puis l'identit\u00e9 de chirurgie vue par ce d\u00e9codeur.\n#check @Sensitivity.TPR.tprReadout\n#check @Sensitivity.TPR.tprSurgery_readout\n#print axioms Sensitivity.TPR.tprSurgery_readout\n", "env": 4}
Raw output {"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "@Sensitivity.TPR.tprReadout : {p q k : ℕ} →\n Matrix (Fin k) (Fin p) ℝ → (Fin k → ℝ) → Matrix (Fin p) (Fin q) ℝ → (Fin q → ℝ) → Fin k → ℝ"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "@Sensitivity.TPR.tprSurgery_readout : ∀ {p q k m : ℕ} {fs : Fin m → Fin p → ℝ} {rs : Fin m → Fin q → ℝ},\n Sensitivity.TPR.RoleFamily rs →\n ∀ (j : Fin m) (f' : Fin p → ℝ) (A : Matrix (Fin k) (Fin p) ℝ) (b : Fin k → ℝ),\n Sensitivity.TPR.tprReadout A b\n (Sensitivity.TPR.tprSuperpos fs rs - Sensitivity.TPR.tprBind (fs j) (rs j) +\n Sensitivity.TPR.tprBind f' (rs j))\n (rs j) =\n Sensitivity.TPR.tprReadout A b (Sensitivity.TPR.tprSuperpos fs rs) (rs j) + A.mulVec (f' - fs j)"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "'Sensitivity.TPR.tprSurgery_readout' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 5}

Lecture du résultat — une différence qui isole le constituant remplacé

Le type de tprSurgery_readout se lit : sortie chirurgicale = sortie originale + A.mulVec (f' - fs j) — la forme exacte que rend le kernel ; c’est la même opération que la notation A *ᵥ (f' - fs j) du source du module. Deux conséquences immédiates, lisibles dans la seule forme du terme :

  1. localité : la différence ignore tout sauf f', fs j et A — si f' = fs j (remplacement par le même filler), les sorties coïncident exactement ;
  2. linéarité en A : l’effet de la chirurgie sur la sortie est proportionnel à la sensibilité du décodeur au filler du rôle j.

L’empreinte #print axioms reste [propext, Classical.choice, Quot.sound] — preuve close. Et la frontière reste intacte : le théorème est conditionnel au décodeur affine ; un décodeur non affine (réel) n’hérite de l’identité que par approximation — encore l’hypothèse, jamais la conclusion.

6. Exemple guidé 4 — stabilité de la lecture sous approximation

Le pont vers les réseaux réels. Un réseau ne produit jamais exactement une superposition TPR ; il produit un état S. L’hypothèse TprApproxEntrywise S T ε dit que S est à ε par entrée d’une superposition T. Le théorème suivant rend cette hypothèse opérationnelle : il quantifie ce qu’on peut en conclure.

L’énoncé. Si S est ε-proche de T entrée par entrée, alors pour tout rôle r et tout indice de filler κ :

\[|(S \cdot r)_κ - (T \cdot r)_κ| \le \epsilon \cdot \sum_j |r_j|.\]

Pourquoi c’est vrai. Chaque entrée de la lecture est une somme \(\sum_j S_{κj} r_j\) ; l’écart terme à terme est borné par \(\epsilon |r_j|\) (hypothèse), et l’inégalité triangulaire discrète (Finset.abs_sum_le_sum_abs) agrège ces bornes. La preuve du module déroule exactement ce calcul.

Ce que le théorème ne dit pas : il ne dit pas qu’un réseau satisfait l’hypothèse — il dit ce qu’on peut conclure s’il la satisfait, et rien sinon.

-- L'hypothèse d'approximation, puis la borne qu'elle déclenche.
#check @Sensitivity.TPR.TprApproxEntrywise
#check @Sensitivity.TPR.tprUnbind_approx
#print axioms Sensitivity.TPR.tprUnbind_approx

-- L'hypothèse d'approximation, puis la borne qu'elle déclenche.
 @Sensitivity.TPR.TprApproxEntrywise : {p q : ℕ} → Matrix (Fin p) (Fin q) ℝ → Matrix (Fin p) (Fin q) ℝ → ℝ → Prop
 @Sensitivity.TPR.tprUnbind_approx : ∀ {p q : ℕ} (S T : Matrix (Fin p) (Fin q) ℝ) (r : Fin q → ℝ) (ε : ℝ),
  Sensitivity.TPR.TprApproxEntrywise S T ε →
    ∀ (κ : Fin p), |Sensitivity.TPR.tprUnbind S r κ - Sensitivity.TPR.tprUnbind T r κ| ≤ ε * ∑ j, |r j|
 'Sensitivity.TPR.tprUnbind_approx' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 6
Raw input {"cmd": "-- L'hypoth\u00e8se d'approximation, puis la borne qu'elle d\u00e9clenche.\n#check @Sensitivity.TPR.TprApproxEntrywise\n#check @Sensitivity.TPR.tprUnbind_approx\n#print axioms Sensitivity.TPR.tprUnbind_approx\n", "env": 5}
Raw output {"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "@Sensitivity.TPR.TprApproxEntrywise : {p q : ℕ} → Matrix (Fin p) (Fin q) ℝ → Matrix (Fin p) (Fin q) ℝ → ℝ → Prop"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "@Sensitivity.TPR.tprUnbind_approx : ∀ {p q : ℕ} (S T : Matrix (Fin p) (Fin q) ℝ) (r : Fin q → ℝ) (ε : ℝ),\n Sensitivity.TPR.TprApproxEntrywise S T ε →\n ∀ (κ : Fin p), |Sensitivity.TPR.tprUnbind S r κ - Sensitivity.TPR.tprUnbind T r κ| ≤ ε * ∑ j, |r j|"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "'Sensitivity.TPR.tprUnbind_approx' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 6}

Lecture du résultat — l’erreur de lecture est bornée par la masse du rôle

La borne rendue par le kernel est ε * ∑ j, |r j| : l’erreur d’état est amplifiée par la masse \(\ell_1\) du rôle de lecture. Trois lectures :

  1. un rôle « économique » (\(\sum |r_j|\) petit, typiquement un vecteur de base) transmet fidèlement un état approximativement TPR ;
  2. un rôle « étalé » amplifie l’écart — pour un rôle normalisé en \(\ell_2\) mais dense, la masse \(\ell_1\) peut atteindre \(\sqrt{q}\) : la dégradation croît avec la dimension de rôle ;
  3. à ε = 0, l’hypothèse d’approximation impose S = T entrée par entrée, donc les lectures coïncident. Si T est en outre une superposition de rôles RoleFamily, le théorème 1 permet alors d’identifier cette lecture au filler correspondant. La borne de stabilité n’établit pas à elle seule l’unbinding exact.

#print axioms rend [propext, Classical.choice, Quot.sound], sans sorryAx : la borne est prouvée pour tout état, tout rôle, tout ε vérifiant l’hypothèse.

7. La frontière épistémique — ce qui est prouvé, ce qui est hypothèse, ce qui n’est pas affirmé

Le module TensorProductRepresentation.lean porte son propre avertissement, que ce notebook reprend intégralement :

Catégorie Contenu Statut
Prouvé dans le modèle unbinding exact (tprUnbind_superpos), identité de chirurgie (tprSurgery), chirurgie vue par un décodeur affine (tprSurgery_readout), borne de stabilité (tprUnbind_approx) théorèmes Lean, 0 sorry, axiomes standards
Hypothèses qu’un réseau satisfait ou non indépendance des rôles (RoleFamily), décodeur affine (tprReadout), état approchant une TPR (TprApproxEntrywise) jamais prouvées pour un réseau — inputs conditionnels des théorèmes
Jamais formalisé ici « GPT-OSS utilise ces rôles », « le réseau calcule un produit tensoriel » assertion empirique, hors scope du lake

C’est la traduction formelle de la thèse limitiviste de McCoy et al. : la structure symbolique émergerait comme approchée. SL-13 mesure de quelle approximation il s’agit (factorisation, réinjection, chirurgie, contrôles de capacité) sur des GRU CPU ; le lake, lui, établit le socle algébrique exact au-dessus duquel ces mesures s’interprètent. Les deux notebooks sont les deux moitiés d’une même affirmation : le modèle est exact, le réseau est approché — et c’est la distance entre les deux qui est l’objet scientifique.

8. Exercices

Les trois exercices suivent la convention de la série (cf. Lean-13c) : des certificats entiers à calculer à la main — le modèle du lake vit sur \(\mathbb{R}\) (non calculable dans le kernel), les exercices calculent ses instances exactes sur Int, et le #check final rappelle le théorème du lake qui certifie la généralité sur \(\mathbb{R}\). Les stubs ne contiennent aucune erreur volontaire : le notebook s’exécute de bout en bout, les #eval rendent la valeur du stub (0) tant que l’exercice n’est pas complété.

Données communes aux exercices 2 et 3 — deux rôles orthonormaux et deux fillers de \(\mathbb{Z}^2\) :

\[r_0 = (1, 0),\quad r_1 = (0, 1),\qquad f_0 = (2, 3),\quad f_1 = (5, 7).\]

Exercice 1 — l’entrée d’un binding de vecteurs de base

Contexte. tprBind f r est la matrice des produits f i * r j. Pour les vecteurs de base \(e_0 = (1,0)\) et \(e_1 = (0,1)\) de \(\mathbb{Z}^2\), le binding \(e_0 \otimes e_1\) est une matrice \(2 \times 2\) à coefficients entiers — à vous d’en déterminer le profil.

Objectif. Compléter entreeBindBase pour qu’elle rende l’entrée \((a, b)\) de \(e_0 \otimes e_1\).

  • Etape 1 : écrire les quatre entrées du produit extérieur \(e_0 \otimes e_1\) à la main — chaque entrée est le produit d’une coordonnée de \(e_0\) par une coordonnée de \(e_1\).
  • Etape 2 : coder le tableau obtenu par un if ... then ... else ... sur les indices.

La comparaison d’indices est calculable (Fin 2 a une égalité décidable) : #eval réduit l’expression sans définition supplémentaire.

-- Exercice 1 : certificat entier de l'entrée (a, b) du binding e_0 (X) e_1,
-- avec e_0 = (1, 0) et e_1 = (0, 1) les vecteurs de base de Z^2.
-- TODO etudiant : remplacer le corps ci-dessous
-- Etape 1 : écrire les quatre entrées du produit extérieur e_0 (X) e_1
-- Etape 2 : coder le tableau par un if ... then ... else ... sur les indices
def entreeBindBase (a b : Fin 2) : Int :=
  0

-- Contrôle : trois des quatre entrées de la matrice (à interpréter vous-même).
#eval entreeBindBase 0 1
#eval entreeBindBase 0 0
#eval entreeBindBase 1 1
-- Le lemme du lake qui généralise cette algèbre à des fillers/rôles quelconques sur ℝ.
#check @Sensitivity.TPR.tprUnbind_bind

-- Exercice 1 : certificat entier de l'entrée (a, b) du binding e_0 (X) e_1,
-- avec e_0 = (1, 0) et e_1 = (0, 1) les vecteurs de base de Z^2.
-- TODO etudiant : remplacer le corps ci-dessous
-- Etape 1 : écrire les quatre entrées du produit extérieur e_0 (X) e_1
-- Etape 2 : coder le tableau par un if ... then ... else ... sur les indices
🟨 Variable name `a` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _a

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `b` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _b

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  0
-- Contrôle : trois des quatre entrées de la matrice (à interpréter vous-même).
 0
 0
 0
-- Le lemme du lake qui généralise cette algèbre à des fillers/rôles quelconques sur ℝ.
 @Sensitivity.TPR.tprUnbind_bind : ∀ {p q : ℕ} (f : Fin p → ℝ) (r r' : Fin q → ℝ),
  Sensitivity.TPR.tprUnbind (Sensitivity.TPR.tprBind f r) r' = fun κ => f κ * r ⬝ᵥ r'
--% env 7
Raw input {"cmd": "-- Exercice 1 : certificat entier de l'entr\u00e9e (a, b) du binding e_0 (X) e_1,\n-- avec e_0 = (1, 0) et e_1 = (0, 1) les vecteurs de base de Z^2.\n-- TODO etudiant : remplacer le corps ci-dessous\n-- Etape 1 : \u00e9crire les quatre entr\u00e9es du produit ext\u00e9rieur e_0 (X) e_1\n-- Etape 2 : coder le tableau par un if ... then ... else ... sur les indices\ndef entreeBindBase (a b : Fin 2) : Int :=\n 0\n\n-- Contr\u00f4le : trois des quatre entr\u00e9es de la matrice (\u00e0 interpr\u00e9ter vous-m\u00eame).\n#eval entreeBindBase 0 1\n#eval entreeBindBase 0 0\n#eval entreeBindBase 1 1\n-- Le lemme du lake qui g\u00e9n\u00e9ralise cette alg\u00e8bre \u00e0 des fillers/r\u00f4les quelconques sur \u211d.\n#check @Sensitivity.TPR.tprUnbind_bind\n", "env": 6}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 6, "column": 20}, "endPos": {"line": 6, "column": 21}, "data": "Variable name `a` is not explicitly referenced.\n\nHint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:\n [apply] _a\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 6, "column": 22}, "endPos": {"line": 6, "column": 23}, "data": "Variable name `b` is not explicitly referenced.\n\nHint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:\n [apply] _b\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 14, "column": 0}, "endPos": {"line": 14, "column": 6}, "data": "@Sensitivity.TPR.tprUnbind_bind : ∀ {p q : ℕ} (f : Fin p → ℝ) (r r' : Fin q → ℝ),\n Sensitivity.TPR.tprUnbind (Sensitivity.TPR.tprBind f r) r' = fun κ => f κ * r ⬝ᵥ r'"}], "env": 7}

Exercice 2 — lire une superposition à rôles orthonormaux

Contexte. Avec les données communes, la superposition vaut \(T = f_0 \otimes r_0 + f_1 \otimes r_1\) — matrice \(2 \times 2\) dont la ligne a est l’indice de filler et la colonne b l’indice de rôle.

Objectif. Compléter lectureSuperposition pour qu’elle rende l’entrée a du vecteur lu au rôle j (c’est-à-dire (T *ᵥ r_j)(a)).

  • Etape 1 : former T à la main (deux bindings à superposer, entrée par entrée).
  • Etape 2 : effectuer le produit matrice-vecteur par \(r_j\) — que survit-il quand les rôles sont orthonormaux ?
  • Indice : le théorème 1 (section 3) prédit la forme du résultat ; appliquez-le aux données communes pour en déduire les valeurs.

Les quatre #eval couvrent les deux rôles × les deux entrées : chacun doit coïncider avec la prédiction du théorème 1 sur les données communes.

-- Exercice 2 : certificat entier de la lecture (T *v r_j)(a) pour la superposition
-- T = f_0 (X) r_0 + f_1 (X) r_1, avec r_0 = (1,0), r_1 = (0,1), f_0 = (2,3), f_1 = (5,7).
-- TODO etudiant : remplacer le corps ci-dessous
-- Etape 1 : former T (ligne a = filler, colonne b = rôle)
-- Etape 2 : effectuer le produit T *v r_j et rendre son entrée a
-- Indice : que prédit le théorème 1 (tprUnbind_superpos) pour cette lecture ?
def lectureSuperposition (j a : Fin 2) : Int :=
  0

-- Contrôle : les deux rôles × les deux entrées.
#eval lectureSuperposition 0 0
#eval lectureSuperposition 0 1
#eval lectureSuperposition 1 0
#eval lectureSuperposition 1 1
-- Le théorème du lake qui certifie cette lecture exacte sur ℝ.
#check @Sensitivity.TPR.tprUnbind_superpos

-- Exercice 2 : certificat entier de la lecture (T *v r_j)(a) pour la superposition
-- T = f_0 (X) r_0 + f_1 (X) r_1, avec r_0 = (1,0), r_1 = (0,1), f_0 = (2,3), f_1 = (5,7).
-- TODO etudiant : remplacer le corps ci-dessous
-- Etape 1 : former T (ligne a = filler, colonne b = rôle)
-- Etape 2 : effectuer le produit T *v r_j et rendre son entrée a
-- Indice : que prédit le théorème 1 (tprUnbind_superpos) pour cette lecture ?
🟨 Variable name `j` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _j

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `a` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _a

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  0
-- Contrôle : les deux rôles × les deux entrées.
 0
 0
 0
 0
-- Le théorème du lake qui certifie cette lecture exacte sur ℝ.
 @Sensitivity.TPR.tprUnbind_superpos : ∀ {p q m : ℕ} {fs : Fin m → Fin p → ℝ} {rs : Fin m → Fin q → ℝ},
  Sensitivity.TPR.RoleFamily rs →
    ∀ (j : Fin m), Sensitivity.TPR.tprUnbind (Sensitivity.TPR.tprSuperpos fs rs) (rs j) = fs j
--% env 8
Raw input {"cmd": "-- Exercice 2 : certificat entier de la lecture (T *v r_j)(a) pour la superposition\n-- T = f_0 (X) r_0 + f_1 (X) r_1, avec r_0 = (1,0), r_1 = (0,1), f_0 = (2,3), f_1 = (5,7).\n-- TODO etudiant : remplacer le corps ci-dessous\n-- Etape 1 : former T (ligne a = filler, colonne b = r\u00f4le)\n-- Etape 2 : effectuer le produit T *v r_j et rendre son entr\u00e9e a\n-- Indice : que pr\u00e9dit le th\u00e9or\u00e8me 1 (tprUnbind_superpos) pour cette lecture ?\ndef lectureSuperposition (j a : Fin 2) : Int :=\n 0\n\n-- Contr\u00f4le : les deux r\u00f4les \u00d7 les deux entr\u00e9es.\n#eval lectureSuperposition 0 0\n#eval lectureSuperposition 0 1\n#eval lectureSuperposition 1 0\n#eval lectureSuperposition 1 1\n-- Le th\u00e9or\u00e8me du lake qui certifie cette lecture exacte sur \u211d.\n#check @Sensitivity.TPR.tprUnbind_superpos\n", "env": 7}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 7, "column": 26}, "endPos": {"line": 7, "column": 27}, "data": "Variable name `j` is not explicitly referenced.\n\nHint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:\n [apply] _j\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 7, "column": 28}, "endPos": {"line": 7, "column": 29}, "data": "Variable name `a` is not explicitly referenced.\n\nHint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:\n [apply] _a\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 13, "column": 0}, "endPos": {"line": 13, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 14, "column": 0}, "endPos": {"line": 14, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 16, "column": 0}, "endPos": {"line": 16, "column": 6}, "data": "@Sensitivity.TPR.tprUnbind_superpos : ∀ {p q m : ℕ} {fs : Fin m → Fin p → ℝ} {rs : Fin m → Fin q → ℝ},\n Sensitivity.TPR.RoleFamily rs →\n ∀ (j : Fin m), Sensitivity.TPR.tprUnbind (Sensitivity.TPR.tprSuperpos fs rs) (rs j) = fs j"}], "env": 8}

Exercice 3 — relire après constituent surgery

Contexte. On opère la chirurgie du constituant 0 : on remplace son binding par celui d’un nouveau filler \(f' = (11, 13)\), soit \(T' = T - f_0 \otimes r_0 + f' \otimes r_0\), puis on relit aux deux rôles.

Objectif. Compléter lectureApresChirurgie pour qu’elle rende l’entrée a de la lecture au rôle j de l’état chirurgical.

  • Etape 1 : retrancher le binding de f_0, ajouter celui de f' — quelles entrées de T sont modifiées, lesquelles ne bougent pas ?
  • Etape 2 : relire aux deux rôles, en confrontant chaque lecture au théorème 1 pour la partie de l’état qui n’a pas changé.
  • Indice : c’est l’exercice de la localité (section 4) — comparez vos deux lectures à celles de l’exercice 2.

Aucune valeur attendue n’est donnée : c’est la comparaison terme à terme avec l’exercice 2 qui valide votre chirurgie.

-- Exercice 3 : certificat entier de la lecture APRES chirurgie du constituant 0,
-- remplacé par f' = (11, 13) : T' = T - f_0 (X) r_0 + f' (X) r_0.
-- TODO etudiant : remplacer le corps ci-dessous
-- Etape 1 : former T' à partir de la superposition T de l'exercice 2
-- Etape 2 : effectuer le produit T' *v r_j et rendre son entrée a
-- Indice : confrontez chaque lecture à celle de l'exercice 2 (localité, section 4).
def lectureApresChirurgie (j a : Fin 2) : Int :=
  0

-- Contrôle : les deux rôles × les deux entrées.
#eval lectureApresChirurgie 0 0
#eval lectureApresChirurgie 0 1
#eval lectureApresChirurgie 1 0
#eval lectureApresChirurgie 1 1
-- L'identité du lake qui certifie la chirurgie sur ℝ.
#check @Sensitivity.TPR.tprSurgery

-- Exercice 3 : certificat entier de la lecture APRES chirurgie du constituant 0,
-- remplacé par f' = (11, 13) : T' = T - f_0 (X) r_0 + f' (X) r_0.
-- TODO etudiant : remplacer le corps ci-dessous
-- Etape 1 : former T' à partir de la superposition T de l'exercice 2
-- Etape 2 : effectuer le produit T' *v r_j et rendre son entrée a
-- Indice : confrontez chaque lecture à celle de l'exercice 2 (localité, section 4).
🟨 Variable name `j` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _j

Note: This linter can be disabled with `set_option linter.unusedVariables false`
🟨 Variable name `a` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _a

Note: This linter can be disabled with `set_option linter.unusedVariables false`
  0
-- Contrôle : les deux rôles × les deux entrées.
 0
 0
 0
 0
-- L'identité du lake qui certifie la chirurgie sur ℝ.
 @Sensitivity.TPR.tprSurgery : ∀ {p q m : ℕ} {fs : Fin m → Fin p → ℝ} {rs : Fin m → Fin q → ℝ},
  Sensitivity.TPR.RoleFamily rs →
    ∀ (j : Fin m) (f' : Fin p → ℝ),
      Sensitivity.TPR.tprUnbind
          (Sensitivity.TPR.tprSuperpos fs rs - Sensitivity.TPR.tprBind (fs j) (rs j) +
            Sensitivity.TPR.tprBind f' (rs j))
          (rs j) =
        f'
--% env 9
Raw input {"cmd": "-- Exercice 3 : certificat entier de la lecture APRES chirurgie du constituant 0,\n-- remplac\u00e9 par f' = (11, 13) : T' = T - f_0 (X) r_0 + f' (X) r_0.\n-- TODO etudiant : remplacer le corps ci-dessous\n-- Etape 1 : former T' \u00e0 partir de la superposition T de l'exercice 2\n-- Etape 2 : effectuer le produit T' *v r_j et rendre son entr\u00e9e a\n-- Indice : confrontez chaque lecture \u00e0 celle de l'exercice 2 (localit\u00e9, section 4).\ndef lectureApresChirurgie (j a : Fin 2) : Int :=\n 0\n\n-- Contr\u00f4le : les deux r\u00f4les \u00d7 les deux entr\u00e9es.\n#eval lectureApresChirurgie 0 0\n#eval lectureApresChirurgie 0 1\n#eval lectureApresChirurgie 1 0\n#eval lectureApresChirurgie 1 1\n-- L'identit\u00e9 du lake qui certifie la chirurgie sur \u211d.\n#check @Sensitivity.TPR.tprSurgery\n", "env": 8}
Raw output {"messages": [{"severity": "warning", "pos": {"line": 7, "column": 27}, "endPos": {"line": 7, "column": 28}, "data": "Variable name `j` is not explicitly referenced.\n\nHint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:\n [apply] _j\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "warning", "pos": {"line": 7, "column": 29}, "endPos": {"line": 7, "column": 30}, "data": "Variable name `a` is not explicitly referenced.\n\nHint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:\n [apply] _a\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`"}, {"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 13, "column": 0}, "endPos": {"line": 13, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 14, "column": 0}, "endPos": {"line": 14, "column": 5}, "data": "0"}, {"severity": "info", "pos": {"line": 16, "column": 0}, "endPos": {"line": 16, "column": 6}, "data": "@Sensitivity.TPR.tprSurgery : ∀ {p q m : ℕ} {fs : Fin m → Fin p → ℝ} {rs : Fin m → Fin q → ℝ},\n Sensitivity.TPR.RoleFamily rs →\n ∀ (j : Fin m) (f' : Fin p → ℝ),\n Sensitivity.TPR.tprUnbind\n (Sensitivity.TPR.tprSuperpos fs rs - Sensitivity.TPR.tprBind (fs j) (rs j) +\n Sensitivity.TPR.tprBind f' (rs j))\n (rs j) =\n f'"}], "env": 9}

Conclusion

Ce companion a interrogé le compilateur Lean sur chaque pièce du module TPR du lake sensitivity_lean, et le kernel a répondu : quatre théorèmes prouvés (unbinding exact, chirurgie, chirurgie vue par un décodeur affine, borne de stabilité), zéro sorry (empreinte [propext, Classical.choice, Quot.sound] partout), et deux hypothèses clairement étiquetées.

Théorème Ce qu’il dit Hypothèses consommées
tprUnbind_superpos la lecture au rôle j rend exactement fs j RoleFamily rs
tprSurgery remplacer le binding de j par f' puis relire rend exactement f' RoleFamily rs
tprSurgery_readout l’effet sur la sortie affine est exactement A.mulVec (f' - fs j) (rendu kernel, notation *ᵥ dans le source) RoleFamily rs + décodeur affine
tprUnbind_approx erreur de lecture bornée par ε * ∑ |r j| TprApproxEntrywise S T ε

Enseignements :

  1. Le modèle est exact, le réseau est approché. Toute la force des théorèmes ci-dessus est conditionnelle aux hypothèses ; la question empirique — un réseau donné les satisfait-il, et à quel ε ? — vit dans SL-13, pas ici.
  2. La chirurgie est une identité, pas une métaphore. « Remplacer un constituant ne déplace que sa lecture » est un théorème d’algèbre dans le modèle — c’est ce qui en fait un test tranchant pour un réseau : soit il approche le modèle et l’intervention transfère, soit il ne l’approche pas.
  3. La cérémonie #check / #print axioms est le garde-fou de l’honnêteté. Elle distingue mécaniquement le prouvé de l’hypothèse — la frontière épistémique de la section 7 n’est pas une posture, elle est dans les types.

Raccords : SL-13 mesure la distance réseau-modèle (DISCOVER, réinjection, chirurgie, contrôles) ; Lean-12b couvre l’autre corpus du lake (Huang 2019) ; Lean-13 poursuit la série. Le module existe aussi en jumeau anglais (TensorProductRepresentation_en.lean, convention i18n #4980) — mêmes énoncés, preuves byte-identiques.

Retour au sommet