From 254155bc8b78fd4923e0d0313fe6c37ff63436bf Mon Sep 17 00:00:00 2001 From: jsboige Date: Fri, 2 Oct 2026 20:41:37 +0200 Subject: [PATCH] =?UTF-8?q?fix(lean,#13483):=20tranche=2011=20=E2=80=94=20?= =?UTF-8?q?admission=20des=20t=C3=A9moins=20glider=20et=20LWSS=20(cha?= =?UTF-8?q?=C3=AEne=20dyadique)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - glider_hcap_of_spaceship / lwss_hcap_of_spaceship : pour tout horizon t, la reconstruction est capturee par Hashlife via hcap_of_spaceship (chaine dyadique : p = 4 = 2^2 divise 2^level des level >= 2 ; cadres de niveaux 3 et 4) - support par temoin : canonical, ship4 (pont beq_iff_eq sur les temoins noyau-certifies glider_spaceship / lwss_is_spaceship), frame_off/lvl, hdiv clos par le noyau sur les quatre phases - aucun sorry, aucun native_decide, aucun axiome ajoute ; paire FR/EN Pattern A resynchronisee (check_i18n_siblings.py : 19/19 byte-identical) - build : lake build Conway.Life.HashlifeMarginFragment Conway.Life.HashlifeMarginFragment_en — SUCCESS (8730 jobs) See #13483 Co-Authored-By: Claude Sonnet 5.5 --- .../Conway/Life/HashlifeMarginFragment.lean | 94 +++++++++++++++++++ .../Life/HashlifeMarginFragment_en.lean | 93 ++++++++++++++++++ 2 files changed, 187 insertions(+) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment.lean index 9e268abb14..42f2131af2 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment.lean @@ -76,6 +76,7 @@ import Conway.Life.AdversarialBattery import Conway.Life.HashlifeCorrectness import Conway.Life.LightCone import Conway.Life.Oscillators +import Conway.Life.PatternTour namespace Conway namespace Life @@ -1926,6 +1927,99 @@ theorem hickersonC3_hcap_of_spaceship_mod : hcap_of_spaceship_mod hickersonC3 hickersonC3_canonical (by decide) (-1, 0) hickersonC3_spaceship hickersonC3_hwin (by norm_num) (by norm_num) +/-! ### Témoins phares : glider et LWSS (tranche 11, admission) + +Les deux **vaisseaux** que la docstring de `hashlife_correct_margin_of_spaceship` +annonçait — glider (`p = 4`, `v = (1, -1)`, « la vérifie strictement ») et LWSS (`p = 4`, +`v = (0, 2)`, « atteint la borne exactement ») — sont admis par la **chaîne dyadique** +`hcap_of_spaceship`. Pour `p = 4 = 2²`, la prémisse de divisibilité `4 ∣ 2^level` est +acquise **dès que le niveau atteint `log₂ p = 2`** : elle vaut donc pour les deux témoins, +dont les cadres se reconstruisent aux niveaux **3** (glider, côté 7) et **4** (LWSS, côté +9). Chaque `hdiv` se clôt par le noyau sur les quatre phases (calcul fini) ; le +relâchement par containment de la tranche 9 n'est pas requis pour des témoins de +période 4. + +**Note preuve.** Les témoins Bool du bestiaire (`Life.glider_spaceship`, +`PatternTour.lwss_is_spaceship`) sont déjà certifiés par le réducteur du **noyau** +(`decide` sur `isSpaceship`, Bool) ; le pont vers l'égalité de listes est `beq_iff_eq` +— aucun `native_decide`, aucun axiome ajouté. -/ + +/-- Le littéral du glider est canonique (trié, sans doublon) : le noyau le + certifie, puis `canonical_sortDedup` convertit. -/ +theorem glider_canonical : Canonical glider := by + have h : glider = sortDedup glider := by decide + rw [h] + exact canonical_sortDedup _ + +/-- Relation de vaisseau du glider en égalité de listes : le témoin Bool + `glider_spaceship` (déjà noyau-certifié) transporté en `Prop`. -/ +theorem glider_ship4 : evolve 4 glider = shift (1, -1) glider := + beq_iff_eq.mp glider_spaceship + +/-- Cadre de reconstruction du glider : offset `(-2, -2)` (marge 2 autour de + la boîte `[0, 2]²`). -/ +theorem glider_frame_off : (gridToMacroCellWithOffset glider).1 = (-2, -2) := by decide + +/-- Niveau du cadre du glider : côté `max(2+5, 2+5) = 7` → niveau **3** — mesuré. + Comme `3 ≥ log₂ 4 = 2`, la divisibilité `4 ∣ 2³ = 8` tient : le glider relève + de la chaîne dyadique, comme le LWSS. -/ +theorem glider_frame_lvl : (gridToMacroCellWithOffset glider).2.level = 3 := by decide + +/-- Le littéral du LWSS est canonique. -/ +theorem lwss_canonical : Canonical lwss := by + have h : lwss = sortDedup lwss := by decide + rw [h] + exact canonical_sortDedup _ + +/-- Relation de vaisseau du LWSS en égalité de listes (témoin Bool + `lwss_is_spaceship` de `PatternTour`, noyau-certifié). -/ +theorem lwss_ship4 : evolve 4 lwss = shift (0, 2) lwss := + beq_iff_eq.mp lwss_is_spaceship + +/-- Cadre de reconstruction du LWSS : offset `(-2, -2)` (marge 2 autour de + la boîte `[0, 3] × [0, 4]`). -/ +theorem lwss_frame_off : (gridToMacroCellWithOffset lwss).1 = (-2, -2) := by decide + +/-- Niveau du cadre du LWSS : côté `max(3+5, 4+5) = 9` → niveau 4 — la chaîne + dyadique s'applique (`4 ∣ 2⁴`), exactement comme la docstring l'annonçait. -/ +theorem lwss_frame_lvl : (gridToMacroCellWithOffset lwss).2.level = 4 := by decide + +/-- Divisibilité de la période sur les quatre phases du LWSS : chaque + `evolve i lwss` (`i < 4`) se reconstruit au niveau 4, donc `4 ∣ 2⁴`. Le + calcul par le noyau est fini : 4 phases, ≤ 17 cellules. -/ +theorem lwss_hdiv : + ∀ i, i < 4 → 4 ∣ 2 ^ (gridToMacroCellWithOffset (evolve i lwss)).2.level := by + intro i hi + interval_cases i <;> decide + +set_option maxRecDepth 1000000 in +/-- Divisibilité de la période sur les quatre phases du glider : chaque + `evolve i glider` (`i < 4`) se reconstruit au niveau 3 (mesuré pour les + quatre phases), et `4 ∣ 2³`. Le calcul par le noyau est fini : 4 phases, + grilles de 5 cellules. -/ +theorem glider_hdiv : + ∀ i, i < 4 → 4 ∣ 2 ^ (gridToMacroCellWithOffset (evolve i glider)).2.level := by + intro i hi + interval_cases i <;> decide + +/-- Capstone : le **glider** est admis par `hcap_of_spaceship` — la chaîne + dyadique, comme le LWSS (`p = 4 = 2²` divise `2^level` dès `level ≥ 2` ; + cadre de niveau 3). La borne de vitesse tient strictement + (`2·|1| = 2 < 4`, `2·|-1| = 2 < 4`) : pour tout horizon `t`, la reconstruction + de `evolve t glider` est capturée par Hashlife. -/ +theorem glider_hcap_of_spaceship : + ∀ t, jumpCapturedF (gridToMacroCellWithOffset (evolve t glider)).2 = true := + hcap_of_spaceship glider glider_canonical (by decide) (1, -1) glider_ship4 + glider_hdiv (by norm_num) (by norm_num) + +/-- Capstone : le **LWSS** est admis par `hcap_of_spaceship` — la borne de + vitesse exacte (`2·|2| = 4 ≤ 4`) et la divisibilité dyadique (`4 ∣ 2⁴`, + cadre de niveau 4) que la docstring annonçait. -/ +theorem lwss_hcap_of_spaceship : + ∀ t, jumpCapturedF (gridToMacroCellWithOffset (evolve t lwss)).2 = true := + hcap_of_spaceship lwss lwss_canonical (by decide) (0, 2) lwss_ship4 + lwss_hdiv (by norm_num) (by norm_num) + /-! ## Sanity-checks sur le bestiaire Le fragment `supportInMargin` est **décidable** (instance `Decidable (BoxAssezGrandN)`, diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment_en.lean index b49ac1b5e3..5e05dbb663 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment_en.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeMarginFragment_en.lean @@ -75,6 +75,7 @@ import Conway.Life.AdversarialBattery_en import Conway.Life.HashlifeCorrectness import Conway.Life.LightCone_en import Conway.Life.Oscillators_en +import Conway.Life.PatternTour_en namespace Conway_en open Conway @@ -1926,6 +1927,98 @@ theorem hickersonC3_hcap_of_spaceship_mod : hcap_of_spaceship_mod hickersonC3 hickersonC3_canonical (by decide) (-1, 0) hickersonC3_spaceship hickersonC3_hwin (by norm_num) (by norm_num) +/-! ### Flagship witnesses: glider and LWSS (tranche 11, admission) + +The two **spaceships** announced by the docstring of `hashlife_correct_margin_of_spaceship` +— the glider (`p = 4`, `v = (1, -1)`, "satisfies it strictly") and the LWSS (`p = 4`, +`v = (0, 2)`, "hits the bound exactly") — are admitted by the **dyadic chain** +`hcap_of_spaceship`. For `p = 4 = 2²`, the divisibility premise `4 ∣ 2^level` holds +**as soon as the level reaches `log₂ p = 2`**: it is therefore available for both +witnesses, whose frames reconstruct at levels **3** (glider, side 7) and **4** (LWSS, +side 9). Each `hdiv` is closed by the kernel over its four phases (finite computation); +the tranche 9 containment relaxation is not required for period-4 witnesses. + +**Proof note.** The bestiaire's Bool witnesses (`Life.glider_spaceship`, +`PatternTour.lwss_is_spaceship`) are already certified by the **kernel** reducer (`decide` +on `isSpaceship`, a Bool); the bridge to list equality is `beq_iff_eq` — no +`native_decide`, no added axiom. -/ + +/-- The glider literal is canonical (sorted, duplicate-free): the kernel + certifies it, then `canonical_sortDedup` converts. -/ +theorem glider_canonical : Canonical glider := by + have h : glider = sortDedup glider := by decide + rw [h] + exact canonical_sortDedup _ + +/-- The glider's spaceship relation as a list equality: the Bool witness + `glider_spaceship` (already kernel-certified) lifted to `Prop`. -/ +theorem glider_ship4 : evolve 4 glider = shift (1, -1) glider := + beq_iff_eq.mp glider_spaceship + +/-- The glider's reconstruction frame: offset `(-2, -2)` (margin 2 around the + `[0, 2]²` box). -/ +theorem glider_frame_off : (gridToMacroCellWithOffset glider).1 = (-2, -2) := by decide + +/-- The glider's frame level: side `max(2+5, 2+5) = 7` → level **3** — measured. + Since `3 ≥ log₂ 4 = 2`, the divisibility `4 ∣ 2³ = 8` holds: the glider goes + through the dyadic chain, like the LWSS. -/ +theorem glider_frame_lvl : (gridToMacroCellWithOffset glider).2.level = 3 := by decide + +/-- The LWSS literal is canonical. -/ +theorem lwss_canonical : Canonical lwss := by + have h : lwss = sortDedup lwss := by decide + rw [h] + exact canonical_sortDedup _ + +/-- The LWSS's spaceship relation as a list equality (Bool witness + `lwss_is_spaceship` from `PatternTour`, kernel-certified). -/ +theorem lwss_ship4 : evolve 4 lwss = shift (0, 2) lwss := + beq_iff_eq.mp lwss_is_spaceship + +/-- The LWSS's reconstruction frame: offset `(-2, -2)` (margin 2 around the + `[0, 3] × [0, 4]` box). -/ +theorem lwss_frame_off : (gridToMacroCellWithOffset lwss).1 = (-2, -2) := by decide + +/-- The LWSS's frame level: side `max(3+5, 4+5) = 9` → level 4 — the dyadic + chain applies (`4 ∣ 2⁴`), exactly as the docstring announced. -/ +theorem lwss_frame_lvl : (gridToMacroCellWithOffset lwss).2.level = 4 := by decide + +/-- Divisibility of the period over the LWSS's four phases: each + `evolve i lwss` (`i < 4`) reconstructs at level 4, hence `4 ∣ 2⁴`. The + kernel computation is finite: 4 phases, ≤ 17 cells. -/ +theorem lwss_hdiv : + ∀ i, i < 4 → 4 ∣ 2 ^ (gridToMacroCellWithOffset (evolve i lwss)).2.level := by + intro i hi + interval_cases i <;> decide + +set_option maxRecDepth 1000000 in +/-- Divisibility of the period over the glider's four phases: each + `evolve i glider` (`i < 4`) reconstructs at level 3 (measured for all + four phases), and `4 ∣ 2³`. The kernel computation is finite: 4 phases, + 5-cell grids. -/ +theorem glider_hdiv : + ∀ i, i < 4 → 4 ∣ 2 ^ (gridToMacroCellWithOffset (evolve i glider)).2.level := by + intro i hi + interval_cases i <;> decide + +/-- Capstone: the **glider** is admitted by `hcap_of_spaceship` — the dyadic + chain, like the LWSS (`p = 4 = 2²` divides `2^level` as soon as `level ≥ 2`; + level-3 frame). The speed bound holds strictly (`2·|1| = 2 < 4`, + `2·|-1| = 2 < 4`): for every horizon `t`, the reconstruction of + `evolve t glider` is captured by Hashlife. -/ +theorem glider_hcap_of_spaceship : + ∀ t, jumpCapturedF (gridToMacroCellWithOffset (evolve t glider)).2 = true := + hcap_of_spaceship glider glider_canonical (by decide) (1, -1) glider_ship4 + glider_hdiv (by norm_num) (by norm_num) + +/-- Capstone: the **LWSS** is admitted by `hcap_of_spaceship` — the exact speed + bound (`2·|2| = 4 ≤ 4`) and the dyadic divisibility (`4 ∣ 2⁴`, level-4 + frame) announced by the docstring. -/ +theorem lwss_hcap_of_spaceship : + ∀ t, jumpCapturedF (gridToMacroCellWithOffset (evolve t lwss)).2 = true := + hcap_of_spaceship lwss lwss_canonical (by decide) (0, 2) lwss_ship4 + lwss_hdiv (by norm_num) (by norm_num) + /-! ## Sanity checks on the bestiary The fragment `supportInMargin` is **decidable** (instance `Decidable (BoxAssezGrandN)`,