diff --git a/.github/workflows/lean-conway.yml b/.github/workflows/lean-conway.yml index ca7b457026..45a16d0280 100644 --- a/.github/workflows/lean-conway.yml +++ b/.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 diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Angel.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Angel.lean index 4ae16ca996..5ab20764ec 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Angel.lean +++ b/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 diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Angel_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Angel_en.lean index ceb66d778b..db410492a9 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Angel_en.lean +++ b/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