fix(lean,#13483): tranche 11 — admission des témoins glider et LWSS (chaîne dyadique)

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)`,

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)`,