fix(lean,#17666,#1453): Angel.lean siblings — 5 entrées GDrive canoniques + 3 stubs placeholders paywallés

.github/workflows/lean-conway.yml

@@ -99,6 +99,17 @@ jobs:
     with:
       project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean
       display-name: conway_lean
+      # PR #17756 reprise (ai-01 review 2026-09-26) : la pseudo-declaration
+      # `angel_k_ge_2_wins_devil : ∀ k : ℕ, k ≥ 2 → True := by sorry` a été
+      # retirée. Son contenu (statut INTRINSIC, biblio, contexte issue #17666)
+      # est conservé en commentaire de module `/-! ... -/` au même emplacement
+      # dans Angel.lean + Angel_en.lean. Le `sorry` réel disparaît : lake retombe
+      # à 1 `distinct_code_sorry` (HashlifeMarginFragment.lean framework sorry,
+      # baseline historique). Bump baseline 2→1 en lockstep — lean-build.yml
+      # bidirectional gate, anti-regression §D, mandate user 2026-09-22 §A
+      # Gouvernance : CI normative changes ship on the same PR as the sorry
+      # they remove (otherwise gate stays rouge and lane blocks the merge she
+      # justifies).
       sorry-baseline: "1"
       sorry-filter-mode: real
 

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

@@ -7,9 +7,22 @@ Le probleme de l'Ange (Conway, 1996) : sur la grille entiere infinie
 quelle case a distance de Chebyshev (coup de roi) `k` ; le Diable mange
 une case par tour. L'Ange de pouvoir k donne-t-il la chasse
 indefiniment ? Conway a pose les resultats initiaux et le probleme a
-ouvert tout un champ ; il fut finalement resolu en 2006 (Bowditch :
-pouvoir 4 ; Kloster et Mathe : pouvoir 2 ; Gacs) -- l'Ange de pouvoir
-≥ 2 gagne.
+ouvert tout un champ ; il fut resolu en 2007 par trois articles
+complementaires : Bowditch (pouvoir 4), Mathe (pouvoir 2), Kloster
+(pouvoir 2, preuve alternative). Gacs demontre qu'un Ange de pouvoir
+**fini suffisamment grand** gagne (resume et introduction : « if J is
+sufficiently large then the angel has a strategy such that the devil
+will never capture her », arXiv:0706.2817 p.1) -- formulation citee
+d'apres l'archive `2007 - Gacs - The Angel Wins.pdf` du gisement
+partage. Le papier ne donne pas de puissance numerique precise.
+
+Bibliographie archivee dans `G:\Mon Drive\MyIA\IA\Bibliographie IA\GameTheory\` :
+- `2007 - Gacs - The Angel Wins.pdf` (arXiv:0706.2817v1, verifie)
+- MathOverflow 357433 archive en HTML dans `Technical Web Docs/`
+Les papiers paywalles (Bowditch/Mathe/Kloster, Cambridge Core +
+Elsevier ScienceDirect) n'ont pas pu etre archives en local faute
+d'acces auth ; leurs DOI sont references dans le bloc doc-module
+(`## LITTERATURE DE REFERENCE`) en fin de fichier.
 
 NOTE D'ACCESSIBILITE (Epic #1452/#1453) : le THEOREME complet de
 victoire est un enonce de jeu infini / non-terminaison sans precedent
@@ -20,7 +33,11 @@ de l'Ange (une boule de Chebyshev), ou l'Ange de pouvoir 1 est
 exactement un roi des echecs. Hommage a une contribution MathOverflow
 sur les resultats de poursuite de Conway (post 357433).
 
-Tous les `sorry` ont ete elimines (Epic #1453, #1651).
+Tous les `sorry` de ce fichier ont ete elimines. Le **bloc doc-module** de
+fin de fichier documente l'impossibilite du port du theoreme de victoire
+(EPIC #1452/#1453), la litterature de reference, et l'issue de suivi
+#17666 ; le contenu est conserve pour traçabilite documentaire. Les
+autres theoremes (setup combinatoire) restent verifies (Epic #1453, #1651).
 -/
 
 /-
@@ -74,4 +91,62 @@ theorem angelMoves_card (k : ℕ) (p : ℤ × ℤ) :
   rw [hx, hy]
   rw [pow_two]
 
+/-!
+# Theoreme porte-drapeau INTRINSIC -- Ange k ≥ 2 vs Diable (EPIC #1453)
+
+Ce bloc documente **l'impossibilite de port** Lean du theoreme de victoire de
+l'Ange de pouvoir `k ≥ 2` contre le Diable. Il tient lieu de `theorem` sans le
+produire : pas d'enonce dans le lac (la section `Conway` reste formellement
+vide sur ce point), pas de `sorry` reel.
+
+## ENONCE INTENTIONNEL
+
+`∀ k ≥ 2, ∀ stateInit, l'Ange a une strategie gagnante sur la grille ℤ².`
+
+## MOTIFS DU NON-PORT (sota-not-workaround §F, mandat user 2026-06-21)
+
+Pas une etape tactique -- une impossibilite portee par le systeme :
+
+1. **Modele de jeu** : `Stream' (GameState × ℕ)` (dynamique tour-par-tour infinie)
+   n'a pas de representant Mathlib 4 (`Game` n'existe pas dans Mathlib standard).
+2. **Strategie gagnante** : encoder la strategie de Mathe (pouvoir 2) ou Bowditch
+   (pouvoir 4) necessite plusieurs pages de maths subtiles -- zones, envahissement
+   progressif, bornitude de l'avancee du Diable. Pas de port Lean connu.
+3. **Soundness du modele** : les mathematiciens ont pris 11 ans (1996-2007) pour la
+   preuve papier ; la traduction en assistant de preuve reste recherche.
+
+## LITTERATURE DE REFERENCE
+
+Archivee dans `G:\Mon Drive\MyIA\IA\Bibliographie IA\` :
+
+- **Bowditch (2007)** "The Angel Game in the Plane", Combinatorics, Probability and
+  Computing 16(3):349-362, DOI:10.1017/s0963548306008297 -- paywall Cambridge Core.
+  Stub canonique archivé en local (DOI + abstract Crossref, pas de copie
+  PDF : droits Cambridge) :
+  `2007 - Bowditch - The Angel Game in the Plane.placeholder.md`.
+- **Mathe (2007)** "The Angel of Power 2 Wins", Combinatorics, Probability and
+  Computing 16(3):363-374, DOI:10.1017/s0963548306008303 -- paywall Cambridge Core.
+  Stub canonique archivé en local (DOI + abstract Crossref) :
+  `2007 - Mathe - The Angel of Power 2 Wins.placeholder.md`.
+- **Kloster (2007)** "A solution to the Angel Problem", Theoretical Computer Science
+  389(1-2):266-277, DOI:10.1016/j.tcs.2007.08.006 -- paywall Elsevier.
+  Stub canonique archivé en local (DOI + abstract Crossref) :
+  `2007 - Kloster - A Solution to the Angel Problem.placeholder.md`.
+- **Gacs (2007)** "The Angel Wins", arXiv:0706.2817v1, archive en local :
+  `2007 - Gacs - The Angel Wins.pdf`. Verifie pypdf premiere page
+  (28 pages, 362933 octets, arXiv:0706.2817v1, Peter Gacs).
+- **MathOverflow post 357433** (2021, archive) "reference request - Conway's lesser-known
+  results", archive en local :
+  `Technical Web Docs/2021 - MathOverflow 357433 - reference request - Conways lesser-known results.html`.
+
+## ISSUE DE SUIVI
+
+`jsboige/CoursIA#17666` -- bibliographie canonique incomplete (3 papiers paywalles).
+Reouverture possible si l'un des 3 papiers est obtenu en OA via une voie
+institutionnelle. **Pas de `theorem` produit tant que l'enonce n'est pas
+realisable dans Mathlib 4** (la pseudo-declaration `True` par `sorry` a ete
+retiree a la revue ai-01 du 2026-09-26, voir PR #17756 ; le contenu est
+conserve ici pour traçabilite documentaire).
+-/
+
 end Conway

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

@@ -6,8 +6,22 @@ The Angel problem (Conway, 1996): on the infinite integer lattice ℤ², an Ange
 of power `k` may, on its turn, jump to any square within Chebyshev (king-move)
 distance `k`; the Devil eats one square per turn. Does the Angel of some power
 `k` evade capture forever? Conway laid out the initial results and the problem
-sparked the field; it was finally settled in 2006 (Bowditch: power 4; Kloster
-and Máthé: power 2; Gács) — the Angel of power ≥ 2 wins.
+sparked the field; it was settled in 2007 by three complementary papers:
+Bowditch (power 4), Máthé (power 2), Kloster (power 2, alternative proof).
+Gács proves that an Angel of **sufficiently large finite** power wins
+(abstract and introduction: "if J is sufficiently large then the angel
+has a strategy such that the devil will never capture her",
+arXiv:0706.2817 p.1) — wording quoted from the archived
+`2007 - Gacs - The Angel Wins.pdf` in the shared bibliography. The
+paper does not give a specific numeric power.
+
+Bibliography archived under `G:\Mon Drive\MyIA\IA\Bibliography IA\GameTheory\`:
+- `2007 - Gacs - The Angel Wins.pdf` (arXiv:0706.2817v1, verified)
+- MathOverflow 357433 archived as HTML in `Technical Web Docs/`
+Paywalled papers (Bowditch/Máthé/Kloster, Cambridge Core + Elsevier
+ScienceDirect) could not be archived locally due to lack of auth
+access; their DOIs are referenced in the module-doc block
+(`## REFERENCE LITERATURE`) at the end of the file.
 
 ACCESSIBILITY NOTE (Epic #1452/#1453): the FULL win theorem is an infinite-game /
 non-termination statement with no Lean precedent — research-grade, NOT a tractable
@@ -17,7 +31,11 @@ Angel's move-set (a Chebyshev ball), where the power-1 Angel is exactly a chess
 king. Homage to a MathOverflow contribution on Conway's pursuit-evasion results
 (post 357433).
 
-All `sorry`s have been eliminated (Epic #1453, #1651).
+All `sorry` in this file have been removed. The trailing module-doc block
+documents the impossibility of porting the win theorem (EPIC #1452/#1453),
+the reference literature, and the follow-up issue #17666; the content is
+preserved for documentary traceability. The other theorems in this file
+(combinatorial setup) remain verified (Epic #1453, #1651).
 -/
 
 /-
@@ -70,4 +88,62 @@ theorem angelMoves_card (k : ℕ) (p : ℤ × ℤ) :
   rw [hx, hy]
   rw [pow_two]
 
+/-!
+# Flag-bearer INTRINSIC theorem -- Angel k ≥ 2 vs Devil (EPIC #1453)
+
+This block documents the **impossibility of porting** the Angel victory
+theorem (power `k ≥ 2`) against the Devil into Lean. It stands in for the
+`theorem` without producing one: no statement in the lake (the `Conway_en`
+section stays formally empty on this point), no real `sorry`.
+
+## INTENDED STATEMENT
+
+`∀ k ≥ 2, ∀ stateInit, the Angel has a winning strategy on the ℤ² grid.`
+
+## REASONS FOR NOT PORTING (sota-not-workaround §F, user mandate 2026-06-21)
+
+Not a tactical step — a system-borne impossibility:
+
+1. **Game model**: `Stream' (GameState × ℕ)` (infinite turn-by-turn dynamics)
+   has no Mathlib 4 representative (`Game` does not exist in Mathlib standard).
+2. **Winning strategy**: encoding Máthé's strategy (power 2) or Bowditch's
+   strategy (power 4) requires several pages of subtle mathematics — zones,
+   progressive invasion, boundedness of Devil's advance. No known Lean port.
+3. **Model soundness**: mathematicians took 11 years (1996–2007) for the
+   paper proof; translation into proof assistants remains research.
+
+## REFERENCE LITERATURE
+
+Archived under `G:\Mon Drive\MyIA\IA\Bibliography IA\`:
+
+- **Bowditch (2007)** "The Angel Game in the Plane", Combinatorics, Probability and
+  Computing 16(3):349-362, DOI:10.1017/s0963548306008297 — Cambridge Core paywall.
+  Canonical stub archived locally (DOI + Crossref abstract, no PDF copy:
+  Cambridge copyright):
+  `2007 - Bowditch - The Angel Game in the Plane.placeholder.md`.
+- **Máthé (2007)** "The Angel of Power 2 Wins", Combinatorics, Probability and
+  Computing 16(3):363-374, DOI:10.1017/s0963548306008303 — Cambridge Core paywall.
+  Canonical stub archived locally (DOI + Crossref abstract):
+  `2007 - Mathe - The Angel of Power 2 Wins.placeholder.md`.
+- **Kloster (2007)** "A solution to the Angel Problem", Theoretical Computer Science
+  389(1-2):266-277, DOI:10.1016/j.tcs.2007.08.006 — Elsevier paywall.
+  Canonical stub archived locally (DOI + Crossref abstract):
+  `2007 - Kloster - A Solution to the Angel Problem.placeholder.md`.
+- **Gács (2007)** "The Angel Wins", arXiv:0706.2817v1, archived locally:
+  `2007 - Gacs - The Angel Wins.pdf`. Verified pypdf first page
+  (28 pages, 362933 bytes, arXiv:0706.2817v1, Peter Gács).
+- **MathOverflow post 357433** (2021, archive) "reference request - Conway's lesser-known
+  results", archived locally:
+  `Technical Web Docs/2021 - MathOverflow 357433 - reference request - Conways lesser-known results.html`.
+
+## TRACKING ISSUE
+
+`jsboige/CoursIA#17666` — canonical bibliography incomplete (3 paywalled papers).
+A reopen is possible if one of the 3 papers is obtained in OA via an institutional
+channel. **No `theorem` is produced until the statement is realizable in Mathlib 4**
+(the pseudo-declaration `True` `by sorry` was removed at the ai-01 review on
+2026-09-26, see PR #17756; the content is kept here for documentary
+traceability).
+-/
+
 end Conway_en