Add(notebook-lean,#20184): ANALYSE-06 Sensibilite 2026 -- carnet FR+_en executes + Check.lean (Pli 2 #19898)

MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Check.lean

@@ -0,0 +1,37 @@
+import Sensitivity.MainTheorem
+import Sensitivity.Sens2026
+
+/-!
+# Point d'entree de verification pour le carnet ANALYSE-06
+
+Ce fichier n'est PAS compile par `lake build` (hors globs de la lib) : il sert
+au carnet `../ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python.ipynb`, qui
+l'execute via `lake env lean Check.lean` pour afficher les signatures reelles
+du socle et de l'ajout 2026, et prouver l'integrite des theoremes (aucun
+axiome au-dela des trois standards, aucun sorry).
+
+Statut epistemique (Epic Origami #19898, Pli 2) : les enonces 127/132/186/192
+du depot openai/math sont cites par le carnet AVEC leur statut — formalises
+en amont (squelette Lean publie), non re-prouves ici. Ce qui est verifie
+ci-dessous est a NOUS : les definitions de `Separations`, le temoin `tribes32`
+de `Sens2026`, et le theoreme de Huang porte par le lac.
+-/
+
+#check @Sensitivity.sensitivity
+#check @Sensitivity.blockSensitivity
+#check @Sensitivity.tribes32
+#check @Sensitivity.tribes32_sensitivity_zero
+#check @Sensitivity.tribes32_sensitivity_eq_three
+#check @Sensitivity.tribes32_blockSensitivity_ge_three
+#check @Sensitivity.tribes32_local_separation
+#check @Sensitivity.or3_blockSensitivity
+#check @Sensitivity.orOfAnds_strict_separation
+#check @Sensitivity.huang_degree_theorem
+
+#print axioms Sensitivity.huang_degree_theorem
+#print axioms Sensitivity.tribes32_sensitivity_zero
+#print axioms Sensitivity.tribes32_sensitivity_eq_three
+#print axioms Sensitivity.tribes32_blockSensitivity_ge_three
+#print axioms Sensitivity.tribes32_local_separation
+#print axioms Sensitivity.or3_blockSensitivity
+#print axioms Sensitivity.orOfAnds_strict_separation

MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity.lean

@@ -21,3 +21,4 @@ import Sensitivity.Fourier
 import Sensitivity.SpectralDegree
 import Sensitivity.TensorProductRepresentation
 import Sensitivity.Separations
+import Sensitivity.Sens2026

MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Sens2026.lean

@@ -0,0 +1,107 @@
+import Sensitivity.Separations
+import Mathlib.Tactic.FinCases
+
+/-!
+# Sensibilité 2026 : trois équipes, une réfutation, et ce que le dépôt openai/math dit de ces objets
+
+Ce fichier est un **ajout additif** au lac `sensitivity_lean` (Epic Origami
+#19898, Pli 2, issue #20184) : il ne modifie aucun énoncé existant — ni le
+théorème de Huang (`MainTheorem`), ni les définitions et témoins de
+`Separations`. Il réutilise `sensitivity`, `blockSensitivity` et `flipBlock`
+tels quels, et ajoute le témoin **tribus à trois équipes** `tribes32` : la
+disjonction de trois conjonctions de taille deux sur `Q 6`.
+
+## La famille 132, citée avec son statut
+
+La famille 132 du dépôt openai/math (2026) — « fonctions booléennes totales
+avec `bs(f) ≥ s(f)^α` pour un `α > 2` fixé » — **réfute** le renforcement
+quadratique de la conjecture de sensibilité : le gap `bs/s` peut dépasser
+tout polynôme fixé en `s`. Ce résultat est cité **avec son statut**
+(formalisé en amont, `lean/docs/132.md` du dépôt ; non re-prouvé par nous) :
+sa re-preuve est hors d'échelle du lac.
+
+`tribes32` est l'**écho calculable** de ce voisinage — et il enseigne deux
+choses, dont une contre-intuitive :
+
+1. **La séparation locale s'étend** : au sommet nul, `s = 0` et `bs ≥ 3`
+   (la famille des trois tribus est admissible) — le même écart local que le
+   témoin `orOfAnds` de `Separations`, mais avec trois blocs au lieu d'un.
+2. **Le majorant naïf `s ≤ t` (taille d'une tribu) est FAUX** — et c'est
+   `decide` qui l'a réfuté, à la compilation : au sommet « une lampe allumée
+   par tribu », chaque première coordonnée allume sa conjonction, et la
+   sensibilité locale vaut **3** (`tribes32_sensitivity_eq_three`). À cette
+   échelle, `s` rattrape `bs` : les tribus seules ne séparent pas
+   *globalement* — la séparation de la littérature demande les constructions
+   d'adressage (Rubinstein 1995), hors d'échelle ici, citées pour ça.
+
+Le récit pédagogique est exactement celui de 2026 : **mesuré, pas supposé** —
+l'intuition « deux lampes par tribu, donc sensibilité 2 » ne survit pas à
+l'énumération exhaustive du noyau.
+-/
+
+namespace Sensitivity
+
+open Bool Finset Fintype
+
+/-- Témoignage « tribus » en dimension 6 : disjonction de trois conjonctions
+de taille deux (trois « équipes » de deux coordonnées) — les `tribes` de la
+littérature Nisan–Szegedy, à l'échelle calculable. -/
+def tribes32 (x : Q 6) : Bool :=
+  (x 0 && x 1) || (x 2 && x 3) || (x 4 && x 5)
+
+/-- Au sommet nul, aucune coordonnée seule n'allume `tribes32` : il faut
+retourner une tribu **entière**. La sensibilité locale y est nulle. -/
+theorem tribes32_sensitivity_zero :
+    sensitivity tribes32 (fun _ => false) = 0 := by
+  decide
+
+/-- **La réfutation de l'intuition, par énumération exhaustive.** Au sommet
+« une lampe allumée par tribu » (coordonnées impaires), chaque première
+coordonnée allume sa conjonction à elle seule : la sensibilité locale vaut
+**3**, pas 2. Le majorant naïf « au plus une taille de tribu » est faux —
+c'est le noyau Lean qui l'a établi, en réfutant la conjecture `∀ x, s ≤ 2`
+à la compilation. -/
+theorem tribes32_sensitivity_eq_three :
+    sensitivity tribes32 (fun i => i.val % 2 = 1) = 3 := by
+  decide
+
+set_option maxRecDepth 8192 in
+/-- Au sommet nul, la famille des trois tribus `{{0,1}, {2,3}, {4,5}}` est
+admissible au sens de `blockSensitivity` : blocs non vides, chacun bascule la
+valeur, deux à deux disjoints. La sensibilité de bloc y est donc au moins
+**3**. -/
+theorem tribes32_blockSensitivity_ge_three :
+    3 ≤ blockSensitivity tribes32 (fun _ => false) := by
+  classical
+  have hfam : ∀ B ∈ ({({0, 1} : Finset (Fin 6)), {2, 3}, {4, 5}} :
+      Finset (Finset (Fin 6))),
+      B.Nonempty ∧ tribes32 (flipBlock (fun _ => false) B) ≠ tribes32 (fun _ => false) := by
+    decide
+  have hpair : ∀ B₁ ∈ ({({0, 1} : Finset (Fin 6)), {2, 3}, {4, 5}} :
+      Finset (Finset (Fin 6))),
+      ∀ B₂ ∈ ({({0, 1} : Finset (Fin 6)), {2, 3}, {4, 5}} :
+        Finset (Finset (Fin 6))),
+      B₁ ≠ B₂ → (B₁ ∩ B₂ : Finset (Fin 6)) = ∅ := by
+    decide
+  have hcard : ({({0, 1} : Finset (Fin 6)), {2, 3}, {4, 5}} :
+      Finset (Finset (Fin 6))).card = 3 := by
+    decide
+  have hle : ({({0, 1} : Finset (Fin 6)), {2, 3}, {4, 5}} :
+      Finset (Finset (Fin 6))).card ≤ blockSensitivity tribes32 (fun _ => false) :=
+    Finset.le_sup (Finset.mem_filter.2 ⟨Finset.mem_univ _, ⟨hfam, hpair⟩⟩)
+  rw [hcard] at hle
+  exact hle
+
+/-- **Séparation locale à trois blocs** : au sommet nul, `s = 0 < 3 ≤ bs`.
+Le même écart local que le témoin `orOfAnds` de `Separations` (un bloc),
+généralisé à trois blocs disjoints — la mécanique exacte par laquelle les
+constructions d'adressage de la littérature fabriquent leurs gaps. La
+séparation *globale* n'est pas claimée : `tribes32_sensitivity_eq_three`
+montre que `s` rattrape `bs` ailleurs sur le cube. -/
+theorem tribes32_local_separation :
+    sensitivity tribes32 (fun _ => false) <
+      blockSensitivity tribes32 (fun _ => false) := by
+  rw [tribes32_sensitivity_zero]
+  exact Nat.lt_of_lt_of_le (by decide) tribes32_blockSensitivity_ge_three
+
+end Sensitivity

MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Sens2026_en.lean

@@ -0,0 +1,110 @@
+import Sensitivity.Separations_en
+import Mathlib.Tactic.FinCases
+
+/-!
+# Sensitivity 2026: three teams, one refutation, and what the openai/math repo says about these objects
+
+This file is an **additive** contribution to the `sensitivity_lean` lake
+(Origami Epic #19898, fold 2, issue #20184): it modifies no existing
+statement — neither Huang's theorem (`MainTheorem`) nor the definitions and
+witnesses of `Separations`. It reuses `sensitivity`, `blockSensitivity` and
+`flipBlock` as they stand, and adds the **three-tribe witness** `tribes32`:
+the disjunction of three size-two conjunctions over `Q 6`.
+
+## Family 132, quoted with its status
+
+Family 132 of the openai/math repository (2026) — "total Boolean functions
+with `bs(f) ≥ s(f)^α` for a fixed `α > 2`" — **refutes** the quadratic
+strengthening of the sensitivity conjecture: the `bs/s` gap can exceed any
+fixed polynomial in `s`. That result is quoted **with its status**
+(formalized upstream, `lean/docs/132.md` of the repository; not re-proved by
+us): re-proving it is out of scale for this lake.
+
+`tribes32` is the **computable echo** of this neighbourhood — and it teaches
+two things, one of them counterintuitive:
+
+1. **The local separation extends**: at the zero vertex, `s = 0` and
+   `bs ≥ 3` (the family of the three tribes is admissible) — the same local
+   gap as the `orOfAnds` witness of `Separations`, but with three blocks
+   instead of one.
+2. **The naive bound `s ≤ t` (one tribe's size) is FALSE** — and it is
+   `decide` that refuted it, at compile time: at the "one lit lamp per
+   tribe" vertex, each first coordinate lights up its conjunction on its
+   own, and the local sensitivity there is **3**
+   (`tribes32_sensitivity_eq_three`). At this scale, `s` catches up with
+   `bs`: tribes alone do not separate *globally* — the literature's
+   separation requires addressing constructions (Rubinstein 1995), out of
+   scale here and quoted for that reason.
+
+The pedagogical story is exactly the 2026 one: **measured, not assumed** —
+the intuition "two lamps per tribe, hence sensitivity 2" does not survive
+the kernel's exhaustive enumeration.
+-/
+
+namespace Sensitivity_en
+
+open Bool Finset Fintype
+
+/-- The "tribes" witness in dimension 6: disjunction of three size-two
+conjunctions (three "teams" of two coordinates) — the `tribes` of the
+Nisan–Szegedy literature, at computable scale. -/
+def tribes32 (x : Q 6) : Bool :=
+  (x 0 && x 1) || (x 2 && x 3) || (x 4 && x 5)
+
+/-- At the zero vertex, no single coordinate lights up `tribes32`: a whole
+tribe must be flipped. The local sensitivity there is zero. -/
+theorem tribes32_sensitivity_zero :
+    sensitivity tribes32 (fun _ => false) = 0 := by
+  decide
+
+/-- **The refutation of the intuition, by exhaustive enumeration.** At the
+"one lit lamp per tribe" vertex (odd coordinates), each first coordinate
+lights up its conjunction by itself: the local sensitivity there is **3**,
+not 2. The naive bound "at most one tribe's size" is false — it is the Lean
+kernel that established this, by refuting the conjecture `∀ x, s ≤ 2` at
+compile time. -/
+theorem tribes32_sensitivity_eq_three :
+    sensitivity tribes32 (fun i => i.val % 2 = 1) = 3 := by
+  decide
+
+set_option maxRecDepth 8192 in
+/-- At the zero vertex, the family of the three tribes `{{0,1}, {2,3}, {4,5}}`
+is admissible in the sense of `blockSensitivity`: nonempty blocks, each
+flipping the value, pairwise disjoint. The block sensitivity there is
+therefore at least **3**. -/
+theorem tribes32_blockSensitivity_ge_three :
+    3 ≤ blockSensitivity tribes32 (fun _ => false) := by
+  classical
+  have hfam : ∀ B ∈ ({({0, 1} : Finset (Fin 6)), {2, 3}, {4, 5}} :
+      Finset (Finset (Fin 6))),
+      B.Nonempty ∧ tribes32 (flipBlock (fun _ => false) B) ≠ tribes32 (fun _ => false) := by
+    decide
+  have hpair : ∀ B₁ ∈ ({({0, 1} : Finset (Fin 6)), {2, 3}, {4, 5}} :
+      Finset (Finset (Fin 6))),
+      ∀ B₂ ∈ ({({0, 1} : Finset (Fin 6)), {2, 3}, {4, 5}} :
+        Finset (Finset (Fin 6))),
+      B₁ ≠ B₂ → (B₁ ∩ B₂ : Finset (Fin 6)) = ∅ := by
+    decide
+  have hcard : ({({0, 1} : Finset (Fin 6)), {2, 3}, {4, 5}} :
+      Finset (Finset (Fin 6))).card = 3 := by
+    decide
+  have hle : ({({0, 1} : Finset (Fin 6)), {2, 3}, {4, 5}} :
+      Finset (Finset (Fin 6))).card ≤ blockSensitivity tribes32 (fun _ => false) :=
+    Finset.le_sup (Finset.mem_filter.2 ⟨Finset.mem_univ _, ⟨hfam, hpair⟩⟩)
+  rw [hcard] at hle
+  exact hle
+
+/-- **Local separation with three blocks**: at the zero vertex,
+`s = 0 < 3 ≤ bs`. The same local gap as the `orOfAnds` witness of
+`Separations` (one block), generalized to three disjoint blocks — the exact
+mechanics by which the literature's addressing constructions build their
+gaps. The *global* separation is not claimed:
+`tribes32_sensitivity_eq_three` shows that `s` catches up with `bs`
+elsewhere on the cube. -/
+theorem tribes32_local_separation :
+    sensitivity tribes32 (fun _ => false) <
+      blockSensitivity tribes32 (fun _ => false) := by
+  rw [tribes32_sensitivity_zero]
+  exact Nat.lt_of_lt_of_le (by decide) tribes32_blockSensitivity_ge_three
+
+end Sensitivity_en

MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity_en.lean

@@ -21,3 +21,4 @@ import Sensitivity.Fourier_en
 import Sensitivity.SpectralDegree_en
 import Sensitivity.TensorProductRepresentation_en
 import Sensitivity.Separations_en
+import Sensitivity.Sens2026_en

scripts/tests/baseline_nb_nav_chain.json

@@ -1890,6 +1890,16 @@
       "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-04-DD-AR-Python.ipynb",
       "series": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry"
     },
+    {
+      "kind": "unreachable",
+      "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-12b-Lean-Sensitivity-Theorem.ipynb",
+      "series": "MyIA.AI.Notebooks/SymbolicAI/Lean"
+    },
+    {
+      "kind": "unreachable",
+      "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-12c-Tensor-Product-Representations-Lean.ipynb",
+      "series": "MyIA.AI.Notebooks/SymbolicAI/Lean"
+    },
     {
       "kind": "unreachable",
       "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb",

scripts/translation/tests/test_check_translation_parity.py

@@ -714,7 +714,12 @@ def test_is_scannable_matches_on_relative_parts_only(tmp_path):
 # sur main avec son carnet et sans mettre a jour cette ligne, ce qui a rougi
 # `test_full_repo_state_passes_parity` (found 9, declared 8) sur toute PR
 # path-filtree scripts/**. Total apres fusion : 9.
-EXPECTED_PAIR_COUNT = 9
+# 2026-10-12 (PR #20392, #20184 pli ANALYSE-06 Sensibilite): +1 paire --
+# jumeau _en d'un carnet Lean : SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python_en.
+# Meme classe que l'entree #19996 ci-dessus : la paire arrive avec son carnet,
+# la declaration l'enregistre dans la meme PR (rouge mesure a tete constante,
+# 1 failed / 34 passed, avant cet enregistrement). Total apres fusion : 10.
+EXPECTED_PAIR_COUNT = 10
 
 
 def _collect_parity_failures(repo_root: Path,