feat(lean,#16341): conway_lean v4.32.1 → v4.33.0 — Foundation simp chain + Fintype FreeWillTheorem

MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/FreeWillTheorem.lean

@@ -114,7 +114,16 @@ La conclusion : la réponse d'aucune des deux particules ne peut être une fonct
 inductive Experimenter
   | alice
   | bob
-  deriving DecidableEq, Fintype
+  deriving DecidableEq
+
+/-- Instance `Fintype` manuelle (migration v4.33, #16341) : `deriving Fintype`
+    produit du code attendant `List.Nodup` alors que `Finset.mk` exige
+    `Finset.Nodup` en v4.33 (nouveau type encapsulant). -/
+instance : Fintype Experimenter where
+  elems := Finset.mk [Experimenter.alice, Experimenter.bob] (by decide)
+  complete := by
+    intro x
+    cases x <;> simp [Finset.mem_mk]
 
 /-- Un modèle déterministe à deux particules associe un résultat {0,1} défini
     à chaque expérimentateur, état caché et direction de mesure.

MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/FreeWillTheorem_en.lean

@@ -128,7 +128,16 @@ The conclusion: neither particle's response can be a function of the past.
 inductive Experimenter
   | alice
   | bob
-  deriving DecidableEq, Fintype
+  deriving DecidableEq
+
+/-- Manual `Fintype` instance (v4.33 migration, #16341): `deriving Fintype`
+    generates code expecting `List.Nodup` while v4.33 `Finset.mk` requires
+    `Finset.Nodup` (new wrapping type). -/
+instance : Fintype Experimenter where
+  elems := Finset.mk [Experimenter.alice, Experimenter.bob] (by decide)
+  complete := by
+    intro x
+    cases x <;> simp [Finset.mem_mk]
 
 /-- A two-particle deterministic model assigns a definite {0,1} outcome
     to each experimenter, hidden state, and measurement direction.

MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeCorrectness/Foundation.lean

@@ -2445,8 +2445,21 @@ private theorem hashlifeResultAux_level_cellWf_step (n : Nat) (hn3 : 3 ≤ n)
                            (hashlifeResultAux (n - 1) (node se_nw se_ne se_sw se_se))
                            hr5.1 hr6.1 hr8.1 hr9.1 hr5.2 hr6.2 hr8.2 hr9.2
     -- Unfold hRA's recursive arm now that the wave facts are established.
-    simp only [hashlifeResultAux, if_neg heq, MacroCell.level]
-    exact node_level_cellWf_conjuncts n hn3 _ _ _ _
+    -- v4.33 (#16341): the elaboration of the upstream `if c.level == 2`
+    -- (Hashlife.lean:174) no longer matches `if_neg heq` after `simp only`;
+    -- case-split the unfolded `if` directly. The positive arm is vacuous:
+    -- 16 grandchildren at level (n - 2) put the node at level n ≥ 3.
+    simp only [hashlifeResultAux]
+    split
+    · exfalso
+      rename_i hcond
+      have hnode := node16_level nw_nw nw_ne nw_sw nw_se ne_nw ne_ne ne_sw ne_se
+                   sw_nw sw_ne sw_sw sw_se se_nw se_ne se_sw se_se n (by omega) hnw_nw_l
+      try rw [hnode] at hcond
+      try simp only [MacroCell.level] at hcond
+      have hn2 : n = 2 := by simpa [beq_iff_eq] using hcond
+      omega
+    · exact node_level_cellWf_conjuncts n hn3 _ _ _ _
         honw.1 hone.1 hosw.1 hose.1 honw.2 hone.2 hosw.2 hose.2
 
 /-- **(c.142) Level + well-formedness preservation of `hashlifeResultAux`**,

MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "520045ab14e26149ee970e2e617ca04b09bde5d6",
+   "rev": "db584cd6d46c92f209a44c0f1c829460d327499d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.32.1",
+   "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
+   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12",
+   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93",
+   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3",
+   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
+   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff",
+   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94",
+   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.32.0",
+   "inputRev": "v4.33.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "conway",

MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/lakefile.lean

@@ -7,13 +7,13 @@ package «conway» where
     ⟨`autoImplicit, false⟩
   ]
 
--- Pin explicite v4.32.1 (harmonisation #4362) : sans `@`, lake resout la
--- require sur `master` par defaut alors que lake-manifest.json est epingle sur
--- v4.32.1 -> warning `manifest out of date: git revision of
+-- Pin explicite v4.33.0 (harmonisation #4362, migration #16341) : sans `@`,
+-- lake resout la require sur `master` par defaut alors que lake-manifest.json
+-- est epingle sur v4.33.0 -> warning `manifest out of date: git revision of
 -- dependency 'mathlib' changed` a CHAQUE lake build (bruit dans les logs du
 -- prover BG, et un `lake update` accidentel sauterait sur master).
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "v4.32.1"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.33.0"
 
 @[default_target]
 lean_lib «Conway» where

MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.32.1
+leanprover/lean4:v4.33.0